Major Section: IO
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 ld to redirect ACL2
output to a file, other than the printing of the prompt (which continues to
go to the terminal).
There are two ld specials that control output from the ld command:
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
"tmp.out". The following command opens a character output channel to
to the file "tmp.out" and redirects proof output to that channel, i.e.,
to file "tmp.out".
(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
"tmp.lisp", and output
will be redirected to file "tmp.out". (The use of
:ld-pre-eval-print t is optional; see ld.)
(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)
