• 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
        • Theories
        • Rule-classes
        • Proof-builder
        • Recursion-and-induction
        • Hons-and-memoization
        • Events
        • Parallelism
        • History
        • Programming
        • Operational-semantics
        • Real
        • Start-here
        • 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
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Trace

      Open-trace-file

      Redirect trace output to a file

      Example:
      (open-trace-file "foo") ; trace output will go to file foo
      
      General Form:
      (open-trace-file filename) ; trace output will go to file filename

      Output from trace$ normally goes to the screen, i.e., standard-co. But it can be redirected to a file as shown above. See close-trace-file for how to send trace output back to the screen.

      Open-trace-file does not work as would reasonably be expected during make-event expansion. Use open-trace-file! instead within make-event.