Preliminaries
Where to find cert.pl, how to set up your environment before
using it, and the supporting software you'll need.
Prerequisite Software
We assume that you have a basic, sensible Unix environment; Windows users
should see cert-pl-on-windows.
We assume that you have GNU
Make installed and available as make in your $PATH. Some
operating systems (e.g., FreeBSD) use a non-GNU make by default. You can check
your copy by running make --version; it should say something like "GNU
Make 3.81."
We assume you have Perl installed, and
that your perl executable is in your $PATH.
We assume you have ACL2
or one of its variants like ACL2(p) or ACL2(r) installed, and that
you know how to launch ACL2—usually with a script named saved_acl2
or similar.
We assume you have a copy of the ACL2 Community Books for your
version of ACL2; they are usually put in acl2/books.
Adding cert.pl to your $PATH
To make running cert.pl more convenient, it's a good idea to have it
accessible in your $PATH. The cert.pl script and related tools like
critpath.pl and clean.pl are found in the build directory of the
Community Books.
- We recommend that you edit your startup scripts (e.g., .bashrc or
similar) to add acl2/books/build to your $PATH.
- You could alternately set up symlinks to acl2/books/build/cert.pl and
the other scripts from a directory that is already in your path, for instance,
~/bin is commonly used for this.
To test that this is working, you can run cert.pl --help. It should
print a usage message, e.g.,:
$ cert.pl --help
cert.pl: Automatic dependency analysis for certifying ACL2 books.
Usage:
perl cert.pl <options, targets>
...
Helping cert.pl find ACL2 and the community books
It is convenient for cert.pl to "just know" where your copy of ACL2
is located.
A third option is to tell cert.pl explicitly which ACL2 you would like
it to use, by using the --acl2 or -a flag:
$ cert.pl -a /path/to/acl2/saved_acl2 [...]
This takes precedence over both the environment variable and any acl2
in your $PATH.
To ensure that cert.pl is properly detecting your copy of ACL2, you can
run cert.pl with no arguments. The output should look something like
this:
$ cert.pl
ACL2 executable is /home/jared/acl2/saved_acl2
System books directory is /home/jared/acl2/books
...
Please check that both the ACL2 executable and your books
directory are correctly detected. If the books directory is not correct, you
may need to help cert.pl find it by setting another environment variable,
e.g.,
export ACL2_SYSTEM_BOOKS=/home/jared/acl2/books
Alternatively, you can tell cert.pl explicitly which books directory
you would like it to use, by using the --acl2-books or -b flag:
$ cert.pl -b /home/jared/acl2/books [...]
This takes precedence over the environment variable.
At this point, cert.pl should be configured properly and ready to
use.
Incidentally, if cert.pl cannot determine the location of the books
directory from one of the above two directives, it will first try to find a
books directory alongside the ACL2 executable. If this fails, it will run
the ACL2 executable and ask it for the value of the expression
(system-books-dir state). If the response it receives does not point to a
directory that exists on the filesystem, cert.pl finally chooses the
parent directory of its own location.
Subtopics
- Cert-pl-on-windows
- Special notes about using cert.pl on Windows.
