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
