7
$\begingroup$

Some time ago I asked this question on Stack Overflow but got no answer:

https://stackoverflow.com/questions/60521384/tracing-tactics-in-isabelle

Section 9.4 The Classical Reasoner of the Isar Reference Manual writes:

The tactics can be traced, and their components can be called directly; in this manner, any proof can be viewed interactively.

I have found sections in this manual about tracing the simplifier and higher order unification.

How can I trace the classical reasoner?

$\endgroup$

1 Answer 1

8
$\begingroup$

I recall there is no end-user method to trace the classical reasoner, but there is a diagnosis configuration.

You should add a line setup "Config.put_global Blast.trace true" and further uses of blast will output the a (rather verbose) trace-like report.

I believe that you can combine this with a judicious use of declare [[blast_depth_limit=n]] with an appropriate non-negative n to dissect the output.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.