Re: [isabelle] 64 bit distro available?



On 22/11/2015 19:36, Makarius wrote:
On Sun, 22 Nov 2015, Daniel Horne wrote:

I'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.


The 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 $ISABELLE_HOME_USER/etc/settings like this:

  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.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.