Major Section: EVENTS
Example: (regenerate-tau-database) General Form: (regenerate-tau-database :doc doc-string)where
doc-string is an optional documentation string not beginning
with ``:Doc-Section ...''. Because no unique name is associated with a
regenerate-tau-database event, there is no way we can store the
documentation string doc-string in our il[documentation] database.
Hence, we actually prohibit doc-string from having the form of an ACL2
documentation string; see doc-string.The tau database is regenerated by scanning the current logical world and re-processing every rule-generating event in it relative to the current enabled theory and current tau auto mode settings. See introduction-to-the-tau-system for background details.
This command was intended to allow the user to remove a fact from the tau
database, by regenerating the database without the fact. But as the
following discussion highlights, regenerate-tau-database does not really
solve the problem. We regard it as a placeholder for a more sophisticated
mechanism. However, we have trouble understanding why a user might wish to
remove a fact from the database and are awaiting further user experiences
before designing the more sophisticated mechanism.
Suppose, for example, that you wanted to remove a signature rule provided by some rule with name rune. You could disable rune and regenerate the database. We discuss why you might -- or might not -- want to do this later. But suppose you did it. Unfortunately, the database you get will not be just like the one you started with minus the signature rule. The reason is that the database you started with was generated incrementally and the current theory might have evolved. To take a simple example, your starting database might have included a rule that has been disabled since it was first added. Thus, the part of your starting database built before the disabling was constructed with the rule enabled and the part built afterwards has the rule disabled. You are unlikely to get the same database whether you enable or disable that rule now.
You might hope that the avoidance of in-theory events would eliminate the
problem but it does not because even the ground-zero theory is
constructed incrementally from the ``pre-history'' commands used to boot up
ACL2. Those pre-history commands include some global in-theory commands.
Since every session starts from the ground-zero state, the starting
database is already ``infected'' with global in-theory commands.
The reason we hope that it will not be necessary to remove tau facts is that the tau system is designed merely to be fast and benign (see Design Philosophy in introduction-to-the-tau-system). The tau system's coverage should grows monotonically with the addition of rules. According to this understanding of tau, adding a signature rule, for example, may allow tau to prove some additional goals but will not prevent it from proving goals it could prove previously. If this is understanding of tau is accurate, we see no fundamental reason to support the removal of a fact. This, of course, ignores the possibility that the user wishes to explore alternative proof strategies or measure performance.
We welcome user observations and experience on this issue.
