[isabelle-dev] Remaining uses of Proof General?

[Matthew Fernandez]

On 29/04/14 01:04, Makarius wrote:
> On Mon, 28 Apr 2014, Matthew Fernandez wrote:
>> My reasons are mostly predictable execution, as I can control what the prover is up to with
>> explicit stepping forwards and backwards. I can probably achieve the same result toggling
>> continuous checking on/off in Isabelle/jEdit, but haven't invested the time in modifying my workflow.
>
> Can you say more about typical situations?  When doing occasional debugging, either of tools or the
> system itself, I need more knowledge about what happens when exactly.  I never do this in Proof
> General these days, but within the Prover IDE in a buffer that contains only the main items of
> interest.  Then I edit carefully, based on educated guesses how the PIDE document model works, or I
> toggle the continuous checking that was newly introduced in Isabelle2013-2.

Currently most of my theories are generated by another tool. When debugging the generated theories,
I often have to open a file that I know contains many broken proofs. In these circumstances it can
be beneficial to have a way of stepping into the middle of a broken proof to explore, while ignoring
all the following (also broken) proofs). Having said that, this cuts both ways. Isabelle/jEdit's
behaviour of continuing in the face of broken proofs can allow me to explore a proof in the middle
of a theory without needing to tediously repair the broken proofs preceding it. To summarise, I use
whichever tool is most applicable to my current situation, but predominantly Isabelle/jEdit.

>> I've also encountered the problems discussed in other threads of the Isabelle/jEdit GUI locking up
>> when some tactic is looping and the JVM heap being exhausted with no indication from the UI.
>
> I reckon that this refers to the official Isabelle2013-2 release.  I have reworked many details of
> scheduling in the past few months, even just now when writing this email.  When the Isabelle2014-RC
> line starts (probably in July) you should look precisely at your typical applications to see how it
> works.  I don't want to see again a situation where problem reports trickle only slowly *after* the
> release is shipped.

Yes, sorry, you are correct. Either way, any UI issues I have encountered are subsumed by threads
others have raised on this mailing list.

________________________________

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.