rene.thiemann at uibk.ac.at
Mon Sep 16 15:34:54 CEST 2013
>> I've made my own tests with the following setup:
>> Poly/ML SVN 1848
>> IsaFoR a44e26d6605e
>> Isabelle a49ce8d72a44
>> AFP 4e87a0fc2528
>> 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?
More information about the isabelle-dev