		Search-engine friendly clone of the ACL2 documentation.

Calling-ld-in-bad-contexts

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:

when calling ld inside progn! unless state global ld-okp is first set to t, e.g., using (assign ld-okp t); also,
when calling ld while inside raw Lisp, e.g., when loading a compiled file during an invocation of include-book.

Consider for example the following book, where file const.lsp contains the single form (defconst *foo* '(a b)) after its initial in-package form.

(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 book, where ld is called in the body of a function; the two conditions above do not prohibit this.

(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 (foo state), and then evaluate calls of h.