Re: [isabelle] Isabelle 2014 and proof general



A week or two ago, Makarius asked us the canonical question:
  "Are there any remaining uses of Proof General?"

I take it Makarius is inquiring whether there are any applications left
that *require* ProofGeneral as opposed to one of the PIDE implementations.

It happens that earlier in the year, I used ProofGeneral to do some
surgery on the "Fastpath" proof. This is the largest and worst of the
proofs about the C code of seL4. At the time I felt that Isabelle/jEdit
was unworkable for this task. I investigated this again today.

I'm now convinced I can do further surgery on this proof using only
PIDE, although the process is currently slower and more painful than
using ProofGeneral.

Those who are interested in pathological uses of Isabelle can find the
proof I'm talking about on github https://github.com/seL4/l4v and the
relevant file here
https://github.com/seL4/l4v/blob/master/proof/crefine/Fastpath_C.thy
although there may be difficulty in building the proof. We're thinking
about simplifying the build process in the future.

It is very important to set the goal print limit to 1. Otherwise too
much CPU is lost attempting to print goals, and Isabelle/jEdit gives at
least the impression that it has broken down entirely. Once the goals
limit is set to 1, Isabelle/jEdit succeeds in reporting on all points in
the proof *eventually*.

I also set the goals limit to 1 in ProofGeneral. This was easier,
firstly because there is a menu option, and secondly because watching
the "blue region" makes it clear how much time is lost on printing.

In Isabelle/jEdit I had to declare [[goals_limit = 1]] explicitly in the
text. Unfortunately this requires backing up to a sensible place. After
some thought I've added "using [[goals_limit = 1]]" permanently to the
two worst proof scripts.

Is there any particular reason why the goals limit isn't a setting that
can be adjusted from a panel or the options in Isabelle/jEdit?

I also tried the "parallel_print" setting which Makarius added when I
last brought this up. This does more or less the opposite of what I
want. However, like ProofGeneral's blue region, it makes it easy to see
the problem. After moving the cursor down rapidly, the window "greys
out" for a while, and then returns to white one line at a time as the
goal states print in order. This process might take a minute or so.

This explains why Isabelle/jEdit seems so slow in these cases: the goal
states render in order, while the user waits for output where their
cursor actually is. In the parallel case the window goes white
immediately once the print tasks have forked, from which point there is
no indication of progress, giving the impression the system has just
given up.

Ideally I'd like to see some approximation ProofGeneral's behaviour, in
which many commands can be processed and only one goal state rendered.
Yes, my proofs are pathological, full of applications of fast
methods/tactics but with large complex goal states. I suspect, however,
that I'm not alone.

Cheers,
    Thomas.


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.