Email Gateway (Aug 22 2022 at 14:12): Email Gateway (Aug 22 2022 at 14:12):From: Manuel Eberl <eberlm@in.tum.de>
Yes, that was me. The "transfer" tool is the most "reliable" way to
produce such a situation, but I occasionally observe similar situations
with other proof methods as well.
Manuel
Email Gateway (Aug 22 2022 at 14:13):From: Makarius <makarius@sketis.net>
I think these are just variations on the old theme of Denial-of-Service
attack on the Prover IDE by massive markup reports. Here it is the
backtracking from "transfer" to "simp", which is invoked afresh each
time, with repeated reports. Thus the IDE is busy stacking up duplicate
markup trees, and reactivity of interrupts is generally delayed -- it
should stop eventually, though.
The same happens in Isabelle2016 already, and probably several earlier
releases. It is unclear to me, why the problem has now more impact in
practice.
Anyway, in changesets
http://isabelle.in.tum.de/repos/isabelle/rev/2efc128370fa and
http://isabelle.in.tum.de/repos/isabelle/rev/681fae6b00b5 I have
reworked that a bit to produce PIDE markup exactly once.
This can be tried out with the nightly snapshot from
http://isabelle.in.tum.de/devel (produced in approx. 2h when all works
well).
There will be also a formal release candidate Isabelle2016-1-RC1,
probably within 24h.
Makarius
Email Gateway (Aug 22 2022 at 14:14):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
the year 2016 is an "Isabelle leap-year", with more than one release.
(The usual distance between regular releases is 8-10 months.)
Many changes and improvements have been accumulated in the past few
months. A preview of what is coming is available here:
http://isabelle.in.tum.de/website-Isabelle2016-1-RC0
This corresponds to Isabelle/666c7475f4f7 and AFP/1e958cc1942e. Note
that the website and documentation still need to be updated.
Despite the name "Isabelle2016-1", this is not a revised version of
Isabelle2016, but a completely new major release. See also
the NEWS file
http://isabelle.in.tum.de/website-Isabelle2016-1-RC0/dist/Isabelle2016-1-RC0/doc/NEWS.html
When discussing problems, observations, suggestions, etc. the mail
subject line should be changed to something meaningful (but the release
candidate number still given in the message body).
Makarius
Email Gateway (Aug 22 2022 at 14:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,
I played a bit with RC0 and noticed that reactivity seems to be a bit lower than with
Isabelle2016. In particular, when I have a non-terminating proof command like
subgoal by transfer simp
and (due to some changes in the theory above) the proof loops, then I have found no way to
interrupt the proof. Even when I delete the whole line, PolyML and the JVM keep running at
100% for minutes and I don't get any updates in the output or state buffer any more. I
really have to shut down Isabelle/jEdit and restart to get back to work. This never
happened to me with Isabelle2016 in the past six months.
In the test, I ran Isabelle with the default settings on a quad core Intel from 4 years
ago with 16GB of RAM under Ubuntu 14.04.
Andreas
Email Gateway (Aug 22 2022 at 14:14):From: Lars Hupel <hupel@in.tum.de>
Dear Makarius,
I noticed that auto-indentation is switched on by default. While this
improves the workflow when typing, it complicates it when committing: it
tends to introduce trailing spaces.
For example, when I finish a sub-proof like this:
have "..." ...<Enter>
<Enter>
...
Now, the middle line contains two trailing spaces. This is mildly
annoying, because I want to avoid checking in trailing spaces into
version control.
The workaround I'm employing currently is the "WhiteSpace" plugin
(<http://plugins.jedit.org/plugins/?WhiteSpace>) which allows to purge
trailing spaces on save. It can also be configured to just show them and
not purge them automatically.
Cheers
Lars
Email Gateway (Aug 22 2022 at 14:22):From: Makarius <makarius@sketis.net>
Someone else reported a similar problem some weeks ago.
Is there a concrete example somewhere, that shows the effect?
Makarius
Email Gateway (Aug 22 2022 at 14:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
All the concrete cases in which I ran into this problem have been fixed now. But I've
attached a small example that shows the problem. The lemma has a pointless assumption, but
this is only to get the theorem sufficiently large such that transfer runs for a while
As is, the proof of the lemma goes through, but if you delete the declaration of
map_concat as a simp rule, then it will not, but keep running for quite some time (if your
patience is longer than mine, just add a few more universal quantifiers in the assumptions
of the lemma; the backtracking in transfer grows exponentially with the number of
quantifiers). What I then typically do is to change the non-terminating line of proof,
usually by adding a space somewhere in transfer (i.e., "by tra nsfer simp") or completely
deleting it.
But despite these changes, the proof method keeps running and Isabelle/jEdit does no
longer update the Output and State panels any more.
Best,
Andreas
Scratch.thy
Last updated: Nov 21 2024 at 12:39 UTC