Bookdata
Write small files with meta-data about certified books
ACL2 provides a primitive capability for writing out a file of
metadata associated with a book. This information might be useful, for
example, in building a database that allows you to search for name conflicts.
See community-books directory books/tools/book-conflicts/ for an
application of this capability by Dave Greve. If you use this capability and
have ideas for enhancing it, please feel free to send them to the ACL2
developers.
If the book has the name BK, then the output file is named
BK__bookdata.out. That file is generated in the same directory as
BK, by certifying BK when state global 'write-bookdata
has a non-nil value, for example as follows.
(assign write-bookdata t)
(certify-book "BK" ...)
Alternatively, one may set environment variable ACL2_WRITE_BOOKDATA to
any non-empty value to cause BK__bookdata.out to be written, with one
exception, namely: when the value of state global write-bookdata is
:never.
The resulting file will contain a single form of the following shape,
although not necessarily in the following order, according to the description
that follows below.
("...BK.lisp"
:PKGS pkgs-val
:BOOKS book-val
:PORT-BOOKS port-book-val
:CONSTS consts-val
:PORT-CONSTS port-consts-val
:FNS fns-val
:PORT-FNS port-fns-val
:LABELS labels-val
:PORT-LABELS port-labels-val
:MACROS macros-val
:PORT-MACROS port-macros-val
:STOBJS stobjs-val
:PORT-STOBJS port-stobjs-val
:THEORIES theories-val
:PORT-THEORIES port-theories-val
:THMS thms-val
:PORT-THMS port-thms-val
)
The first entry in the form will always be the full-book-name of the
certified book, BK, possibly in sysfile format.
Subsequent values in the form are based on events introduced by
including BK. For various values of xxx as described below,
port-xxx-val is a list of values corresponding to events introduced in the certification world for BK (see portcullis), and xxx-val is a list of values corresponding to
events introduced non-locally by BK. These lists include
only ``top-level'' events, not those that are introduced by a book included
either in BK or its certification world.
Pkgs-val is a list of names of packages introduced in the
certification world (at the top level, not in an included book). Note that no
packages are introduced in a book itself, so no distinction is made between
pkgs-val and port-pkgs-val. Both port-book-val and
book-val are lists of full-book-names of included books. The
values associated with the other keywords are, themselves, association
lists (see alistp) such that each key is a package name, which is
associated with a list of symbol-names for symbols in that package that
are introduced for that keyword. For example, fns-val may be the
alist
(("ACL2" "F1" "F2")
("MY-PKG" "G1" "G2"))
if the function symbols introduced in the book are F1 and F2 in
the "ACL2" package, as well as G1 and G2 in the
"MY-PKG" package.
We next explain what kinds of symbols are introduced for each keyword
:xxx. Each such symbol would be associated with either the keyword
:port-xxx or the keyword :xxx depending respectively on whether the
symbol is introduced at the top level of the certification world for BK
or BK itself.
- :CONSTS
- constant symbol introduced by defconst
- :FNS
- function symbol: introduced by defun, defuns, or defchoose; or
constrained (by an encapsulate event)
- :LABELS
- symbol introduced by deflabel
- :MACROS
- macro name introduced by defmacro
- :STOBJS
- stobj name introduced by defstobj or defabsstobj
- :THEORIES
- theory name introduced by deftheory
- :THMS
- theorem name, which may be introduced by defthm or a macro call
expanding to a call of defthm, such as see defequiv or
defaxiom; but may be introduced by defpkg, for example, with
name "MYPKG-PACKAGE" if the package name is "MYPKG"
Our hope is that people in the ACL2 community will generate and use this
data to improve the ACL2 community-books. Here is an example
illustrating how to generate bookdata files for those books as a byproduct of
a regression run. Below, we write {DIR} as an abbreviation for the ACL2
sources directory, and assume that this command is run from that directory.
Of course, you may wish to use make options like -j 8 and make
variable settings like ACL2={DIR}/my-saved_acl2; see books-certification for details.
make regression-fresh \
ACL2_CUSTOMIZATION={DIR}/acl2-customization-files/bookdata.lisp
