[isabelle-dev] NEWS: interactive simplifier trace

[Christian Sternagel]

Dear Lars,

today I first tried using the new simplifier tracing facility (within 
Isabelle/jEdit). I just started but have already some questions ;)

In the Simplifier Trace panel itself I did not find out how to get any 
output. Only after pressing the "Show Trace" button a new window opens 
that contains the output.

Also in the output, as opposed to [[simp_trace]] I do not see output for 
recursive calls in conditional rewriting (for the single example I 
tried). Is there an option to get this?

And two general questions (sorry if this is already documented). What is 
the meaning of "Auto update" and "Auto reply" in this panel?

cheers

chris

On 02/04/2014 10:55 AM, Lars Hupel wrote:
> As of Isabelle/885500f4aa6a:
>
>    New panel: Simplifier trace.  Provides an interactive view of the
>    simplification process, enabled by the newly-introduced
>    "simplifier_trace" declaration.
>
> Note that the previous "simp_trace" declaration continues to be available.
>
>
> To make use of the new tracing facility, the declaration
>
>    [[simplifier_trace mode=full]]
>
> can be used. It produces (roughly) the same information as the old
> trace. The trace isn't displayed in the "Output" panel though, but
> rather in a "Trace window" which can be opened via the "Show trace"
> button in the "Simplifier trace" panel. For some more details, refer to
> the attached "user manual" (draft). It is an excerpt from my MSc thesis
> and not yet incorporated into the main Isabelle documentation.
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>