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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and