Re: [isabelle] Insufficient memory when building heap image



On Mon, 1 Oct 2012, Jasmin Blanchette wrote:

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.

Having "modes", i.e. opportunities for slightly changed behaviour is indeed evil in its own right. In the end the possibilities of every system component that might change its behaviour are multiplied, so you get an exponential number of oddities in the worst case.

The traditional "interactive mode" vs. "batch mode" has accumulated quite a few such oddities over time, and it will take a few more years to chop off most of the heads of the hydra.


Quick and dirty mode is a well-known special case of this principle, and Proof General has depended on it a lot, and will continue to do so, because it is not moving anymore.

These things need to be understood from their historic context and technical side-condutions. In the next Isabelle release, the regular Isabelle/jEdit interaction mode will already work smoothly without quick and dirty, because proofs are parallel by default, and not so expensive after all in the overall bilance.

At some later stage the competiting "skip_proofs" feature should be somehow integrated into the parallel interaction model, lets say as forked proofs that are deferred for much longer, or indefinitely.


	Makarius





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