Re: [isabelle] 64 bit distro available?



The second part should, of course read:

Or you can import "~~/src/HOL/Library/Char_ord" and do

definition "isIdentifierStartChar c â
  c = CHR ''_'' â (c â CHR ''A'' â c â CHR ''Z'') â (c â CHR ''a'' â c â CHR ''z'')

For code generation, this is probably the most efficient way to state it.


On 22/11/15 21:53, Manuel Eberl wrote:
I very much recommend that you define your function differently, e.g.

definition "isIdentifierStartChar c â
   c â set ''_abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ''"

Or you can import "~~/src/HOL/Library/Char_ord" and do

definition "isIdentifierStartChar c â
   c â set ''_abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ''"


Cheers,

Manuel


On 22/11/15 21:34, Daniel Horne wrote:
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.