Re: [isabelle] Insufficient memory when building heap image



Am 01.10.2012 um 05:33 schrieb Tobias Nipkow:

> Am 28/09/2012 17:26, schrieb Jasmin Blanchette:
>> 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...

By "in general", I meant "as the default for both interactive and noninteractive". (Remember: Manuel was suggesting making the PG defaults the defaults for command-line.) I'm a big fan of quick-and-dirty for the interactive mode myself, as can be seen from the source code of the new (co)datatype package (grep quick_and_dirty ~/isabelle/src/HOL/BNF/Tools/*ML).

When it comes to having one vs. two modes, my comment was meant as a general programming guideline, not an actual opinion of mine on this specific case:

> 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.


It's just one of many usually conflicting criteria that must be considered when developing software.

Jasmin






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