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 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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.