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

Reply via email to