SET-WRITE-ACL2X

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


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 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
See book-makefiles, and 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.