LD-VERBOSE

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