Cert.pl
cert.pl is a mature, user-friendly, industrial-strength tool for
certifying ACL2 books.
Introduction
For "pure" ACL2 projects—even large ones—cert.pl will let
you to certify any book, whenever you like, without writing any Makefiles. If
your book includes supporting books that aren't certified, cert.pl will
rebuild exactly the necessary books, in parallel, even if they're in other
directories.
For more complex projects, where (say) besides just certifying ACL2 books
you also need to build large C libraries and certify ACL2 books that you're
generating on the fly, cert.pl can automate the dependency tracking for
your regular ACL2 books, and you can easily integrate this information into
your project's Makefile.
For industrial-scale projects, cert.pl has many features that you may
find valuable. For instance:
- ACL2 features like packages, ttags, add-include-book-dir, and save-exec images are properly supported. In particular,
(.port) files (see ACL2::portcullis) of included books are loaded
automatically before certification; see pre-certify-book-commands.
- Parallel builds (as in make -j) are well-supported. For the truly
adventurous, you may even be able to distribute your build over a cluster.
- Tools like critpath.pl can help you to more effectively optimize your
build time for multi-core environments.
- Dependency scanning is cached for better performance on NFS file
systems.
- Ifdef/ifndef constructs are supported for conditional build features -- see
ACL2::ifdef, ACL2::ifndef, ACL2::ifdef-define, and ACL2::ifdef-undefine.
cert.pl was originally developed in 2008 by Sol Swords at Centaur
Technology, and has been actively used and improved since then. It is now
distributed in the build directory of the Community Books, and is today
the main tool behind books/GNUmakefile.
Using cert.pl
This documentation is really a tutorial, not a reference. We
recommend that you read the topics in order. Also see ACL2::books-certification for additional information on how to automate the
certification of the community-books, and for more details, execute the
following command in the shell.
<path_to_acl2>/books/build/cert.pl --help
We assume basic familiarity with a Unix environment, e.g., we expect that
you know how to edit your startup scripts to set up a PATH, create
symbolic links, etc.
Subtopics
- Cert_param
- Restricting and modifying community-books
certification using make.
- Preliminaries
- Where to find cert.pl, how to set up your environment before
using it, and the supporting software you'll need.
- Using-extended-ACL2-images
- (Advanced) how to get cert.pl to use save-exec images
to certify parts of your project.
- Distributed-builds
- (Advanced) how to distribute ACL2 book building over a cluster
of machines.
- Certifying-simple-books
- How to use certify simple ACL2 books, take advantage of parallel
builds, and manage the dependency scanner.
- Pre-certify-book-commands
- How to add commands to be executed before calling certify-book. You'll need this to use ACL2 features like defpkg and
add-include-book-dir.
- ACL2-system-feature-dependencies
- Automatically forcing recertification when changes in the ACL2 sources
would invalidate a certificate.
- Static-makefiles
- How to use cert.pl within a larger Makefile that needs to know
how to build non-ACL2 files (e.g., C libraries) or dynamically generated ACL2
books.
- Optimizing-build-time
- How to use critpath.pl to profile your build, so that you can
focus your efforts on speeding up the most critical parts.
- Raw-lisp-and-other-dependencies
- How to use depends-on to tell cert.pl about additional,
non-Lisp files that your books depend on.
- Custom-certify-book-commands
- How to use cert-flags to control the options that will be passed
to the certify-book command. You'll need this to allow the use of trust tags, skip-proofs, defaxioms,
and so forth.
- Include-events
- A build-system-supported mechanism to include the events from a
book as a progn or encapsulate.
- Ifdef
- Run some events only if an environment variable is defined and nonempty,
with build system support.
- Ifdef-define
- Define an environment variable for use with ifdef and ifndef.
- Ifndef
- Run some events only if an environment variable is undefined or empty,
with build system support.
- Ifdef-undefine
- Undefine an environment variable for use with ifdef and ifndef.
- Ifdef-undefine!
- Undefine an environment variable for use with ifdef and ifndef, persistent across include-book.
- Ifdef-define!
- Define an environment variable for use with ifdef and ifndef, whose effect persists across include-books.
- Include-src-events
- Like include-events but allows an arbitrary file extension.
