Re: [isabelle] Insufficient memory when building heap image



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. Then you're thankful that your command-line-based nightly tests have it disabled.

Jasmin






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