[isabelle-dev] Remaining uses of Proof General?

[Andreas Lochbihler]

On 28/04/14 22:25, Makarius wrote:
> 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.
I know, I have myself untangles such one-liners often enough when something has changed. 
Nevertheless, I believe that I'm still faster to build these one-liners than write pretty 
Isar proofs of hundreds of lines, just because the goal states are huge and all cases are 
shown in the same way.

> Back to the actual technical questions.  What are the main performance bottle-necks here?
> Printing of intermediate goal states?  Or applying intermediate steps repeatedly?
There are hardly any performance problems in terms of computing power, possibly except for 
Isabelle processing a slow call to auto over and over again. The efficiency problem is the 
interaction with the IDE. I use the Find panel a lot, but then my output panel is not 
visible at the same time (that's why I would like to split the right dock in two). And 
when I scroll upwards to find a snippet of tactic script that I want to copy, the output 
updates and my current goal state is gone. (I know I could disable the updating, but then 
I have to enable it manually again.)

> 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.
Maybe I can show you what my problems are at ITP in Vienna in July.

Andreas