On Mon, 28 Apr 2014, Andreas Lochbihler wrote:
My main usage of PG is when I want to construct a complicated proof method
call like
(fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ...
simp del: ...)+
that collapses an apply script of a hundred lines. I haven't yet found a
convenient way to write the apply script in Isabelle/jEdit, because of
reactivity issues (see item 2 below) and the continuous updates of the output
window (when I scroll to some other part of the apply script using the cursor
keys). Are there key bindings for scrolling that do not move the cursor?
This reminds me of a very old insider jokes from the mid-1990-ies: Dieter
Nazareth had finished the W0 formalization where he had turned half-decent
tactic scripts into such compact one-liners, and shortly afterwards
Wolfgang Naraschewski had to disentangle that again for the full W
formalization, or rather start from scratch. A few years later, the Isar
language emerged and made that approach in principle obsolete.
Back to the actual technical questions. What are the main performance
bottle-necks here? Printing of intermediate goal states? Or applying
intermediate steps repeatedly?
As you move the cursor over commands, the Output updates itself, without
any activity from the prover. The prover prints states as you change the
editor view, e.g. by scrolling or resizing the window. You can disable the
Auto-update of the Output dockable, but that does not affect the proof
process, only the display.
You can prevent the prover from burning cycles either by reducing the
number of worker threads, or disabling the continuous checking.
I can say more when I understand the actual problem better. In such
situations I normally have to see the dynamics of how you actually work.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
