Re: [isabelle] Insufficient memory when building heap image
- To: Jasmin Blanchette <jasmin.blanchette at gmail.com>
- Subject: Re: [isabelle] Insufficient memory when building heap image
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Mon, 01 Oct 2012 05:33:32 +0200
- Cc: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <2EFF753A-F553-42D0-BEDF-4DACCD2BC394@gmail.com>
- References: <5065BA13.firstname.lastname@example.org> <2EFF753A-F553-42D0-BEDF-4DACCD2BC394@gmail.com>
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:15.0) Gecko/20120907 Thunderbird/15.0.1
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and