On Wed, 21 Mar 2012, Christian Sternagel wrote:
Is it just me or is Isabelle/jEdit really much faster than
ProofGeneral/emacs when loading theories? (Maybe this is due to some
other difference between Isabelle2011-1 and the repo version; I only use
emacs if I have to stick to Isabelle2011-1.)
Ça depend, as the French like to say.
Isabelle/jEdit in Isabelle2011-1 and repository versions until today
(8e1b14bf0190) uses a uniform model to process buffer content, intermixed
with potential user edits, with full document markup reports that
eventually causes the "Haribo effect" in the sources. This is done in a
reasonably fast way, but there are still situations where too many goal
states are printed and thus the prover session gets overloaded. (E.g. in
Hoare_Parallel or AFP/JinjaThreads.)
In contrast, Proof General / Emacs is very slow in processing the current
buffer (especially on Mac OS), but resolves imports via the batch-mode
theory loader of Isabelle, which is presently faster than any other way of
processing theories. (The same is used for isabelle usedir/make/makeall.)
The general direction is to unify old-style batch loading with new-style
document processing, such that it is both very fast and produces the full
markup. It will also overcome occasional confusions about different
behaviour of tools in different modes of theory processing.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
