[isabelle-dev] NEWS: numeral representation

Lukas Bulwahn bulwahn at in.tum.de
Mon Mar 26 18:00:58 CEST 2012

On 03/26/2012 02:10 PM, Makarius wrote:
> On Sun, 25 Mar 2012, Brian Huffman wrote:
>> As of 2a1953f0d20d, Isabelle now has a new representation for binary 
>> numerals
> Execellent, this is a big step forward in this important reform.  It 
> seems we now have the main parts in place, so that we can start 
> consolidating towards the release over a couple of weeks.  (I am still 
> unsure myself, when the release point will be precisely.)
> Another pending issue of 2a1953f0d20d is HOL-Proofs-Lambda.  When run 
> in parallel it fills up > 25 GB of memory on my 32 GB machine.  When 
> run in x86 mode, it runs out of stack on polyml-5.4.1.  The critical 
> spot might be a definition of datatype or datatype realizer.
> This needs further investigation.  Do you have any ideas on the spot?

This problem is reproducible on our testboard servers.
At the moment, all tests of changesets after 2a1953f0d20d have to be 
manually aborted because of that reason. I hope you find a solution 
quickly, otherwise we should deactivate the Proofs-Lambda theory to keep 
a stable testing environment.


More information about the isabelle-dev mailing list