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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
