[isabelle-dev] simplifier trace (and jedit)

[Christian Sternagel]

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