• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
      • Break-rewrite
      • Proof-builder
      • Accumulated-persistence
      • Cgen
      • Forward-chaining-reports
      • Proof-tree
      • Print-gv
      • Dmr
      • With-brr-data
      • Splitter
      • Guard-debug
      • Set-debugger-enable
      • Redo-flat
      • Time-tracker
      • Set-check-invariant-risk
      • Removable-runes
      • Efficiency
      • Explain-near-miss
      • Tail-biting
      • Failed-forcing
      • Sneaky
      • Invariant-risk
      • Failure
      • Measure-debug
      • Dead-events
      • Compare-objects
      • Prettygoals
      • Remove-hyps
      • Type-prescription-debugging
      • Pstack
      • Trace
        • Trace$
        • Wet
        • Trace!
        • Break-on-error
        • Set-trace-evisc-tuple
        • Untrace$
        • Open-trace-file
        • Open-trace-file!
        • Close-trace-file
      • Set-register-invariant-risk
      • Walkabout
      • Disassemble$
      • Nil-goal
      • Cw-gstack
      • Set-guard-msg
      • Find-lemmas
      • Watch
      • Quick-and-dirty-subsumption-replacement-step
      • Profile-all
      • Profile-ACL2
      • Set-print-gv-defaults
      • Minimal-runes
      • Spacewalk
      • Try-gl-concls
      • Near-misses
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Debugging

Trace

Tracing functions in ACL2

ACL2 provides a trace utility, trace$, with corresponding reverse operation untrace$. These can be used without any dependence on the underlying Lisp utility, and are the tracing utilities of choice in ACL2; see trace$ and see untrace$.

However, for advanced users we note that the underlying host Lisp may also provide a trace utility, trace, and corresponding untrace. Moreover, these have been modified in the case that the host Lisp is GCL, Allegro CL, or CCL (OpenMCL), to provide limited support for :entry, :exit, and perhaps :cond keywords, to hide certain large data structures (world, enabled structure, rewrite constant), and to trace executable-counterparts (see evaluation). See source files *-trace.lisp. For the above Lisps, you can invoke the original trace and untrace by invoking old-trace and old-untrace, respectively, in raw Lisp rather than in the normal ACL2 loop.

Subtopics

Trace$
Trace function evaluations
Wet
Evaluate a form and print subsequent error trace
Trace!
Trace the indicated functions after creating an active trust tag
Break-on-error
Break when encountering a hard or soft error caused by ACL2
Set-trace-evisc-tuple
Set the trace evisc tuple
Untrace$
Untrace functions
Open-trace-file
Redirect trace output to a file
Open-trace-file!
Redirect trace output to a file, even within events
Close-trace-file
Stop redirecting trace output to a file