[isabelle-dev] Isabelle_10-Sep-2013

[Makarius]

On Fri, 13 Sep 2013, Makarius wrote:

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


 	Makarius