ACL2-system-feature-dependencies
Automatically forcing recertification when changes in the ACL2 sources
would invalidate a certificate.
In principle, every time the ACL2 system changes, all books should
be recertified. However, in practice many users don't do this because the ACL2
system is updated frequently and it is time-consuming to rebuild all the
community books. But sometimes a change to the ACL2 system makes certain books
no longer work correctly until they are recertified. For example, the book
system/apply/apply-prim uses the value of
*first-order-like-terms-and-out-arities*, a constant defined by the ACL2
system, in a make-event form in order to define apply$-prim-meta-fn-ev.
If the value of that constant changes, that book should be recertified;
otherwise, books that depend on it might fail to certify.
The GNUMakefile provided with the ACL2 community books provides a
mechanism to force certain books to be recertified when the values of constants
built into the ACL2 system change. To fix apply-prim using this
mechanism, we add a comment to the book:
; (depends-on "build/first-order-like-terms-and-out-arities.certdep" :dir :system)
This forces apply-prim to be recertified if that file changes. We
arrange for this file to change by running ACL2 at the start of each invocation
of the community books' GNUMakefile and comparing the value of
*first-order-like-terms-and-out-arities* to the object read from
build/first-order-like-terms-and-out-arities.certdep. If those objects
differ, then the current *first-order-like-terms-and-out-arities* is
written to that file, which then forces apply-prim to be recertified.
It is fairly easy to add dependencies on other ACL2 features: simply add a
new invocation of write-file-if-obj-differs to
build/cert_features.lsp, similar to the ones that already exist there.
For example, the one used in the example above is:
(write-file-if-obj-differs "first-order-like-terms-and-out-arities.certdep"
*first-order-like-terms-and-out-arities*
state)
Then add dependencies using depends-on comments in the books that
depend on the current value of that constant.
The cert.pl build system by itself does not update these files, which means
that Makefiles that use cert.pl will not support this feature unless they run
the cert_features.lsp script on startup, like books/GNUMakefile does.
A workaround is to invoke books/GNUMakefile after any rebuild of ACL2,
before using cert.pl alone or using a separate Makefile:
cd acl2/books
make build/Makefile-features
Cert.pl and cert.pl-generated Makefiles will arrange for files
build/%.certdep to be created if they do not exist, so that books that
depend on them can still be certified using cert.pl alone.
Cert.pl also makes every certificate depend on two special certdep files:
build/acl2-version.certdep and build/universal-dependency.certdep.
The former is updated by cert_features.lsp like the others, containing the
current ACL2 version string; this forces all books to be recertified when the
ACL2 version number changes. The latter, unlike the others, is stored in the
ACL2 git repository. It may be updated by ACL2 maintainers to force all books
to be recertified when they make other changes that require this, or by
community members who notice that such a change has been made without a
corresponding update.
