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.
By default, ACL2's certify-book command does not allow your
books to use unsafe features that can easily lead to unsoundness. For
instance, your book may not skip proofs, add arbitrary axioms, or use trust
tags to smash raw Lisp definitions.
However, these restrictions can be lifted by giving certify-book
options such as :skip-proofs-okp t and :ttags :all. In such cases
the resulting certificate is annotated to reflect that it is less trustworthy
and include-book may print warnings about the book or even reject it
when given suitable options. See certify-book and include-book
for details.
By default cert.pl will similarly disallow these unsafe features. More
precisely, the default command it uses to certify books is looks like this:
(certify-book "foo" ? t)
If you want to permit your book to use trust tags, skipped proofs, etc.,
you'll need to tell cert.pl that you want to give different arguments to
certify-book.
You can do this on a per-book or per-directory basis by adding a special
comment into the corresponding .acl2 file. If you don't know what an
.acl2 file is, see pre-certify-book-commands.
Example: to allow all trust tags, you could use a comment like this:
; cert-flags: ? t :ttags :all
Example: to allow trust tags and skip-proofs, you could use:
; cert-flags: ? t :ttags :all :skip-proofs-okp t
Rules of thumb:
- Your cert-flags should probably start with ? t.
- Even if you have a long list of :ttags, keep them on one line. A
dumb perl script is reading this, after all.
- You should probably not use arguments like :acl2x,
:write-port, or :pcert.
