*standard-output*
Major Section: IO
The value of the ACL2 constant *standard-co* is an open character
output channel that is synonymous to Common Lisp's
*standard-output*.
ACL2 character output to *standard-co* will go to the stream named
by Common Lisp's *standard-output*. That is, by changing the
setting of *standard-output* in raw Common Lisp you can change the
actual destination of ACL2 output on the channel named by
*standard-co*. Observe that this happens without changing the
logical value of *standard-co* (which is some channel symbol).
Changing the setting of *standard-output* in raw Common Lisp
essentially just changes the map that relates ACL2 to the physical
world of terminals, files, etc.
To see the value of this observation, consider the following.
Suppose you write an ACL2 function which does character output to
the constant channel *standard-co*. During testing you see that the
output actually goes to your terminal. Can you use the function to
output to a file? Yes, if you are willing to do a little work in
raw Common Lisp: open a stream to the file in question, set
*standard-output* to that stream, call your ACL2 function, and then
close the stream and restore *standard-output* to its nominal value.
Similar observations can be made about the two ACL2 input channels,
*standard-oi* and *standard-ci*, which are analogues of
*standard-input*.
Another reason you might have for wanting to change the actual
streams associated with *standard-oi* and *standard-co* is to drive
the ACL2 top-level loop, ld, on alternative input and output
streams. This end can be accomplished easily within ACL2 by either
calling ld on the desired channels or file names or by resetting the
ACL2 state global variables 'standard-oi and 'standard-co which are
used by ld. See standard-oi and see standard-co.
