[isabelle] »strict« or »sequential« mode in Isabelle/jEdit?



During fine-point tuning of a huge bunch of theories (e.g.
Multivariate_Analysis / Probability in Isabelle/HOL), I am often in the
situation to incrementally adjust the sources following the error
reporting of Isabelle/jEdit (e.g. adding a simp rule and adjusting
subsequent broken proofs).

In this particular situation I experience two inconveniences with
continuous proof checking »as it is« in Isabelle/jEdit:

* The prover tries to work hard to give early feedback on the current
focus of the edit panel, e.g. leaving proofs unfinished in earlier
theories and so on.  Thus the (expected) spots of problems get reported
quite late, and, after adjusting those spots, a lot of material which
follows afterwards has to be re-checked.

* If existing proofs degenerate into non-termination, the risk is that
these spots will consume a lot of resources and turn Isabelle/jEdit
little reactive until the spots are identified and interrupted by hard
edits.

What works as workaround is to set the number of threads temporarily to
1.  Beside the comparably deep path through GUI elements for switching
back and forth, parallelism (e.g. wrt. complete theories) is entirely lost.

I'm not sure how relevant this is (how do other people experience such
situations?), but maybe there is a different approach to the whole
scenaio which so far did not come to my mind.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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