Major Section: IO
See IO for a summary of printing in ACL2. Here we document some advanced ways to control what is printed by ACL2's primary printing routines.
See set-print-base, see set-print-radix, and see set-print-case for
discussions of the most common ways to control what is printed. Indeed,
these are the only ways to control the behavior of princ$ and
prin1$.
The rest of this topic is for advanced users of ACL2. We refer to Common Lisp behavior, as described in any good Common Lisp documentation.
Print-control variables. Set-print-base, set-print-radix,
and set-print-case assign to corresponding so-called ``state
global variables'' 'print-base, 'print-radix, and 'print-case,
which can be accessed using the expressions (@ print-base),
(@ print-radix), and (@ print-case), respectively; see assign. Here
is a table showing all print-control variables, their setters, and their
defaults.
print-base set-print-base 10 print-case set-print-case :upcase print-circle set-print-circle nil [but see remark on print-circle-files, below] print-escape set-print-escape t print-length set-print-length nil print-level set-print-level nil print-lines set-print-lines nil print-pretty set-print-pretty nil print-radix set-print-radix nil print-readably set-print-readably nil print-right-margin set-print-right-margin nil
Each ACL2 print-control variable print-xxx can correspond in function to
Common Lisp variable *PRINT-XXX*. Specifically, the evaluation of forms
(set-print-base t), (set-print-radix t), and (set-print-case t)
affects ACL2 printing functions in much the same way that setting to t
Common Lisp variables *PRINT-BASE*, *PRINT-RADIX*, and
*PRINT-CASE*, respectively, affects Common Lisp printing. The same is
true for print-escape, except that this does not affect princ$ or
prin1$, which correspond to Common Lisp functions princ and
prin1: princ treats *PRINT-ESCAPE* as nil while prin1
treats *PRINT-ESCAPE* as t. Moreover, all print-control variables
not mentioned in this paragraph are set to their defaults in princ$ and
prin1$, as indicated by ACL2 constant *print-control-defaults*,
except that print-readably is set to nil in princ$.
Fmt and its related functions are sensitive to state globals
'print-base, 'print-radix, 'print-case, 'print-escape, and
'print-readably, in analogy with Common Lisp functions that don't fix
*PRINT-ESCAPE* or *PRINT-READABLY*. But the fmt functions do
not respect settings of other print-control variables; for example, they act
as though 'print-circle is nil. Since ACL2 output is produced using
the same underlying print routines as the fmt functions, it also is
insensitive to all print-control variables except for the five above. To
control the print-level and print-length used for producing ACL2 output,
see set-evisc-tuple.
Print-object$ is sensitive to all of the print-control variables.
Remark on print-circle-files: ACL2 typically binds 'print-circle to
t before writing certificate files, or auxiliary files that are
compiled when make-event forms are present in a book, or files in
support of :comp commands. This binding allows for structure
sharing that can keep these files from growing large. However, this behavior
is defeated in GCL (Gnu Common Lisp), because of the small number of indices
n available by default (1024) for the #n= reader macro. For the
files described above, what actually happens is that 'print-circle is
bound to the value of 'print-circle-files, which by default is t
unless the underlying Lisp is GCL, in which case it is set to nil.
See assign for how to set state globals such as 'print-circle-files.
For example, if you build GCL with a larger number of #n= indices
available, you may wish to restore the print-circle behavior for
certificate files by following these instructions from Camm Maguire:
This can trivially be revised to any larger constant by editing the following line of read.d and recompiling:
#ifndef SHARP_EQ_CONTEXT_SIZE
#define SHARP_EQ_CONTEXT_SIZE 500
#endif
End of Remark.
Evaluate (reset-print-control) to restore all print-control variables to
their original settings, as stored in constant *print-control-defaults*.
(Remark for those using ACL2 built on Gnu Common Lisp (GCL) versions that are
non-ANSI, which as of October 2008 is all GCL versions recommended for ACL2:
Note that Common Lisp variables *PRINT-LINES*, *PRINT-MISER-WIDTH*,
*PRINT-READABLY*, *PRINT-PPRINT-DISPATCH*, and
*PRINT-RIGHT-MARGIN* do not have any effect for such GCL versions.)
