On 05/23/2012 10:38 PM, Makarius wrote:
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.
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. 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). (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).
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
