[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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