ldprints ``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
nil or a string or
consp suitable for
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
ld may print a header.
The printing of this header is controlled by
nil, no header is printed. If it is
ld prints the
ACL2 loading <file>where
<file>is the input channel supplied to
ld. A similar message is printed when
nilthen it is presumably a header and is printed with the
ldbegins to read and process forms. In this case the
fmtdirective is interpreted in an environment in which
#\vis the ACL2 version string,
#\lis the level of the current recursion in
#\cis the connected book directory