[isabelle-dev] NEWS: interactive simplifier trace
c.sternagel at gmail.com
Fri Feb 28 13:36:51 CET 2014
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?
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
More information about the isabelle-dev