Redirecting output to a file

For a general discussion of ACL2 input/output and of the ACL2
read-eval-print loop, see io and see ld (respectively). Here we
use an example to illustrate how to use some of the options provided by

There are two `proofs-co` for proof output and `standard-co` for other
output. The following example shows how to use these to redirect output to a
file

(mv-let (chan state) (open-output-channel "tmp.out" :character state) (set-proofs-co chan state))

Next, we redirect standard output to that same channel.

(set-standard-co (proofs-co state) state)

Now we can load an input file, in this case file

(ld "tmp.lisp" :ld-pre-eval-print t)

Having completed our load operation, we restore both proof output and standard output to the terminal, as follows.

(set-standard-co *standard-co* state) (close-output-channel (proofs-co state) state) (set-proofs-co *standard-co* state)

The following variant of the above example shows how to redirect output as
above except without changing the global settings of the two `ld`
specials, `proofs-co` and `standard-co`. This approach uses a
notion of ``global variables'' stored in the ACL2 state; see assign and see @.

(mv-let (chan state) (open-output-channel "tmp.out" :character state) (assign tmp-channel chan)) (ld "tmp.lisp" :ld-pre-eval-print t :proofs-co (@ tmp-channel) :standard-co (@ tmp-channel)) (close-output-channel (@ tmp-channel) state)