Re: [isabelle] Insufficient memory when building heap image

Am 28/09/2012 17:26, schrieb Jasmin Blanchette:
> Am 28.09.2012 um 16:54 schrieb Manuel Eberl:
>> In my case, loading everything in Proof General works, loading
>> everything in batch mode does not work. Based on that, I would argue
>> that whatever options Proof General does run things with are a good
>> idea, not a mistake. Therefore, I cannot quite follow your reasoning here.
> I think Makarius just means that it's generally a bad idea to have two modes, because it's more likely that at least one of them will break.
> I don't know for the other options, but "quick and dirty" is certainly not a good idea in general, as illustrated recently on this mailing list by Brian Huffman, who derived "False" by exploiting a bug in the "datatype" package.

I beg to differ. It has saved users countless hours waiting for packages to
perform long routine proofs. So it certainly was of great benefit at the time.
And if you think green IT...

> Then you're thankful that your command-line-based nightly tests have it disabled.

Anything else would be throwing the baby out with the bath water.


> Jasmin

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.