Re: [isabelle] Insufficient memory when building heap image




Am 01/10/2012 10:25, schrieb Jasmin Blanchette:
> 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).

Sorry, I misunderstood you. Then we are in violent agreement ;-)

Tobias

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