PRINT-CONTROL

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 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 and set-print-case assign to corresponding so-called ``state global variables'' 'print-base and 'print-case, which can be accessed using the expressions (@ print-base) 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) and (set-print-case t) affects ACL2 printing functions in much the same way that setting to t Common Lisp variables *PRINT-BASE* 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-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 four 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

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.)