traceFeedback.trace : string * int -> ('a -> 'b) -> 'a -> 'bInvoke a function with a specified level of tracing.
The trace function is used to set the value of a tracing
variable for the duration of one top-level function call.
A call to trace (nm,i) f x attempts to set the tracing
variable associated with the string nm to value
i. Then it evaluates f x and returns the
resulting value after restoring the trace level of nm.
Fails if the name given is not associated with a registered tracing variable. Also fails if the function invocation fails.
> load "mesonLib";
val it = (): unit
> trace ("meson",2) prove
(concl SKOLEM_THM,mesonLib.MESON_TAC []);
0 inferences so far. Searching with maximum size 0.
0 inferences so far. Searching with maximum size 1.
Internal goal solved with 2 MESON inferences.
2 inferences so far. Searching with maximum size 0.
2 inferences so far. Searching with maximum size 1.
Internal goal solved with 4 MESON inferences.
4 inferences so far. Searching with maximum size 0.
4 inferences so far. Searching with maximum size 1.
Internal goal solved with 6 MESON inferences.
6 inferences so far. Searching with maximum size 0.
6 inferences so far. Searching with maximum size 1.
Internal goal solved with 8 MESON inferences.
solved with 8 MESON inferences.
val it = ⊢ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x): thm
> traces();
val it =
[BasicProvers.var_eq_old: 0 [0..1], Definition.TC extraction: 0 [0..5],
Definition.allow_schema_definition: 0 [0..1],
Definition.auto Defn.tgoal: 1 [0..1],
Definition.delete support defs: 1 [0..1],
Definition.induction derivation: 0 [0..1],
Definition.storage_message: 1 [0..1],
Definition.termination candidates: 0 [0..4],
EmitTeX: K&R record type defns: 1 [0..1],
EmitTeX: dollar parens: 1 [0..1],
EmitTeX: print datatype names as types: 0 [0..1],
EmitTeX: print datatypes compactly: 0 [0..1],
EmitTeX: print thm turnstiles: 1 [0..1],
Goalstack.howmany_printed_assums: 1000000 [0..1000000],
Goalstack.howmany_printed_subgoals: 10 [0..10000],
Goalstack.other_subgoals_pretty_limit: 100 [0..100000],
Goalstack.print_assums_reversed: 0 [0..1],
Goalstack.print_goal_at_top: 0 [0..1],
Goalstack.print_goal_fvs: 0 [0..1],
Goalstack.show_proved_subtheorems: 1 [0..1],
Goalstack.show_stack_subgoal_count: 1 [0..1], Greek tyvars: 1 [0..1],
Ho_Rewrite: 0 [0..1], HolSatLib_warn: 1 [0..1],
PAT_ABBREV_TAC: match var/const: 1 [0..1], PP.avoid_unicode: 0 [0..1],
PP.catch_withpp_err: 1 [0..1], PP.print_firstcasebar: 0 [0..1],
PP.qblock_smash_limit: 4 [0..1000], PPBackEnd show types: 1 [0..1],
PPBackEnd use annotations: 1 [0..1], PPBackEnd use css: 1 [0..1],
PPBackEnd use styles: 1 [0..1],
Parse.unicode_trace_off_complaints: 1 [0..1], QUANT_INST_DEBUG: 0 [0..3],
QUANT_INST_DEBUG_DEPTH: 5 [0..2000],
QUANT_INST___REC_DEPTH: 250 [0..20000],
QUANT_INST___print_term_length: 2000 [0..2000], RealArith dp: 0 [0..1],
Rewrite: 0 [0..1], Theory.allow_rebinds: 0 [0..1],
Theory.debug: 0 [0..1], Theory.save_thm_reporting: 1 [0..2],
TheoryPP.include_html_docs: 1 [0..1], Unicode: 1 [0..1],
Unicode Univ printing: 1 [0..1], Univ pretty-printing: 1 [0..1],
Vartype Format Complaint: 1 [0..1], ambiguous grammar warning: 1 [0..2],
assumptions: 0 [0..1], computeLib.auto_import_definitions: 1 [0..1],
guess overloads: 1 [0..1], inddef strict: 0 [0..1], meson: 1 [0..2],
metis: 1 [0..10], normalForms: 0 [0..10],
notify type variable guesses: 1 [0..1], numeral types: 0 [0..1],
paranoid string literal printing: 0 [0..1], pp_annotations: 1 [0..1],
pp_array_types: 1 [0..1], pp_avoids_symbol_merges: 1 [0..1],
pp_cases: 1 [0..1], pp_dollar_escapes: 1 [0..1], pp_num_types: 1 [0..1],
pp_unambiguous_comprehensions: 0 [0..2], print_tyabbrevs: 1 [0..1],
report_thy_times: 1 [0..1], show_alias_printing_choices: 1 [0..1],
show_typecheck_errors: 0 [0..1], simplifier: 0 [0..7],
syntax_error: 1 [0..1], types: 0 [0..2], use pmatch_pp: 1 [0..1]]:
trace_elt listFeedback, Feedback.register_trace,
Feedback.reset_trace,
Feedback.reset_traces,
Feedback.set_trace,
Feedback.traces, Lib.with_flag