Ld-verbose
Determines whether ld prints ``ACL2 Loading ...''
Ld-verbose is an ld special (see ld). The
accessor is (ld-verbose state) and the updater is (set-ld-verbose val
state). Ld-verbose must be t, nil or a string or consp suitable for fmt printing via the ~@ command. The initial
value of ld-verbose is a fmt message that prints the system books
directory.
Note: Ld-verbose has no effect on proofs. See set-gag-mode and
see set-inhibit-output-lst for how to control the size of proof
output.
Before processing the forms in standard-oi, ld may print a
header. The printing of this header is controlled by ld-verbose. If
ld-verbose is nil, no header is printed. If it is t, ld prints the message
ACL2 loading <file>
where <file> is the input channel supplied to ld. A similar
message is printed when ld completes. If ld-verbose is neither
t nor nil then it is presumably a header and is printed with the
~@ fmt directive before ld begins to read and process
forms. In this case the ~@ fmt directive is interpreted in an
environment in which #\b is the system books directory, #\v is the
ACL2 version string, #\l is the level of the current recursion in ld and/or wormhole, and #\c is the connected book directory
(cbd).
