*standard-co*
The ACL2 analogue of CLTL's *standard-output*
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.
