Post by MakariusPost by Daniel HorneI'm running into situations where the polyml executable is running
out of memory and being killed when it uses ~4Gb of memory.
It is relatively rare that Isabelle applications run out of ML heap
memory. It might indicate an abnormal situation, e.g. a
non-terminating tool that allocates data structures indefinitely.
Well, this is with the 2015 distribution on either windows 7 or gentoo
linux x86_64. I'm trying to model the subset of c++ I use (mostly for
learning purposes), and I'm trying to create a set of functions that
correspond to a simple parser - namely in this case classifying whether
a particular char is valid as part of an identifier. So I created this:
fun isIdentifierStartChar:: "char ⇒ bool" where
"isIdentifierStartChar CHR ''_'' = True" |
"isIdentifierStartChar CHR ''a'' = True" |
"isIdentifierStartChar CHR ''b'' = True" |
"isIdentifierStartChar CHR ''c'' = True" |
"isIdentifierStartChar CHR ''d'' = True" |
"isIdentifierStartChar CHR ''e'' = True" |
"isIdentifierStartChar CHR ''f'' = True" |
"isIdentifierStartChar CHR ''g'' = True" |
"isIdentifierStartChar CHR ''h'' = True" |
"isIdentifierStartChar CHR ''i'' = True" |
"isIdentifierStartChar CHR ''j'' = True" |
"isIdentifierStartChar CHR ''k'' = True" |
"isIdentifierStartChar CHR ''l'' = True" |
"isIdentifierStartChar CHR ''m'' = True" |
"isIdentifierStartChar CHR ''n'' = True" |
"isIdentifierStartChar CHR ''o'' = True" |
"isIdentifierStartChar CHR ''p'' = True" |
"isIdentifierStartChar CHR ''q'' = True" |
"isIdentifierStartChar CHR ''r'' = True" |
"isIdentifierStartChar CHR ''s'' = True" |
"isIdentifierStartChar CHR ''t'' = True" |
"isIdentifierStartChar CHR ''u'' = True" |
"isIdentifierStartChar CHR ''v'' = True" |
"isIdentifierStartChar CHR ''w'' = True" |
"isIdentifierStartChar CHR ''x'' = True" |
"isIdentifierStartChar CHR ''y'' = True" |
"isIdentifierStartChar CHR ''z'' = True" |
"isIdentifierStartChar CHR ''A'' = True" |
"isIdentifierStartChar CHR ''B'' = True" |
"isIdentifierStartChar CHR ''C'' = True" |
"isIdentifierStartChar CHR ''D'' = True" |
"isIdentifierStartChar CHR ''E'' = True" |
"isIdentifierStartChar CHR ''F'' = True" |
"isIdentifierStartChar CHR ''G'' = True" |
"isIdentifierStartChar CHR ''H'' = True" |
"isIdentifierStartChar CHR ''I'' = True" |
"isIdentifierStartChar CHR ''J'' = True" |
"isIdentifierStartChar CHR ''K'' = True" |
"isIdentifierStartChar CHR ''L'' = True" |
"isIdentifierStartChar CHR ''M'' = True" |
"isIdentifierStartChar CHR ''N'' = True" |
"isIdentifierStartChar CHR ''O'' = True" |
"isIdentifierStartChar CHR ''P'' = True" |
"isIdentifierStartChar CHR ''Q'' = True" |
"isIdentifierStartChar CHR ''R'' = True" |
"isIdentifierStartChar CHR ''S'' = True" |
"isIdentifierStartChar CHR ''T'' = True" |
"isIdentifierStartChar CHR ''U'' = True" |
"isIdentifierStartChar CHR ''V'' = True" |
"isIdentifierStartChar CHR ''W'' = True" |
"isIdentifierStartChar CHR ''X'' = True" |
"isIdentifierStartChar CHR ''Y'' = True" |
"isIdentifierStartChar CHR ''Z'' = True" |
"isIdentifierStartChar a = False"
.and isabelle crashes after several minutes of it being purpled-out. I
guess it's the sheer number of terms here that's causing the problem.
Post by MakariusPost by Daniel HorneThe machine I'm working on has 12Gb of ram, so I thought I might
attack this problem by using a 64-bit version of the relevant programs.
In order to switch the ML system into x86_64 mode, you can edit
ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$ML_HOME/../$ML_PLATFORM"
Isabelle/jEdit supports symbolic file names with $ literally as
written above.
Great - I'll try that, thanks.