Errors caused by calling ld in inappropriate contexts
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 that is an error.
Specifically: ACL2 will cause an error in the following two circumstances:
Consider for example the following book, where file
(in-package "ACL2") (defttag t) (progn! (ld "const.lsp"))
An attempt to certify this book as follows
(certify-book "const-wrapper" 0 t :ttags :all)
will cause an error:
ACL2 Error in LD: It is illegal to call LD in this context. See :DOC calling-ld-in-bad-contexts.
However, that error can be avoided by expanding the progn! call as follows.
(progn! (assign ld-okp t) (ld "const.lsp"))
Now certification succeeds; however, any subsequent call of include-book will fail to load the compiled file for the book. Again, that is necessary because of how ACL2 is designed; in this case, the ld call would interfere with tracking of constant definitions when loading the compiled file for the book. To avoid warnings about loading compiled files, either certify the book without creating a compiled file or else include the book without loading the compiled file; see certify-book and include-book.
Note that it is legal to put a definition such as the following into a
(defun foo (state) (declare (xargs :guard t :stobjs state :mode :program)) (ld '((defun h (x) x)) :ld-user-stobjs-modified-warning t))
One can then include the book, evaluate