[isabelle-dev] Remaining uses of Proof General?
andreas.lochbihler at inf.ethz.ch
Tue Apr 29 08:54:01 CEST 2014
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.
More information about the isabelle-dev