the ACL2 analogue of CLTL's *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.