Email Gateway (Aug 19 2022 at 12:34): Email Gateway (Aug 19 2022 at 12:34):From: Peter Lammich <lammich@in.tum.de>
Hi all,
while giving a tutorial on Isabelle, I run into the following strange
effect, where jEdit seems to indicate that a lemma is proven. Actually,
the lemma just contains a diverging method invocation. See screenshot.
To reproduce this behaviour, just load the attached theory file, wait a
few seconds (the simp add: A A[symmetric] is marked purple now). Then
move the cursor after the lemma and type some newlines, save the file,
and you get (on my machine) the above effect. You can even use the lemma
to prove further non-theorems from it without any problems!
False.png
False.thy
Email Gateway (Aug 19 2022 at 12:34):From: Peter Lammich <lammich@in.tum.de>
Another, even nastier, way to reproduce this behaviour:
Load the theory and wait some time (a few minutes or so),
then the purple mark goes away automagically.
This is confusing, in particular if you use some long-running proof
methods or switch to another workspace while your proofs run through ...
if you return to jEdit after a few minutes, it seems as everything went
through.
Email Gateway (Aug 19 2022 at 12:34):From: Peter Lammich <lammich@in.tum.de>
To be more precise: On my machine, the time required until the command
appears as processed is, nondeterministically, something between a few
seconds (!) and a few minutes, so it is almost impossible to distinguish
a long-running method-invocation from a diverging one.
Email Gateway (Aug 19 2022 at 12:35):From: bnord <bnord01@gmail.com>
Hi,
I can reproduce this easily on OS X and Windows with Isabelle2013-1.
Any edit after the non terminating command suffies, no saving or waiting
required.
So if one, in good hope, simply presses return, after the command was
dispatched, the markup disappears and the command seems to be fine.
Very nasty. ;) Couldn't reproduce it with Isabelle2013.
Best
Benedikt
Email Gateway (Aug 19 2022 at 12:35):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
you probably missed the relevant entry in the NEWS for Isabelle 2013-1:
* Prover IDE -- Isabelle/Scala/jEdit *
[…]
Personally, I am delighted to see this finally happening, I'd say it's
about time. In fact, it may be the one thing that finally gets me to
abandon Proof General in favour of jEdit.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 12:35):From: Peter Lammich <lammich@in.tum.de>
It seems to work with any diverging command, not only simp.
Thus, a minimal example is to type
lemma False by (intro TrueE) <RETURN>
and after you typed RETURN, the thing appears proven in jEdit.
-- Peter
Email Gateway (Aug 19 2022 at 12:35):From: Makarius <makarius@sketis.net>
I still need to check what actually happens here.
In the meantime just a few hints:
* jEdit is a plain text editor, it proves nothing.
* Isabelle/jEdit is a Prover IDE, which gives you some view on the
interactive document model of Isabelle/Scala, where things really
happen in conjunction with the Isabelle/ML process.
* Just like in Proof General Emacs, there is no guarantee that something
that "looks checked" actually is checked. In Proof General the
quick_and_dirty flag is enabled by default, and Isabelle/jEdit
is likewise relatively bold in favour of performance, instead of
strictness of checking.
I've occasionally seen very bad drop-outs in the past, when some Swing GUI
component was crashing and displaying outdated content, e.g. a solved goal
state instead of a failed one.
This does not mean that such things should happen too easily. I do have
the ambition to make the Prover IDE appear as correctly as feasible, even
though authentic proof checking only happens in batch mode. We have this
principle for almost 20 years already: only batch builds really count.
Makarius
Email Gateway (Aug 19 2022 at 12:35):From: Makarius <makarius@sketis.net>
Such jokes are funny on 01-Apr, but not for production versions of
Isabelle, especially after an unusually long phase of testing release
candidates.
As there is a tendency here to blame Isabelle/jEdit versus Isabelle Proof
General, I would like to remind that I was responsible for the latter as
well.
5 years ago, I started to move away from the TTY model of Proof General,
in order to support interactive document processing natively in
Isabelle/Scala.
2 years ago, the first stable release of Isabelle/jEdit came out (as part
of Isabelle2011-1).
October 2011 also marks the point where I stopped doing any work on Proof
General. As I had been the only one to do anything for Proof General over
several years, the number has dropped to zero ever since.
People who are still using Proof General should see what they can do
themselves to maintain it. I can give some hints how to get involved --
or just look at http://proofgeneral.inf.ed.ac.uk/devel
Makarius
Email Gateway (Aug 19 2022 at 12:35):From: Christoph Feller <c_feller@informatik.uni-kl.de>
Hallo,
I just wanted to add that I migrated to Isabelle/JEdit recently (with
Isabelle 2013-1) and I was rather confused by this behaviour, too.
Regards,
Christoph Feller
Email Gateway (Aug 19 2022 at 12:36):From: Makarius <makarius@sketis.net>
The behaviour is definitely bad. I still need to investigate it further.
So far I can only declare the extra-long testing phase before the
Isabelle2013-1 release a failure. Instead of spending several weeks
myself in an alert situation to make sure that all goes well, I went on
vacation in the middle of the process.
Problem reports then came in right after official lift-off, as was already
the tendency in the last 2 or 3 times.
Makarius
Email Gateway (Aug 19 2022 at 12:36):From: Makarius <makarius@sketis.net>
I confirm that this is a serious problem. Thanks for reporting this.
I need further digging in the sources and history to work to the bottom of
it. I am also getting mentally ready for another release very soon.
Are there any further serious problems in Isabelle2013-1 that nobody has
dared to report yet?
It is part of the routine of release management to "disprove" the need for
immediate changes in the last moment. The incident here was actually
introduced by trying to "fix" the sledgehammer panel at the end of
September, just before the Isabelle2013-1-RC phase started
(https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-September/004689.html).
This dilemma of accepting or not accepting issues sometimes discourages
people to report things, but the principles of empiric science help: plain
observations, no "fixes", no "bugs", no nonsense.
Makarius
Email Gateway (Aug 19 2022 at 12:37):From: Makarius <makarius@sketis.net>
The situation is indeed so bad that I am about to produce a new stable
release of Isabelle2013-2 soon: the first (and probably only) release
candidate is scheduled for Sun 24-Nov-2013 and the final release for Sun
01-Dec-2013.
So if there is anything else to report, there are a few days left to do it
in a relaxed manner. Changing a formal release candidate next week
requires more weight and gravity. The current state of affairs can be
seen here https://bitbucket.org/isabelle_project/isabelle-release/commits
For completeness, here is a wrapup of the incident.
Formally, the interactive front-ends (Proof General, Isabelle/jEdit, or
whatever), are not required to be fully authentic. Only batch builds
really count at the end of the day. But a system that breaks down too
easily is not a stable release. (This concept is taken seriously for
Isabelle, against the tides of the time.)
Here the problem is that editing a running task with internal parallel
forks can cause accidental interrupts, which are not reported as error to
the front-end, because they should not happen under normal circumstances.
So the proof status appeared OK on the surface, but the internal thm was
in a "failed state" -- as correctly recorded by the LCF-kernel.
The source of the problem is twofold: (1) a genuine mistake in the
implementation of the Execution.fork mechanism of PIDE, which caused the
accidental interrupt of a running task (Sep-2013). (2) failure to report
the interrupt as error on purpose (!) "to avoid confusion in log etc." as
the changelog entry says (Oct-2012). The "log etc." refers to batch
builds, TTY mode, and Proof General, which is easily confused by error
messages coming in the wrong moment.
This illustrates again the problems of having too many old and new things
in an increasingly complex system. I am trying for years to unify the
batch build with the PIDE interaction model, which is difficult in its own
right. The legacy interaction modes of TTY or Proof General are adding to
the complication.
Last spring, I actually dismantled the old PGIP experiment, which greatly
simplified the classic Proof General mode and recovered some long lost
functionality. Likewise, a much greater relieve will happen when Proof
General itself comes out of use and can be dismantled.
I've no idea how long it will take to sort it all out. The number of
people who are still using Proof General is unclear to me. When traveling
to ITP 2013 this summer, my guess was 40% Isabelle/jEdit vs. 60% Proof
General among power users, but it turned out the opposite when traveling
back home.
Maybe we should make a "coming out" session at ITP 2014: "My name is
P. W. User, ... and I am still using Proof General" :-)
(Further elaboration Proof General issues deserve a separate mail thread.)
Makarius
Email Gateway (Aug 19 2022 at 12:37):From: Gottfried Barrow <gottfried.barrow@gmx.com>
That's what I was talking about. In the the drop-down box, there's the
string "Previously entered strings:". There's nothing ever there except
for that message.
Regards,
GB
theory i131123a__scala_hask_for_meta_obj_imps
imports Complex_Main
begin
definition metaImp :: "prop => prop => prop" where
"metaImp x y == (PROP x ==> PROP y)"
definition objToMetaImp :: "bool => bool => prop" where
"objToMetaImp x y == (x ==> y)"
definition objImp :: "bool => bool => bool" where
"objImp x y == (x --> y)"
export_code metaImp objToMetaImp objImp in Scala file "i131123a.scala"
export_code metaImp objToMetaImp objImp in Haskell file "."
end
Email Gateway (Aug 19 2022 at 12:37):From: Makarius <makarius@sketis.net>
The history text field updates its history when you type RETURN into it,
which then also has the effect of "Apply". The Apply button alone does not
update the history.
Since the Sledgehammer panel is new, I did not have any ambitions to make
it super fancy. Just plain and solid functionality.
Note that for Isabelle2013-2, I did already change the spontaneous restart
behaviour of sledgehammer after editing the text:
https://bitbucket.org/isabelle_project/isabelle-release/commits/50169ef2cca3
You can try that when Isabelle2013-2-RC1 appears.
Makarius
Email Gateway (Aug 19 2022 at 12:37):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 11/22/2013 4:16 PM, Makarius wrote:
The history text field updates its history when you type RETURN into
it, which then also has the effect of "Apply". The Apply button alone
does not update the history.
That does it. In the find panel and sledgehammer panel, I was executing
the commands with the mouse.
I make a tangent here, which is not a complaint. It's just to inform you
on how some people work, and how it's related to getting info in the IDE.
I work a lot with my right hand on the mouse, and my left hand far away
from the keyboad. That causes me to prefer looking at info in the output
panel, rather than moving my left hand to the keyboard to press the
control key.
There are also two other things which prevent me from taking full
advantage of the info you make available. In the IDE gutter, I always
have line numbers displayed. Consequently, your icons aren't displayed.
As far as I can tell, I can't show both line numbers and information
icons in the gutter.
I also set the tooltip delay to about 1.5 seconds, because in Windows,
when I start typing, I immediately get an error, and a popup window pops
up where the mouse cursor is, which is where the text cursor is, and it
beeps at me for every character I type. The workaround is to move the
mouse cursor away from the text cursor before I begin typing, but I
don't remember to do that, so I set the tooptip delay to be long, which
is not optimal for cntl-mouse hovering.
You don't need to respond to any of that. I say it to explain that there
are a number of reasons that keep me hooked on output panel for info,
among which is wanting to see lots of info at once, primarily to see all
of the typing, bracketing, and constants.
Note that for Isabelle2013-2, I did already change the spontaneous
restart behaviour of sledgehammer after editing the text:
https://bitbucket.org/isabelle_project/isabelle-release/commits/50169ef2cca3You can try that when Isabelle2013-2-RC1 appears.
Okay. I'll try it out. I never actually switched beyond
Isabelle2013-1-RC3, except for a small test of Isabelle2013-1 on my laptop.
Thanks,
GB
Email Gateway (Aug 19 2022 at 12:38):From: Makarius <makarius@sketis.net>
Such precise descriptions of the manner of working are very important, to
help figure out further refinements of the Prover IDE.
Makarius
Last updated: May 07 2024 at 01:07 UTC