set_trace

Feedback.set_trace : string -> int -> unit

Set a tracing level for a registered trace.

Invoking set_trace n i sets the level of the tracing mechanism registered under n to be i. These settings control the verboseness of various tools within the system. This can be useful both when debugging proofs (with the simplifier for example), and also as a guide to how an automatic proof is proceeding (with mesonLib for example).

There is no single interpretation of what activity a tracing level should evoke: each tool registered for tracing can treat its trace level in its own way.

Failure

A call to set_trace n i fails if n has not previously been registered via register_trace. It also fails if i is less than zero, or if it is greater than the trace’s specified maximum value.

Example

   - set_trace "Rewrite" 1;

   - PURE_REWRITE_CONV [AND_CLAUSES] (Term `x /\ T /\ y`);

   <<HOL message: Rewrite:
   |- T /\ y = y.>>

   > val it = |- x /\ T /\ y = x /\ y : thm

See also

Feedback, Feedback.register_trace, Feedback.reset_trace, Feedback.reset_traces, Feedback.trace, Feedback.traces