• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
      • Miscellaneous
      • Output-controls
        • With-output
        • Summary
        • Set-inhibit-output-lst
        • Set-gag-mode
        • Goal-spec
        • Set-warnings-as-errors
        • Saving-event-data
        • Pso
        • Finalize-event-user
        • Set-inhibit-er
        • Checkpoint-list
        • Set-inhibit-warnings
        • Get-event-data
        • Set-inhibited-summary-types
        • Set-print-clause-ids
        • Set-let*-abstractionp
        • Gag-mode
        • Initialize-event-user
        • Set-raw-proof-format
        • Checkpoint-list-pretty
        • Psof
        • Set-raw-warning-format
        • Toggle-inhibit-warning
        • Toggle-inhibit-er
        • Warnings
        • Show-checkpoint-list
        • Wof
          • Psog
          • Checkpoint-info-list
          • Pso!
          • Toggle-inhibit-warning!
          • Set-duplicate-keys-action!
          • Toggle-inhibit-er!
          • Set-inhibit-warnings!
          • Set-inhibit-er!
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Output-controls
    • Io

    Wof

    Direct standard output and proofs output to a file

    Example Form:
    (wof "tmp" (pso)) ; same as (psof "tmp")
    
    General Form:
    (wof filename form)

    where filename is a writable filename and form is any form that evaluates to an error triple (see programming-with-state), that is, a multiple value of the form (mv erp val state). All output to channels standard-co and proofs-co will be directed to the indicated file. It is acceptable to replace filename with (quote filename).

    For a general discussion about redirection of output to a file, see output-to-file.

    Note that so-called comment-window output (see cw and see observation-cw) is not redirected by wof to a file, nor is printing from a wormhole.