Email Gateway (Aug 19 2022 at 13:12): Email Gateway (Aug 19 2022 at 13:12):From: bnord <bnord01@gmail.com>
Hi Makarius,
I've been working a few days with RC3 now. Even if you say "As long as
it comes back eventually, it is not fully frozen." I find the
responsitivity of Isabelle/jEdit in the presence of non-terminating/slow
tasks unsatisfactory. I regularly have to interrupt my work for 30
seconds or so to wait for Isabelle/jEdit. This often occurs when jumping
back up within a proof and changing something that causes some of the
later commands to diverge or if I simply have some diverging try running
on my last goal which I don't care about at the moment.
Maybe this is a problem which doesn't affect "pro users" as much as they
always know how their proof will work and only type commands that
immediately run successfully. ;)
Another side remark: Where is one supposed to place the sledgehammer
panel in docked mode? I only see three bad options:
Switching between the output and the sledgehammer panel all the time.
Obviously bad.
Docking it at the right. The space there is to thin.
And one feature request:
When ctrl+hovering over some fact/variable whose definition is currently
visible it would be nice if that where high-lighted and maybe
eclipse-like also all occurrences in a different colour.
Best
Benedikt
Email Gateway (Aug 19 2022 at 13:12):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
this is still one more release candidate for the second attempt to make a
stable release of Isabelle this autumn:
http://isabelle.in.tum.de/website-Isabelle2013-2-RC3
The good news is that no new problems have shown up, but I managed to find
a solution to an old problem of external process management.
Notable changes versus Isabelle2013-2-RC2:
* More robust termination of external processes managed by Isabelle/ML:
support cancellation of tasks within the range of milliseconds, as
required for PIDE document editing with automatically tried tools
(e.g. Sledgehammer).
* Clarified application icons and window titles -- more uniform on all
platforms.
* Minimal tuning of some Isabelle/jEdit GUI elements.
The final Isabelle2013-2 release should emerge after 2-3 days of further
testing. This is the very last chance to point out serious drop-outs.
Observations from testing release candidates may be discussed here on
isabelle-users (not isabelle-dev), on the bitbucket tracker
https://bitbucket.org/isabelle_project/isabelle-release/issues or via private
mail.
Makarius
Email Gateway (Aug 19 2022 at 13:12):From: Makarius <makarius@sketis.net>
On Wed, 4 Dec 2013, bnord wrote:
I've been working a few days with RC3 now. Even if you say "As long as
it comes back eventually, it is not fully frozen." I find the
responsitivity of Isabelle/jEdit in the presence of non-terminating/slow
tasks unsatisfactory. I regularly have to interrupt my work for 30
seconds or so to wait for Isabelle/jEdit.
As far as I can tell, Isabelle/Scala and Isabelle/jEdit are waiting for
Isabelle/ML. The interruptibility of the underlying Poly/ML process is
the same all the time, even on the TTY, but the editor model puts more
pressure on it.
Do you have the impression that this behaviour has changed in
Isabelle2013-1 and Isabelle2013-2 compared to Isabelle2012 and
Isabelle2013?
How many "threads" do you have active, compared to the physical hardware?
This can be changed in "Plugin Options / Isabelle / General" and the
effective value is reported by ML "Multithreading.max_threads_value ()".
This often occurs when jumping back up within a proof and changing
something that causes some of the later commands to diverge or if I
simply have some diverging try running on my last goal which I don't
care about at the moment.Maybe this is a problem which doesn't affect "pro users" as much as they
always know how their proof will work and only type commands that
immediately run successfully. ;)
I did not hear anything about such inconveniences in the past couple of
months. On the other hand there were several serious problems that nobody
dared to report.
Another side remark: Where is one supposed to place the sledgehammer panel in
docked mode? I only see three bad options:
1. Switching between the output and the sledgehammer panel all the time.
Obviously bad.
2. Docking it at the right. The space there is to thin.
3. Docking it at the top. Because all the panels waste so much space there
isn't much space left for my proof script, of which I like to see as much as
possible.
You can also dock left, or let the window float (even several copies of
it). The jEdit action isabelle.sledgehammer activates some instance of
the panel according to standard jEdit policies. You can experiment
binding this to some keyboard shortcut.
And one feature request: When ctrl+hovering over some fact/variable
whose definition is currently visible it would be nice if that where
high-lighted and maybe eclipse-like also all occurrences in a different
colour.
Even more could be done there, and is in the pipeline for quite some time
already.
I've got too much side-tracked by technical issues that are strictly
speaking outside my control and responsibility, such as general JVM
integrity and too much divergence and fragmentation of major operating
system platforms.
Makarius
Email Gateway (Aug 19 2022 at 13:12):From: bnord <bnord01@gmail.com>
Hi,
Am 04.12.13 13:00, schrieb Makarius:
Do you have the impression that this behaviour has changed in
Isabelle2013-1 and Isabelle2013-2 compared to Isabelle2012 and
Isabelle2013?
Sorry, can't tell because I didn't use Isabelle/jEdit intensively before.
How many "threads" do you have active, compared to the physical
hardware? This can be changed in "Plugin Options / Isabelle / General"
and the effective value is reported by ML
"Multithreading.max_threads_value ()".
ML "Multithreading.max_threads_value ()" returns 4, I've an Core i5 with
4 hardware threads running on 2 cores, I changed max_threads to 2, I'll
see how that works out.
Best
Benedikt
Email Gateway (Aug 19 2022 at 13:12):From: Makarius <makarius@sketis.net>
Does it mean you are a former Proof General user or non-user?
If you have large "scripts" that depend a lot on sequential stepping and
easily run into non-termination of some parts, you can try flipping the
"Continuous checking" option, e.g. in the Theories panel. There is also a
keyboard shortcut "C+e ENTER" for it, which is a bit reminiscent of
Escape-Meta-Alt-Control-Shift.
This hand-control is a bit odd, but it sometimes helps. The system should
eventually become smarter in just the right scheduling of pending tasks,
but not here and not now.
Makarius
Email Gateway (Aug 19 2022 at 13:12):From: bnord <bnord01@gmail.com>
I had a longer Isabelle brake and before that there was no
Isabelle/jEdit release.
Email Gateway (Aug 19 2022 at 13:13):From: Makarius <makarius@sketis.net>
Some more notes on this: there was a very old race condition where the
external process, when cancelled too early, was not killed at all. This
was not relevant in the past, because cancellation happened only due to
relative long timeouts (seconds) not the user editing (milliseconds).
(This is why I always call the TTY loop "boring", instead of the genuine
interaction that happens in the PIDE document processing game.)
As a consequence, there could be these typical "eprover" processes being
left over, after some minutes or hours of editing with auto sledgehammer
enabled. The new scheme is much more robust, but without any claim for
100% certainty (which is very difficult to achieve with arbitrary POSIX
processes).
The effect was particularly bad on Windows, where process startup takes
approx. 100ms instead of 1..10ms on Unix, but it did happen on Unix in
practice as well. I was finally convinced when I saw a stray "java"
process due to auto nitpick on Linux, so it was neither the notorious
Windows platform nor the very special eprover with its sophisticated
internal signal handling.
Further practical notes on automatically tried tools in Isabelle/jEdit:
* The Isabelle option "threads" should be the physical number of cores.
On Intel hardware with hyperthreading this is doubled by default and
thus reduces editor reactivity by too many parallel tasks.
i3 has 2 cores
i5 has 2 or 4 cores
i7 has 2 or 4 or 6 cores
* "Auto methods", which is similar to the command 'try0', tends to burn
a lot of cycles. Its internal parallelization and the global auto
tool time-out probably require some rethinking: this is still too
close to TTY mode, where the CPU is mostly idle, and sometimes rushes
through a few parallel tasks on all available cores. In PIDE, the
prover does more things all the time -- similar to an operating
system.
Makarius
Email Gateway (Aug 19 2022 at 13:14):From: Julian Brunner <julianbrunner@gmail.com>
The issues I had with RC1 appear to have been fixed in RC2, things ran
fairly smoothly in that version.
My work during the last few days consisted mostly of writing
definitions and thinking on paper, so I haven't had any opportunity to
test the process termination part of RC3 properly, but a few quick
tests indicated that it's working fine there, too.
Last updated: Apr 19 2024 at 16:20 UTC