ld in inappropriate contexts
Major Section: LD
The macro ld was designed to be called directly in the top-level ACL2
loop, although there may be a few occasions for calling it from functions.
ACL2 cannot cope with invocations of ld during the process of loading a
compiled file for a book, so this is an error.
To see how that can happen, consider the following book, where file
const.lsp contains the single form (defconst *foo* '(a b)).
(in-package "ACL2") (defttag t) (progn! (ld "const.lsp"))An attempt to certify this book will cause an error, but that particular error can be avoided, as discussed below. If the book is certified, however, with production of a corresponding compiled file (which is the default behavior for
certify-book), then any subsequent call of
include-book that loads this compiled file will cause an error.
Again, this error is necessary because of how ACL2 is designed; specifically,
this ld call would interfere with tracking of constant definitions when
loading the compiled file for the book.Because including such a book (with a compiled file) causes an error, then as a courtesy to the user, ACL2 arranges that the certification will fail (thus avoiding a surprise later when trying to include the book). The error in that case will look as follows.
ACL2 Error in LD: It is illegal to call LD in this context. See DOC calling-ld-in-bad-contexts.If you really think it is OK to avoid this error, you can get around it by setting state global variable
ld-okp to t: (assign ld-okp t).
You can then certify the book in the example above, but you will still not be
able to include it with a compiled file.
