ld prints ``ACL2 Loading ...''
Major Section: MISCELLANEOUS
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 ACL2 version number, ld level and
connected book directory.
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
#\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).
