How to enable Trace in Isabelle / jEdit

Question

I'm a vim fan, but only emacs has an Isabelle / HOL environment. jEdit is fine, but I can't use

using [[simp_trace=true]] 

like in emacs.

How to enable tracing in jEdit?

Answer 1

You can really use simp_trace in the middle of the proof in Isabelle / jEdit, for example:

 lemma "(2 :: nat) + 2 = 4" using [[simp_trace]] apply simp done 

Alternatively, you can declare it globally, for example:

 declare [[simp_trace]] lemma "(2 :: nat) + 2 = 4" apply simp done 

Both give you a simplification trace in the Exit window when your cursor immediately after the apply simp in jEdit.

Answer 2

If you need a track depth deeper than 1 (default), you set it to

 declare [[simp_trace_depth_limit=4]] 

This example gives track depth 4.

Answer 3

As others have pointed out, you can use simp_trace. However, you can also use simp_trace_new in combination with the Simplify Trace window. This provides an improved output compared to simp_trace:

 lemma "rev (rev xs) = xs" using [[simp_trace_new]] apply(induction xs) apply(auto) done 

To view the trace, place the cursor on "apply (auto)", then click on "See traceifier trace". The Trace Accelerator window opens (tab). Click Show Trace, and a new window should appear showing the trace for each subgoal.

The Isabelle / Isar link contains more detailed information:

simp_trace_new controls simplification tracing in Isabelle / PIDE applications, in particular Isabelle / jEdit.
This provides a hierarchical representation of the rewriting steps performed by the Uptifier.
Users can customize behavior by specifying breakpoints, verbosity, and enabling or disabling interactive mode.
In regular verbosity (the default), only the rules corresponding to the breakpoint apply. user shown . In full, all application rules will be registered. Interactive mode interrupts the normal flow of Resistance and discards the decision on how to continue working with the user through any dialogue with a graphical interface.

Alternatively, you can specify "using the link [[simp_trace_new mode = full]]" here to see all the steps taken by the simplifier.

NOTE: in the previous example, showing the trace "apply (induction xs)" does not output.