Major Section: MISCELLANEOUS
General Forms: :ttags-seen (ttags-seen)Suppose the output is as follows.
(T NIL)
(FOO "/home/bob/bar.lisp"
"/home/cindy/bar.lisp")
Warning: This output is minimally trustworthy (see :DOC TTAGS-SEEN).
This output indicates that the current logical world has seen the
declaration of trust tag T at the top-level (see defttag) and the
declaration of trust tag FOO in the two books included from the listed
locations. The warning emphasizes that this command cannot be used to
validate the ``purity'' of an ACL2 session, because using a ttag renders
enough power to hide from this or any other command the fact that the ttag
was ever declared.
As discussed elsewhere (see defttag), the only reliable way to validate
the ``purity'' of a session is to watch for ``TTAG NOTE'' output.
Another shortcoming of this command is that it only checks the current
logical world for ttag declarations. For example, one could execute a
defttag event; then use progn! and set-raw-mode to replace
system functions with corrupt definitions or to introduce inconsistent axioms
in the ground-zero world; and finally, execute
:ubt! 1 to remove all evidence of the ttag in the world
while leaving in place the corrupt definitions or axioms. The base world is
now tainted, meaning we could prove nil or certify a book that proves
nil, but the resulting session or book would contain no trace of the ttag
that tainted it!
Despite shortcomings, this command might be useful to system hackers. It
also serves to illustrate the inherent flaw in asking a session whether or
how it is ``tainted'', justifying the ``TTAG NOTE'' approach
(see defttag).
