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