Email Gateway (Aug 19 2022 at 14:07): Email Gateway (Aug 19 2022 at 14:07):From: Lawrence Paulson <lp15@cam.ac.uk>
Without reopening the “what is a bug” debate, I need to say that this sort of thing is inevitable with the approach taken by Isabelle/jEdit, in attempting to process everything, parsing errors and all. If you type in a syntactically incorrect proof, it tries to recover as best it can. In this case, it ignores the syntactically incorrect “show” command, causing the behaviour you observe. An alternative would be to silently insert “sorry” in order to complete the previous proof, preventing that behaviour but having other undesirable consequences.
The best overall approach to all such situations is to fix syntax errors as soon as they are flagged. If I am working on a proof and notice that processing power is being wasted processing some proof text down below, I delete or disable this material. Inserting “sorry” beforehand should always do the trick. Needless to say, your work isn't done until every “sorry” has been removed again.
Larry Paulson
Email Gateway (Aug 19 2022 at 14:07):From: Lars Noschinski <noschinl@in.tum.de>
What I sometimes wished for (in interactive mode) was a way to limit the
resources (in particular cpu-time) consumed by the proof tools. I almost
never write proofs where a single method call takes longer than a
second; so a single proof method which takes more than say 10s is a sure
indication of a broken proof (for me). But this is of course hard to
codify in a robust and system-independent manner ...
Email Gateway (Aug 19 2022 at 14:07):From: Makarius <makarius@sketis.net>
IIRC, you have reported massive waste of CPU cycles and unresponsiveness
before.
This can certainly happen, and the system could be smarter in the
scheduling of tasks. Such improvements are on the TODO list of
improvements (neither "issues" nor "bugs") for several years. The reason
why it is still not done, is lack of priority: I simply don't see really
bad effects so often.
Maybe it is just a problem of adjusting Isabelle multi-threading
parameters to your hardware. The above description sounds like you have
either very few cores (only 2) or a lot of virtual cores (due to
hyperthreading).
Makarius
Email Gateway (Aug 19 2022 at 14:07):From: Makarius <makarius@sketis.net>
("Bug" is indeed a meangingless word, and I can't imagine anybody
attaching that label to this thread.)
The general problem here is how to recover from errors (or
non-termination) while the user is editing some unfinished proof text.
(Really proof text and not proof script because we are in the lucky
situation that Isar proofs have a lot of explicit structure.)
The current implementation is still very crude in this respect. It does
not even "try as best as it can". It merely ignores failed commands, and
often makes a mess while bumping into later parts of the text. An obvious
approach is to take syntactic proof structure into account, using implicit
'sorry' as sketched above (and in fact making 'sorry' obsolete for
end-users).
This is not totally trivial, since a proof might be so broken that the
system cannot guess its structure anymore. So this important reform of
the PIDE document model in that respect is related to proper indendation
support in the editor, which is also lacking from the very start of
Isabelle/jEdit. (It will be probably also the notable point in history,
where hard tabulators are discontinued as "blanks", because they make the
indentation unclear.)
A few months before every release in the past 3 years, I routinely check
if it is now feasible to open that can of interactive structured error
recovery. But again, I don't see it happining for the coming release,
because so many changes in PIDE interaction have already accumulated that
will take months to consolidate and polish.
Makarius
Email Gateway (Aug 19 2022 at 14:07):From: bnord <bnord01@gmail.com>
I can't imagine a situation where I would like Isabelle/jEdit to recover
from a syntax error by ignoring a single show command. I'd rather expect
it to ignore everything from the syntax error until the next "save"
place e.g. a theorem.
I'm also very much against the "insert a sorry" approach. I'd embrace an
"oops" version discarding the last goal.
Best
Benedikt
Email Gateway (Aug 19 2022 at 14:07):From: Makarius <makarius@sketis.net>
Why this? Proofs are conceptually irrelevant in various respects. Local
skips are done in many situations already, with increasing tendency in the
past 7 years.
What is missing in the PIDE model is a global checkpoint to summarise the
degree of "finishedness" of the overall project, or rather an overview of
the inevitably unfinished parts. Right now, users have to do this via
eye-balling on the Theories dockable.
Makarius
Email Gateway (Aug 19 2022 at 14:07):From: bnord <bnord01@gmail.com>
When inserting my previous example 6 times I get no feedback in the
sixth version. (The first four loop the fifth yields feedback the sixth
doesn't. I have two cores with four threads, I've set parallel proofs to
two.)
I'd tag a single looping thread as undesirable and would understand
tagging thins with "meaningless" words as artistic freedom.
I just reported this to make sure it's on such a list and maybe increase
it's relative priority a little.
Best
Benedikt
Email Gateway (Aug 19 2022 at 14:07):From: Makarius <makarius@sketis.net>
Time limits indeed introduce erratic behaviour. Nonetheless, I have
something like this on my list of further improvements of PIDE document
processing for a long time. It might be even done in a manner of
"iterative deepening", with 2-3 rounds of attempts to check some piece of
text with increasing timeout. Doing that with a few milliseconds in the
first round might even have a big impact on overall reactivity of the
proof checking game, although that is pure speculation at the moment.
Makarius
Email Gateway (Aug 19 2022 at 14:07):From: bnord <bnord01@gmail.com>
Am 22.04.14 14:15, schrieb Makarius:
On Tue, 22 Apr 2014, bnord wrote:
I'm also very much against the "insert a sorry" approach. I'd embrace
an "oops" version discarding the last goal.Why this?
Because they're insufficiently highlighted and not tracked through later
proofs.
Proofs are conceptually irrelevant in various respects. Local skips
are done in many situations already, with increasing tendency in the
past 7 years.What is missing in the PIDE model is a global checkpoint to summarise the
degree of "finishedness" of the overall project, or rather an overview
of the inevitably unfinished parts. Right now, users have to do this
via eye-balling on the Theories dockable.Makarius
Email Gateway (Aug 19 2022 at 14:08):From: Makarius <makarius@sketis.net>
So far this does not disprove my reasing.
Just the standard game:
* What is your hardware precisely?
* What is your operating system?
* What is your Isabelle version?
* What are your Isabelle options for "threads" and "parallel_proofs"?
Makarius
Email Gateway (Aug 19 2022 at 14:08):From: Makarius <makarius@sketis.net>
On Tue, 22 Apr 2014, bnord wrote:
Am 22.04.14 14:15, schrieb Makarius:
On Tue, 22 Apr 2014, bnord wrote:
I'm also very much against the "insert a sorry" approach. I'd embrace an
"oops" version discarding the last goal.Why this?
Because they're insufficiently highlighted and not tracked through later
proofs.
OK. That is subsumed by:
What is missing in the PIDE model is a global checkpoint to summarise the
degree of "finishedness" of the overall project
Makarius
Email Gateway (Aug 19 2022 at 14:08):From: bnord <bnord01@gmail.com>
Am 22.04.14 14:28, schrieb Makarius:
So far this does not disprove my reasing.
Wasn't meant to disprove anything.Just the standard game:
* What is your hardware precisely?
Macbook Pro with 2.4GHz Core i5 (2 Cores with 4 Threads) and 8GB of Ram
* What is your operating system?
OS X 10.9.2
* What is your Isabelle version?
2013_2
* What are your Isabelle options for "threads" and "parallel_proofs"?
0 and 2
Makarius
Email Gateway (Aug 19 2022 at 14:08):From: Makarius <makarius@sketis.net>
That is a relatively weak CPU, but Intel makes it appear stronger via
hyperthreading, thus it gets somewhat overloaded and burns a lot of CPU
cycles (literally, by turning them into heat).
So lets try the following parameters:
threads = 2
and in $ISABELLE_HOME_USER/etc/settings:
ML_OPTIONS="-H 500 --gcthreads 2"
This requires a "reboot" of Isabelle.
The above will be morally the default in the next Isabelle release,
because David Matthews now uses explicit information about virtual CPU
cores.
For mobile systems it could also make sense to use only half of the number
of real CPU cores, although for 2 cores that gives an unexciting 1 with
quite different interactive behaviour in sequential mode.
Makarius
Email Gateway (Aug 19 2022 at 14:08):From: bnord <bnord01@gmail.com>
Thanks, this helped with the responsiveness.
Email Gateway (Aug 19 2022 at 14:08):From: Lars Noschinski <noschinl@in.tum.de>
You have now often recommended reducing the number of threads to the
number of real physical cores. Does this hold for interactive mode only?
Because on my machine (a quadcore with 8 virtual cores), there are
several theories in the AFP with a speedup factor around 5 or even 6; so
at least raw throughput sometimes profits from the virtual cores on
Isabelle workload.
-- Lars
Email Gateway (Aug 19 2022 at 14:08):From: Makarius <makarius@sketis.net>
I also do systematic "overburning" of CPU cycles in batch mode, it gives
me (real) warp factor 9.6 for 8 real cores (Intel Xeon from 2009) --
hyperthreading actually has a purpose. Concerning the "factor" one needs
to be careful, though: the figure given in Isabelle build on the spot is
merely the relative burn-factor of CPU cycles, and that is a quite
distorted version of the true speed-up factor compared to sequential mode.
So yes, one could probably make this a general rule of thumb: interactive
mode refers to physical CPU cores and batch more to the maximum number of
virtual CPU cores, even more.
I usually get that effect by having the persistent default options as
described before, which will be also the default in the next release.
For batch builds I then give a generous -j4 to the implicit -o threads=4.
In this "4x4" mode (which means "4-wheel drive" in French), I get the
"sound of speed" in my office from the CPU fans, and Isabelle + AFP built
quite fast.
Makarius
Email Gateway (Aug 19 2022 at 14:09):From: Thomas Sewell <thomas.sewell@nicta.com.au>
I'd just like to add that this problem can be compounded by some other
issues, such as one we mentioned before where a diverging "blast" can
slow down jEdit. On rare occasions I've had to go hunting for blasts and
fastforces in the future part of my theory just to get enough CPU back
to work on the problem I have.
Not sure what else to say about it, but if some improvement to the
prioritising of these speculative calculations could be made, I'd be all
for it.
Cheers,
Thomas.
Email Gateway (Aug 19 2022 at 14:09):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I remember Coq has a different way to handle this: there are explicit
forward and backward (in proof state) commands. The processed part of a
proof is not editable and one have to go backward to edit it, then go
forward again and resume up to the last proof statement. This is sometime
tedious, while clean.
That's a way too much different compared to what Isabelle users are
accustomed to. Personally, it happens I think about the Coq way when I
feel Isabelle process too much of invalid text during editing, while in
other cases, I enjoy the reactivity of feedback from Isabelle while
editing.
May be an idea could be to have a keystroke to quickly enable/disable
“Continuous checking”… a keystroke, so that this would remain handy while
editing: no need to leave the keyboard to go from and to the mouse to
check/uncheck the option and no need to have the theories panel always
visible (otherwise needed, as the option is located on this panel).
Email Gateway (Aug 19 2022 at 14:09):From: Lawrence Paulson <lp15@cam.ac.uk>
You seem to be describing Proof General, which is still available for Isabelle, but no longer supported.
We have to live with the problems of a radically new interaction paradigm that’s still being fleshed out. Maple, for example, offers a superficially similar document model, but you can’t tell whether what you are looking at has been evaluated or not, and even Maple itself doesn’t seem to know. That approach is efficient but has many of its own limitations.
Larry Paulson
Email Gateway (Aug 19 2022 at 14:09):From: Lars Noschinski <noschinl@in.tum.de>
On 23.04.2014 05:27, Yannick Duchêne (Hibou57) wrote:
I remember Coq has a different way to handle this: there are explicit
forward and backward (in proof state) commands. The processed part of
a proof is not editable and one have to go backward to edit it, then
go forward again and resume up to the last proof statement. This is
sometime tedious, while clean.
This is the classic way of Proof General, which also was the main
Isabelle UI till ~3 years ago.May be an idea could be to have a keystroke to quickly enable/disable
“Continuous checking”… a keystroke, so that this would remain handy
while editing: no need to leave the keyboard to go from and to the
mouse to check/uncheck the option and no need to have the theories
panel always visible (otherwise needed, as the option is located on
this panel).
In 2013-2, this is bound to C+e ENTER.
BTW, there are many actions in the Isabelle plugin which can be
potentially bound to a shortcut, but aren't by default. To see them, go to
Utilities / Global Options / jEdit / Shortcuts
and select "Plugin: Isabelle" in the "Edit Shortcuts" dropdown.
-- Lars
Email Gateway (Aug 19 2022 at 14:10):From: Makarius <makarius@sketis.net>
Funny that you see the difference of Coq vs. Isabelle today like that, as
someone who did not know Isabelle about 3 years ago, when Proof General
was still the default.
In 1998, David Aspinall started an important pan-European prover interface
project called "Proof General". He asked several prover experts to help
him connect their particular system to that still emerging and
revolutionary front-end. I was the one to do the Isabelle/Isar
connection, when Isar itself was just about to emerge.
Note that "... while clean" above does not really apply, especially for
Coq. The real prover syntax is too complex for Proof General and its
modest elisp code to guess what the text means to the prover process.
The Coq toplevel also has some legacy operations from the pre-Proof
General era that make this harder than in Isabelle, and some Coq users are
actually still using the TTY loop (which normally does not happen for
Isabelle, because the Isar language makes this hard).
15 years ago there were also various internal discussions about the key
concepts how the prover front-end and back-end processes should
communicate, and certain fundamental limitations were already
well-understood, imposed by accidental side-conditions of existing
provers and the Emacs LISP machine.
Much of that is forgotten to outsiders now, and many Proof General users
think of it as something that has to be exactly like it is, because they
have never seen anything else. This lack of imagination and stagnation is
escpecially frustrating for me when I see the Proof General clone n + 1,
with excactly the same limitations, and just some change in colors and
icons.
The PIDE project came out of this more about 6 years ago, and it has
required a bit longer than expected to make it all ready for prime time.
Today it is hard to imagine anybody still using Isabelle Proof General,
and de-facto there has been nobody else maintaining it for about 3 years.
Makarius
Email Gateway (Aug 19 2022 at 14:10):From: Makarius <makarius@sketis.net>
That is unrealated to thread scheduling. It is merely the oldest trick
that tools can play on the front-end to bomb it, by emitting vast amounts
of "potentially useful" tracing information.
That is already resolved for the coming release, see also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-December/msg00138.html
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-December/004919.html
A prover that is running efficiently on more and more cores poses extra
challenges on the front-end. But even with single-threaded Proof General,
the danger had been there all the time. When I discovered an easy
workaround with "nice" on Unix in 2006, it was too late: the single-core
era had already ended and that crude process priority trick was useless,
except on my last 1-core laptop.
Makarius
Email Gateway (Aug 19 2022 at 14:24):From: bnord <bnord01@gmail.com>
I'd expect the following issue to be well known but didn't find it in
the "known issues".
When inserting a new goal (have ...) into a proof, proof methods
belonging to later goals seem to be applied wrongly sometimes causing
them to loop and make my PC noisy after a while. ;)
Here's a small example:
lemma assumes "m ∈ M" and "M ⊆ N" shows "m ∈ N" proof -
have P(* incomplete goal *)
show "m ∈ N" using assms by (metis in_mono) (* loops *)
qed
The "show" already produces a syntax error but the later "by" is applied
anyhow yet to the wrong goal causing it to loop.
A student of mine is highly skilled in producing such situations in many
theorems simultaneously causing the editor to become very unresponsive.
Best Benedikt
Last updated: Apr 20 2024 at 08:16 UTC