Print-control
Advanced controls of ACL2 printing
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-radix, set-print-base, set-print-radix, and 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$.
See set-fmt-hard-right-margin for how to set the right margin for
prover output and, more generally, output from formatted printing
functions (see fmt). Note that set-print-right-margin, mentioned
below, does not affect such printing.
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. Also see set-print-base-radix.
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$ and print-object$-preserving-case are sensitive
to the values of all of the print-control variables except for
'print-escape.
Evaluate (reset-print-control) to restore all print-control variables
to their original settings, as stored in constant
*print-control-defaults*.
(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. End of Remark.)
(Remark for those using ACL2 built on CLtL1 (non-ANSI) Gnu Common
Lisp (GCL): 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.)
Subtopics
- Plev
- Easy-to-use functions for controlling the printer.
