Re: [isabelle] Isabelle2013-2-RC3 available for testing
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
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.
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
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
Even more could be done there, and is in the pipeline for quite some time
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and