Cert_param
Restricting and modifying community-books
certification using make.
You can restrict the books to be certified using make
by adding a stylized ``cert_param:'' comment. For example, suppose that
you include the following comment in your book or in a corresponding
.acl2 file (see pre-certify-book-commands).
; cert_param: (ccl-only)
Then your make command will only certify that book if your host Lisp
is CCL. Moreover, if your host Lisp is not CCL, then make will skip not
only the certification of that book but will also not attempt to certify any
book that includes it (and recursively).
The syntax for cert_param comments is as follows, where the whitespace
is optional, and each entry without an '=' is just set to 1, that is, it
is activated as described below.
; cert_param: ( foo = bar , baz = 1 , bla )
The meaning of an activated cert_param is generally clear from its
name, as follows. Additional cert_param values might be supported in the
future; you can browse community-books file build/cert.pl for
additional supported values. The acl2x, acl2xskip, and
reloc_stub values affect only the book itself, not books that include it.
However, the other values affect not only the certification of the indicated
book but also apply to all books that include it (and recursively).
- acl2x: use two-pass certification (see set-write-ACL2x)
- acl2xskip: use skip-proofs during two-pass certification
- ansi-only: only certify when the host Lisp is an ANSI Common
Lisp (hence, not an older version of GCL)
- ccl-only: only certify when the host Lisp is CCL
- non-acl2r: only certify when the real numbers are NOT
supported, i.e., when NOT using ACL2(r)
- non-acl2p: only certify when ACL2::parallelism is NOT
supported, i.e., when NOT using ACL2(p)
- non-allegro: only certify when the host Lisp is NOT Allegro CL
- non-cmucl: only certify when the host Lisp is NOT cmucl
- non-gcl: only certify when the host Lisp is NOT gcl
- non-lispworks: only certify when the host Lisp is NOT LispWorks
- non-sbcl: only certify when the host Lisp is NOT sbcl
- pcert: use provisional certification (see ACL2::provisional-certification)
- reloc-stub: print a suitable ``relocation stub'' warning
- uses-abc: only certify when the external equivalence/model-checking
tool ABC is available
- uses-acl2r: only certify when the real numbers are supported,
i.e., with ACL2(r)
- uses-glucose: only certify when Glucose (a SAT solver) is
available
- uses-ipasir: only certify when Ipasir (a simple C interface to
incremental SAT solvers) is available
- uses-smtlink: only certify when Smtlink (see smt::smtlink) is
available
- uses-stp: only certify when STP (an SMT solver available here) is available (to suppress the use
of STP, even when an executable for it seems to be available, set environment
variable ACL2_DONT_USE_STP to any non-empty value)
- uses-quicklisp: only certify when quicklisp is available
- uses-cpp: only certify when cpp is available. See c$::preprocessing.
In addition to the non-acl2p cert_param that excludes books from
ACL2(p) builds (see ACL2::parallelism), there is also the related ACL2::non-parallel-book utility for turning off waterfall-parallelism.
