[isabelle-dev] simplifier trace (and jedit)
makarius at sketis.net
Fri May 25 11:01:28 CEST 2012
On Thu, 24 May 2012, Christian Sternagel wrote:
>> The Prover Session panel has check/cancel buttons that are reminiscent
>> of manual control in PG. The keyboard shortcuts are C-SPACE and
>> C-BACKSPACE, respectively. You need to avoid rash movements after
>> cancelation, outerwise the checking process restarts.
> I overlooked those, thanks! Unfortunately, this does not work very well
> (or maybe I misunderstood the intended way of use). I don't see the
> purpose of "Check", since it seems that as soon as I start typing again,
> asynchronous checking does start anyway.
Normally the implicit execution process follows the "perspective" of the
editor, i.e. the set of visible text ranges. So when you move around and
expose more text, it causes updates on the perspective (edits) and
The "Check" button or C-SPACE key pretends that the whole buffer is
visible, and thus commences its full checking until you change the
Eventually, I would like to make this yet more declarative, with some
properties to control the checking process of the session, say to assert
that a certain subgraph of the current session is processed continously.
> While clicking on "Cancel" does not always cancel the process (or maybe
> there is just a huge delay, since the trace is so big; anyway the result
> is that jedit becomes unresponsive and I basically have to kill it).
This could well be. The protocol is asynchronous and maximizes
throughput, without any flow control. So the prover can easily cause
denial-of-service of the front-end side.
After all these years with this fundamental problem of high-volume traces,
I think I now know how to avoid it in the first place. The idea is to
"pause" prover transactions in certain situations, say after a certain
amount of tracing messages have been output. The user then needs to react
on it, by clicking somewhere in the Output window, or entering some text
in an input field.
This could work via Future.promise/fulfill in a similar way like the
Invoke_Scala.method function in Isabelle/ML. This works, because the
documen model is inherently multi-threaded.
> The keyboard shortcuts do not work for me, C-SPACE is already in use in
> my GNOME, so I know why this does not work, but C-BACKSPACE apparently
> does backwards deletion of a word inside jedit; I'll check whether this
> works when I set different keyboard shortcuts).
It is C-E SPACE and C-E BACKSPACE, and a bit too close to
ESCAPE-META-ALT-CONTROL-SHIFT. C-E is a common jEdit prefix for certain
"extended" key sequences.
See also the jEdit "Shortcuts" options in the "Plugin: Isabelle" section.
More information about the isabelle-dev