• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
      • Break-rewrite
      • Proof-builder
      • Accumulated-persistence
      • Cgen
      • Proof-tree
      • Forward-chaining-reports
      • Print-gv
      • Dmr
      • Splitter
      • Guard-debug
      • Set-debugger-enable
      • Redo-flat
      • Time-tracker
      • Set-check-invariant-risk
      • Removable-runes
      • Efficiency
      • Tail-biting
      • Failed-forcing
      • Sneaky
      • Invariant-risk
      • Failure
      • Measure-debug
      • Dead-events
      • Remove-hyps
      • Type-prescription-debugging
      • Pstack
      • Set-register-invariant-risk
      • Trace
        • Trace$
        • Wet
        • Trace!
        • Break-on-error
        • Set-trace-evisc-tuple
        • Untrace$
        • Open-trace-file
        • Open-trace-file!
        • Close-trace-file
        • 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
      • Testing-utilities
      • Math
    • Trace

    Close-trace-file

    Stop redirecting trace output to a file

    General Form:
    (close-trace-file) ; trace output is no longer redirected to a file

    Output from trace$ normally goes to the screen, or more precisely, standard-co. It can be redirected to a file; see open-trace-file. Use close-trace-file to redirect trace output to standard-co.