[isabelle-dev] NEWS: numeral representation

[Lukas Bulwahn]

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.


Lukas