Messages about expensive use of the tau-system
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 that the tau-system is causing an expensive
(in-theory (disable (:executable-counterpart foo))) (in-theory (disable (:e 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
A more sophisticated solution is to record values of the
(defthm lemma (and (foo 0) (foo 17) (foo t) (not (foo '(a b c)))) :rule-classes :tau-system)