		Search-engine friendly clone of the ACL2 documentation.

Cert.pl

Certifying-simple-books

How to use certify simple ACL2 books, take advantage of parallel builds, and manage the dependency scanner.

Basic Example

Let's use cert.pl to build a simple ACL2 project. Say we have two ACL2 books:

;; inc.lisp            |  ;; prop.lisp
(in-package "ACL2")    |  (in-package "ACL2")
(defun inc (x)         |  (include-book "inc")
  (+ 1 x))             |
                       |  (defthm natp-of-inc
                       |    (implies (natp x)
                       |             (natp (inc x)))

We can now certify either book by just running cert.pl on it. Let's first just build the inc book:

$ cert.pl inc
ACL2 executable is /home/jared/bin/acl2
System books directory is /home/jared/acl2/books/
Making /home/jared/acl2/books/tmp/inc.cert on 25-Oct-2013 21:49:11
Successfully built /home/jared/acl2/books/tmp/inc.cert
-rw-rw-r-- 1 jared logic 378 Oct 25 21:49 inc.cert

If we run ls, we'll now see some new files:

inc.cert, the ACL2 ACL2::certificate for inc.lisp
inc.cert.out, the log for certifying inc; this shows the instructions that were submitted to ACL2, and the output from the certify-book command.
inc.lx64fsl or .fasl or perhaps some other extension, depending on the underlying host Lisp.
Makefile-tmp, a Makefile that cert.pl generated.

We might now run cert.pl to certify the prop book. Since inc is already certified, it only needs to build prop:

$ cert.pl prop
ACL2 executable is /home/jared/bin/acl2
System books directory is /home/jared/acl2/books/
Making /home/jared/acl2/books/tmp/prop.cert on 26-Oct-2013 07:55:16
Successfully built /home/jared/acl2/books/tmp/prop.cert
-rw-rw-r-- 1 jared logic 465 Oct 26 07:55 prop.cert

An ls will now show us many files:

$ ls
inc.cert      inc.lisp     Makefile-tmp  prop.cert.out  prop.lx64fsl
inc.cert.out  inc.lx64fsl  prop.cert     prop.lisp

We can delete the generated files with clean.pl, a companion script of cert.pl:

$ clean.pl
clean.pl: scanning for generated files
clean.pl: found 7 targets (0 seconds)
clean.pl: deleted 7 files (0 seconds)
$ ls
inc.lisp  prop.lisp

If we now tell cert.pl to certify the prop book directly, it will notice that the inc book needs to be certified, and do the right thing:

$ cert.pl prop
ACL2 executable is /home/jared/bin/acl2
System books directory is /home/jared/acl2/books/
Making /home/jared/acl2/books/tmp/inc.cert on 26-Oct-2013 07:59:41
Successfully built /home/jared/acl2/books/tmp/inc.cert
-rw-rw-r-- 1 jared logic 378 Oct 26 07:59 inc.cert
Making /home/jared/acl2/books/tmp/prop.cert on 26-Oct-2013 07:59:42
Successfully built /home/jared/acl2/books/tmp/prop.cert
-rw-rw-r-- 1 jared logic 465 Oct 26 07:59 prop.cert

Useful Features

Multiple Targets

You can tell cert.pl to build multiple top-level books at once, for instance:

$ cert.pl foo bar baz

will try to certify foo.lisp, bar.lisp, and baz.lisp.

File Name Extensions

You don't have to include a .lisp or .cert extension, but if you do, cert.pl will do what you mean. For instance, the following commands are all equivalent:

$ cert.pl foo
$ cert.pl foo.lisp
$ cert.pl foo.cert

The .lisp form can be handy, e.g., you can do:

$ cert.pl *.lisp

Parallel Builds (-j)

You can tell cert.pl to build books in parallel, to take advantage of multi-core processors. The -j switch tells it how many processors you want to use, just like with make. Typically you would want to set -j no higher than the number of cores your machine has available. For instance:

$ cert.pl -j 2 foo    # for a dual-core system
$ cert.pl -j 4 foo    # for a 4-core system
$ cert.pl -j 8 foo    # for an 8-core system

Warning: setting -j too high can cause serious performance problems. If you often use ACL2 on both, say, a 16-core server and a 2-core laptop, then you may sometimes find yourself accidentally telling the laptop to run 16 jobs at once! To avoid this kind of trouble, Jared sets up an alias like this in his .bashrc:

# in the laptop's .bashrc:
alias cj="cert.pl -j 2"

# in the server's .bashrc:
alias cj="cert.pl -j 16"

This way, just running cj will use an appropriate number of cores no matter which system is being used.

Warning: the CPU count is not the only factor to consider when choosing a -j to use. You may also need to consider how much memory your machine has. For instance, on a quad-core laptop you'd like to run 4 jobs at once, but if you only have 8 GB of memory and each job takes 4 GB, then using -j 4 may get you into swapping trouble.

Keep Going (-k)

Like make, cert.pl will ordinarily stop as soon as it fails to build any book.

Occasionally this may not be what you want. You might have made a change that you know will break several books. One way to find out what's broken is to just try to build everything. The default behavior—stopping as soon as anything is broken—will only let you find one broken book at a time.

In this situation, you may want to instead do, e.g.,

$ cert.pl -j 4 top.cert -k

This is identical to make's "keep going" switch.

Prepare (-p)

Sometimes you want to work on a particular book, which you know won't certify (e.g., because you're only part-way through a proof). Before you begin working on the book again, you may want to rebuild any supporting books it depends on. The -p flag lets you do this, e.g.,

$ cert.pl -p mybook

won't try to certify mybook.lisp, but it will try to certify any books that mybook.lisp includes.

Dependency Scanning Limitations

Keep in mind that cert.pl is a dumb Perl script. It's quite easy to fool it using ACL2::macros or other tricks. But you don't even need to get that fancy—a newline will do the trick. For instance, if foo.lisp contains the following, then cert.pl will not think it depends on bar:

(include-book     ;; newline to fool dependency scanner
  "bar")

This is documented behavior that you may rely on.

For instance, sometimes we put multi-line comments in books with performance comparisons or other kinds of examples or testing code. This code might need additional include-books to work. By putting in newlines, we can hide these books from the dependency scanner, to avoid slowing down our build with unnecessary dependencies. For instance:

(defun my-function ...)

#|| ;; this benchmark says my-function is 3x faster than yours:

(include-book           ;; fool dependency scanner
   "your-function")

:q
(time (loop for i fixnum from 1 to 100000 do (my-function ...)))
(time (loop for i fixnum from 1 to 100000 do (your-function ...)))
||#

(defthm my-lemma ...)

You can also trick cert.pl in the other direction, to add additional, unnecessary dependencies. For instance, a macro library might have some unit testing books to try to ensure the macros are behaving correctly. To ensure these tests get run when the library is rebuilt, we might write a top book like this:

(in-package "ACL2")
(include-book "module1")
(include-book "module2")
(include-book "module3")

#|| ;; trick cert.pl into running the unit tests:
(include-book "module1-tests")
(include-book "module2-tests")
(include-book "module3-tests")
||#