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 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)