Raw-lisp-and-other-dependencies
How to use depends-on to tell cert.pl about additional,
non-Lisp files that your books depend on.
Some ACL2 books load extra files in unusual ways. For
instance,
- An ACL2 book for verifying a Java program might use ACL2::io
routines to load encrypt.java, or
- An ACL2 book with trust tags might use ACL2::include-raw to load in
some extra raw Lisp file named server-raw.lsp.
In either case, since these extra files are not being loaded using include-book, cert.pl will not automatically know that these book depend
on encrypt.java and server-raw.lsp.
To tell cert.pl about additional dependencies, you may put a special
depends-on comment in your book. For the Java program we might write
something like this:
; (depends-on "encrypt.java")
(defconsts (*java-file* state)
(read-java-program "encrypt.java"))
Whereas for the server, you could write, e.g.,
; (depends-on "server-raw.lsp")
(include-raw "server-raw.lsp")
This dependency mechanism is good enough to handle situations where you are
directly reading in these source or data files. However, it is not
general enough to handle the situations where the file you are reading needs to
be rebuilt.
For instance, suppose that our Java book doesn't verify a source code file
like encrypt.java, but instead verifies the output of the Java compiler,
i.e., encrypt.class. Normally we would need to build encrypt.class
whenever encrypt.java is updated, by running a command like
$ javac encrypt.java
We can still use a depends-on comment to tell cert.pl that our
ACL2 book depends on encrypt.class, e.g.,
; (depends-on "encrypt.class")
(defconsts (*class-file* state)
(read-java-class-file "encrypt.class"))
This is better than nothing. cert.pl will at least know it needs to
recertify our ACL2 book if the .class file changes. However, there's no
way to tell cert.pl that this .class file also depends on
encrypt.java, so editing encrypt.java won't be enough to trigger a
recertification.
When your project gets to this point—needing a build system that can
deal with both ACL2 books and other kinds of files—you have exceeded the
ability of cert.pl as a purely standalone tool. It now becomes a tool
to help you write a Makefile for your whole project.
