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?
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
