Set-write-ACL2x
Cause certify-book to write out a .acl2x file
Example Forms:
(set-write-acl2x nil state)
(set-write-acl2x t state)
(set-write-acl2x '(nil) state) ; same as just above, but allow inclusion of
; uncertified books during certify-book
(set-write-acl2x '(t) state)
(set-write-acl2x '(include-book-with-locals) state)
General Form:
(set-write-acl2x val state)
where val evaluates to t, nil, or a one-element list whose
element is a legal value for the global 'ld-skip-proofsp; see ld-skip-proofsp. The value returned is an error triple, which in the
non-error case is (mv nil v state), where v is the value of val
and state is the result of updating the input state by assigning
state global 'write-acl2x the value v.
The command (set-write-acl2x val state) assigns the value of val
to the state global variable 'write-acl2x, affecting whether or
not certify-book writes out a file with extension acl2x, called a
``.acl2x file'' and pronounced ``dot-acl2x file''. Such a file is read
or written by certify-book when it is supplied with keyword argument
:acl2x t. By default, such a call of certify-book reads a
.acl2x file; but if the value of state global variable 'write-acl2x
is not nil, then certify-book writes a .acl2x file (in which
case it is illegal to specify a non-nil value for certify-book
keyword argument :pcert). Consider for example (certify-book "foo"
0 nil :acl2x t). By default, this command reads file foo.acl2x, which
supplies replacements for some forms in foo.lisp, as described later
below. But if the value of state global 'write-acl2x is not nil,
then instead, this certify-book command writes such a file
foo.acl2x.
Before we discuss the function of .acl2x files, we first explain more
about how a non-nil value of state global 'write-acl2x
affects the behavior of a command (certify-book ... :acl2x t ...). A
significant effect on the behavior is that after processing events in the
given book, ACL2 writes out a .acl2x file and then returns, skipping the
other subsequent actions typically performed by certify-book: a local-incompatibility check, writing of a certificate file, and
possibly compilation. Another effect is that proofs may be skipped
when processing events assuming that the certify-book command
does not explicitly specify :skip-proofs-okp nil, as we now explain. A
non-nil value of 'write-acl2x should either be t or a
one-element list (x), where x is a legal value for the state
global 'ld-skip-proofsp (see ld-skip-proofsp). In both cases,
certify-book will process events to write out a .acl2x file
as described above. But in the latter (list) case, event processing will take
place according to the value of x: in particular, proofs will be skipped
when x is not nil, and if moreover x is the symbol
include-book-with-locals, then only one pass will be made through each
encapsulate form. A third effect of a non-nil value of
'write-acl2x, which is restricted to the list case, is that include-book events encountered during event processing are allowed to
succeed on uncertified books, something that is prohibited during most calls
of certify-book.
When certify-book is used to write out a .acl2x file, there is
typically a subsequent run of certify-book that reads that file.
Consider how this can work with a book foo.lisp. In the first call of
certify-book, a file foo.acl2x is written that contains all make-event expansions, but foo.cert is not written. In the second call
of certify-book, no make-event expansion typically takes place,
because foo.acl2x supplies the expansions. The command
(set-write-acl2x t state) should be evaluated before the first
certification (though another legal non-nil value may be used in place of
t), setting the value of state global 'write-acl2x to
t, to enable writing of foo.acl2x; and the command
(set-write-acl2x nil state) may be evaluated before the second run
(though this is not necessary in a fresh ACL2 session) in order to complete
the certification (writing out foo.cert) using foo.acl2x to supply
the make-event expansions.
When Certify-book is supplied with keyword argument :acl2x t
it will read or write the book's .acl2x file; when supplied with
:acl2x nil, it will not read or write that .acl2x file. The value
of :acl2x is nil by default. The interaction of certify-book with the corresponding .acl2x file is as follows.
o If :acl2x is t, then:
- If set-write-acl2x has been (most recently) called with a value of
t for its first argument,then ACL2 writes the corresponding
.acl2x file.
- If set-write-acl2x has been (most recently) called with a value of
nil for its first argument, or not called at all, then ACL2 insists
on a corresponding .acl2x file that is at least as recent as the
corresponding .lisp file, causing an error otherwise.
o If :acl2x is nil,then:
- If set-write-acl2x has been (most recently) called with a value
t for its first argument, or if argument :ttagsx is supplied,
then an error occurs.
- If the .acl2x file exists, then regardless of whether or how
set-write-acl2x has been called, ACL2 ignores the .acl2x file
but issues a warning about it.
Suppose you use the two-runs approach: first write a .acl2x file, then
certify using (reading) that .acl2x file. Then with scripts such as
makefiles, then you may wish to provide a single certify-book command
to use for both runs. For that purpose, certify-book supports the
keyword argument :ttagsx. If this argument is supplied and
write-acl2x is true, then this argument is treated as the :ttags
argument, overriding a :ttags argument if present. That is, for the two
runs, :ttagsx may be used to specify the trust tags used in the first
certification while :ttags specifies the trust tags, if any (else
:ttags may be omitted), used in the second certification. Note: If the
argument :ttagsx is not supplied, then its value defaults to the
(explicit or default) value of the :ttags argument.
The built-in ACL2 Makefile support automatically generates suitable
dependencies if you create a .acl2 file with a certify-book call
matching the following regular expression, case-independent:
(certify-book[^;]*:acl2x t
For an example .acl2 file with a certify-book call matching the
above pattern, see community books file
books/make-event/double-cert-test-1.acl2.
Note that include-book is generally not affected by
set-write-acl2x, other than through the indirect effect on certify-book. More precisely: All expansions are stored in the certificate file, so when include-book is applied to a certified
book, the .acl2x file is not consulted.
An example of how to put this all together may be found in community book
books/make-event/double-cert-test-1.lisp. There, we see the following
form.
(make-event
(progn (defttag :my-ttag)
(progn! (let ((val (sys-call "pwd" nil)))
(value (list 'defun 'foo () val))))))
Imagine that in place of the binding computed using sys-call, which
by the way requires a trust tag, is some computation of your choice (such as
reading forms from a file) that is used to construct your own event, in place
of the defun event constructed above. The Makefile in that
directory contains the following added dependency, so that file
double-cert-test-1.acl2x will be created:
double-cert-test-1.cert: double-cert-test-1.acl2x
There is also the file double-cert-test-1.acl2 in that directory,
which contains a single form as follows.
(certify-book "double-cert-test-1" ? t :ttagsx :all :ttags nil)
Thus, a call of `make' first creates file double-cert-test-1.acl2x,
which uses the above :ttagsx argument in order to support the use of
defttag during make-event expansion. Then, `make' goes on to
cause a second certification in which no trust tags are involved. As a
result, the parent book double-cert-test.lisp is ultimately certified
without requiring any trust tags.
The discussion above is probably sufficient for most users of the two-run
approach it describes. We conclude with further details for those who want
more information. Those who wish to see a yet lower-level explanation of how
all this works are invited to read the comment in the ACL2 source code
entitled ``Essay on .acl2x Files (Double Certification).
Consider the .acl2x file produced by the first run as described above.
It contains a single expression, which is an association list whose keys are
all positive integers, which occur in increasing order. When the .acl2x
file is present and at least as recent as the corresponding .lisp file,
then for a subsequent certify-book with argument :acl2x t and the
(default) value of nil for state global 'write-acl2x, that
association list will be applied to the top-level events in the book, as
follows. Suppose the entry (n . ev) belongs to the association list in
the .acl2x file. Then n is a positive integer, and the nth
top-level event in the book — where the 0th event is the initial
in-package form — will be replaced by ev. In practice,
ev is the make-event expansion created during certification for
the nth top-level event in the book; and this will always be the case if
the .acl2x file is created by certify-book after execution of the
form (set-write-acl2x t state). However, you are welcome to associate
indices manually with any events you wish into the alist stored in the
.acl2x file.
Note: Also see the community book make-event/acl2x-help.lisp for a
useful utility that can be used to skip proofs during the writing of
.acl2x files.
