Major Section: MISCELLANEOUS
This documentation topic explains messages printing by the theorem prover about the tau-system, as follows.
During a proof you may see a message such as the following.
TIME-TRACKER-NOTE [:TAU]: Elapsed runtime in tau is 4.95 secs; see :DOC time-tracker-tau.
Just below a proof summary you may see a message such as the following.
TIME-TRACKER-NOTE [:TAU]: For the proof above, the total runtime spent in the tau system was 30.01 seconds. See :DOC time-tracker-tau.
Both of these messages are intended to let you know that certain prover heuristics (see tau-system) may be slowing proofs down more than they are helping. If you are satisfied with the prover's performance, you may ignore these messages or even turn them off by disabling time-tracking entirely (see time-tracker). Otherwise, here are some actions that you can take to solve such a performance problem.
The simplest solution is to disable the tau-system, in either of the following equivalent ways.
(in-theory (disable (:executable-counterpart tau-system))) (in-theory (disable (tau-system)))
But if you want to leave the tau-system enabled, you could investigate the
possibility is that the tau-system is causing an expensive
:
logic
-mode function to be executed. You can diagnose that problem
by observing the rewriter -- see dmr -- or by interrupting the system
and getting a backtrace (see set-debugger-enable). A solution in that case
is to disable the executable-counterpart of that function, for example in
either of these equivalent ways.
(in-theory (disable (:executable-counterpart foo))) (in-theory (disable (foo)))As a result, the tau-system will be weakened, but perhaps only negligibly.
In either case above, you may prefer to provide :
in-theory
hints
rather than :in-theory
events; see hints.
A more sophisticated solution is to record values of the
:
logic
-mode function in question, so that the tau-system will look
up the necessary values rather than calling the function, whether or not the
executable-counterpart of that function is enabled. Here is an example of a
lemma that can provide such a solution. See tau-system.
(defthm lemma (and (foo 0) (foo 17) (foo t) (not (foo '(a b c)))) :rule-classes :tau-system)