Re: [isabelle] 64 bit distro available?



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.