[isabelle-dev] simplifier trace (and jedit)

[Makarius]

On Wed, 23 May 2012, Christian Sternagel wrote:

> 3) Furthermore, in my course I recommend students (which know about term 
> rewriting before) to have a look at the simplifier trace whenever the 
> simplifier does something unexpected or does not terminate. However, for 
> the latter use-case (i.e., finding cause of nontermination) I do not 
> even know how to do it myself in jedit. As soon as I write, e.g., "apply 
> simp" the simplifier starts to loop, if I don't delete the command it 
> continues looping (and thus the whole system becomes highly unresponsive 
> very soon), if I delete the command, the trace is gone too. Is there any 
> way (or workaround), such that I can generate (part of) the trace of a 
> (potentially) looping reduction.

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.


> Maybe giving a timeout to "apply simp" (but I don't know whether or how 
> this is possible) does work?

Long-running commands are generally bad for reactivity.  Using timeouts 
with some kind of iterative deepening of the amount of checking might help 
here.  It is one of the many fine points in the scheduling that can be 
improved beyond the received PG/TTY model, so that manual cancelation can 
be discontinued altogether at some point.


 	Makarius