makarius at sketis.net
Mon Sep 16 12:28:57 CEST 2013
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_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.
More information about the isabelle-dev