[isabelle-dev] Isabelle_10-Sep-2013

[René Thiemann]

>> I've made my own tests with the following setup:
>> 
>> Poly/ML SVN 1848
>> IsaFoR a44e26d6605e
>> Isabelle a49ce8d72a44
>> AFP 4e87a0fc2528
>> 
>> ML_PLATFORM="x86-darwin"
>> ML_HOME="/Volumes/Macintosh_HD/Users/makarius/lib/polyml/polyml-svn/x86-darwin"
>> ML_SYSTEM="polyml-5.5.1"
>> ML_OPTIONS="--minheap 500 --gcthreads 4 --debug=sharing"
> 
>> If you say that we can just absorb an exception Fail "Insufficient memory" in ML, we can do that on the Isabelle/ML side as a workaround.
> 
> Trying PolyML.shareCommonData PolyML.rootFunction with some exception handling, there is another breakdown with PolyML.SaveState.saveState:
> 
>  Assertion failed: (space != 0), function ScanAddressAt, file exporter.cpp, line 187.

Since the problem seems to be not that easy to fix, and since the 64-bit mode does not seem to have this problem, 
would it be sensible to make the 64-bit version the default for Isabelle on MacOS? Or are there other known problems with
the 64-bit version?

René