On 16/09/2013 11:28, Makarius wrote:
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.
It's possible the recovery from insufficient memory is not completely
correct. I'm on the point of releasing 5.5.1 so I'd rather not make any
changes just now which might break something else. Perhaps just now it
might be better not to handle the exception.
David
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
