• 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

• Trace

Open-trace-file!

Redirect trace output to a file, even within events

See open-trace-file for a utility that redirects trace output to a file. The utility, open-trace-file!, is similar, but differs from open-trace-file in the following two ways.

• You can use open-trace-file! within make-event forms, and thereby within books.
• An active trust tag is required (see defttag) when calling open-trace-file!.

For example, we can open a trace file as follows, but the second form fails to open a trace file if open-trace-file! is replaced by open-trace-file.

(defttag t)
(make-event
 (pprogn (open-trace-file! "xx")
         (value '(value-triple nil))))