SET-WRITE-ACL2X

cause certify-book to write out a .acl2x file
Major Section:  SWITCHES-PARAMETERS-AND-MODES

General Forms:
(set-write-acl2x t state)
(set-write-acl2x nil state)

Note: Also see the distributed book make-event/acl2x-help.lisp for a useful utility that can be used to skip proofs during the writing of .acl2x files.

This command is provided for those who use trust tags (see defttag) to perform make-event expansions, yet wish to create certified books that do not depend on trust tags. This is accomplished using two runs of certify-book on a book, say foo.lisp. In the first run, a file foo.acl2x is written that contains all make-event expansions, but foo.cert is not written. In the second certification, 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, setting 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.

Note that for the first certification (i.e., after evaluation of the form (set-write-acl2x t state)), it is permitted to skip proofs even if keyword value :skip-proofs-okp t has not been supplied to certify-book. An analogous situation holds for :defaxioms-okp.

Also note that certify-book needs to be supplied with keyword argument :acl2x t in order to read or write .acl2x files; the value of :acl2 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 (the default), 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.
  - Regardless of whether or how set-write-acl2x has been
    called, ACL2 ignores an existing .acl2x file but issues a
    warning about it.

If you use this two-runs approach 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.

The built-in ACL2 Makefile support automatically generates suitable dependencies if you create a .acl2 file with a certify-book call matching the following pattern, case-independent: (certify-book<characters_other_than_;>:acl2x t. See book-makefiles, and for an example .acl2x file see distributed file books/make-event/double-cert-test-1.acl2.

Note that include-book is not affected by set-write-acl2x, other than through the indirect effect on certify-book. More precisely: All expansions will be stored in the certificate file, so include-book does not depend on the .acl2x file.

An example of how to put this all together may be found in distributed 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 (pronounced ``dot-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 when write-acl2x is nil (the default), 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.