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.


isabelle-dev mailing list

Reply via email to