[isabelle-dev] Isabelle_10-Sep-2013

[David Matthews]

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