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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
