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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
