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

Reply via email to