[isabelle-dev] NEWS: numeral representation
makarius at sketis.net
Mon Mar 26 14:10:55 CEST 2012
On Sun, 25 Mar 2012, Brian Huffman wrote:
> As of 2a1953f0d20d, Isabelle now has a new representation for binary
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?
More information about the isabelle-dev