*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Isabelle 2014 and proof general*From*: Thomas Sewell <thomas.sewell at nicta.com.au>*Date*: Thu, 18 Sep 2014 20:25:42 +1000*In-reply-to*: <alpine.LNX.2.00.1409102031580.41896@lxbroy10.informatik.tu-muenchen.de>*References*: <A216A54B-BD72-4913-ADE9-B545E83D0813@cmu.edu> <alpine.LNX.2.00.1409102031580.41896@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.1.1

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.

**Follow-Ups**:**Re: [isabelle] Isabelle 2014 and proof general***From:*Carst Tankink

**References**:**[isabelle] Isabelle 2014 and proof general***From:*Vadim Zaliva

**Re: [isabelle] Isabelle 2014 and proof general***From:*Makarius

- Previous by Date: [isabelle] Lemma pos_mod_bound
- Next by Date: Re: [isabelle] Isabelle 2014 and proof general
- Previous by Thread: Re: [isabelle] Isabelle 2014 and proof general
- Next by Thread: Re: [isabelle] Isabelle 2014 and proof general
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list