Include-raw
A better way to load raw Lisp code than directly using progn!
or set-raw-mode.
Sometimes you want to include raw Lisp code in an ACL2 book to
achieve better performance or do fancy things like connect to external
programs. With trust tags, you can do this.
Unfortunately, the built-in mechanisms (progn! and set-raw-mode)
have some portability problems related to compilation, file paths, read tables,
non-ACL2 objects, and so on; see below for some examples.
Using Include-Raw
Using include-raw solves some of these problems. Here are some
examples of how to use it:
(include-book "tools/include-raw" :dir :system)
(defttag :my-ttag) ; required before calling include-raw
(include-raw "my-raw-lisp-file.lsp")
(include-raw "another-raw-lisp-file.lsp"
:do-not-compile t)
When you use include-raw, your raw Lisp code goes into a separate file.
If your book is named foo.lisp, then this file should typically be named
foo-raw.lsp. Why?
- The .lsp extension helps build systems realize that the raw file is
not a proper ACL2 book and should not be certified.
- The -raw part helps to avoid running into a problem: on most Lisps,
compiling foo.lisp or foo.lsp results in the same compiled file,
e.g., foo.fasl or similar. So it is a mistake to use the same base name
for a raw Lisp file with a .lsp extension and an ACL2 book with .lisp
extension.
The path of the raw Lisp file must be given relative to the book containing
the include-raw form. Typically we put the raw Lisp file in the same
directory as its book.
By default, the raw Lisp file will be compiled and loaded when the
containing book is certified. When including the book, the compiled file will
be loaded if possible, otherwise the original file will be loaded instead. By
default, if either compilation or loading fails, an error will occur.
Benefits
Keeping raw Lisp code in a separate file means you can use various kinds of
Lisp syntax that are not allowed in ACL2. Otherwise you have to jump through
awful hoops like having to interning the names of functions like
ccl::static-cons that you want to call. It's also nice to be able to use
floats, etc.
Using include-raw instead of something like load after a
set-raw-mode means you get predictable path behavior. Otherwise, unless
you go out of your way to save the cbd with a make-event, you can
end up with include-book failing when you try to load your book from
other directories.
Using include-raw means that by default your definitions get compiled,
which can help to avoid stack overflows on some Lisps that don't compile
definitions automatically. This isn't the case for definitions submitted
inside a progn!. It also helps defend against the comp command
undoing your raw Lisp definitions.
Optional Arguments
The optional keywords :on-compile-fail and/or :on-load-fail may be
used to suppress the error for failed compilation or loading, respectively;
their argument is a term which will be evaluated in lieu of producing an error.
When evaluating this term, the variable condition is bound to a value
describing the failure; see Common Lisp documentation on handler-case.
Note: for non-ansi-compliant Common Lisp implementations, such as GCL 2.6.*, no
such error handling is provided. Here is an example:
(include-raw "a-raw-lisp-file.lsp"
:on-compile-fail
(format t "Compilation failed with message ~a~%"
condition)
:on-load-fail
(cw "Oh well, the load failed~%")
:host-readtable t)
The optional keyword :do-not-compile may be used to suppress
compilation. In this case, during book certification the file will just be
loaded using load. Similarly, during include-book we will only load
the lisp file, and not try to load a compiled file.
The optional keyword :host-readtable may be used to make sure that the
original *readtable* for this Lisp is being used, instead of the ACL2
readtable, while reading the file. This may sometimes be necessary to avoid
differences between ACL2's reader and what raw Lisp code is expecting.
