TRACE!

trace the indicated functions after creating an active trust tag
Major Section:  TRACE

Example:
(trace! (fact :entry (list 'tracing-mark (car arglist))))

General Form: (trace! fn1 fn2 ... fnk)

where the fni are suitable arguments to the underlying Lisp trace.

Trace! is a version of trace$ that avoids the need for an already-active trust tag (or ``ttag''; see defttag), as explained below. If each fni is a symbol, you may prefer simply to use trace$. Alternatively, you can use trace$ in raw Lisp, though evaluating forms in raw Lisp should be viewed as a hack that invalidates any logical claims made about that ACL2 session.

See untrace$ for how to undo the effect of trace!.

Consider the following example, essentially suggested by Peter Dillinger:

(value-triple (trace$ (bar :entry (defun foo () 17))))
Clearly, a trace performed of bar can change the definition of an existing defined function foo; and this can render ACL2 unsound!

Thus, if trace$ is given any argument that is not a symbol, then there must be an active trust tag (see defttag). A user who is hacking may prefer to use a command that takes care of this issue automatically, and trace! is such a command. The evaluation of a trace! causes temporary creation of an active trust tag, :trace!, followed by the corresponding trace$ form. The trust tag will disappear when the call to trace! completes. Even though trace! will remove its temporary ttag, it will still print a ``TTAG NOTE'', which indicates that the session is suspect. See defttag and see ttags-seen for further remarks on this issue.