Introduction

The following alphabetical list of books and directories describes additions to ACL2 Version 3.6 (made after the release of ACL2 Version 3.5). For changes to existing books rather than additions, see the log entries (follow the [Source] link) starting with revision r286 up through revision r329.

List of Books

critpath.pl:

Part of an experimental build system that is not yet intended, for example, to be capable of running the whole regression

defsort/remove-dups.lisp:

Minor addition of a duplicate-removing function to defsort

fix-cert/:

After moving books from one place to another in a filesystem, use this library to update the .cert files accordingly without costly recertification.

hacking/dynamic-make-event.lisp:

Low-level support for system hacking; see comment near top of file. New, related files: hacking/dynamic-make-event-test.acl2, hacking/dynamic-make-event-test.lisp, and hacking/dynamic-make-event.acl2.

misc/seqw.lisp:

New SEQW macro is like seq (see misc/seq.lisp), but collects warnings. See also new, related file misc/seqw-examples.lsp.

serialize/:

Optimized routines for Serializing ACL2 objects (for any host Lisp other than GCL). Quoting the :doc: "We implement some routines for writing arbitrary ACL2 objects to files, and for loading those files later."

tools/with-quoted-forms.lisp:

Useful for computing large :USE hints; see comment at top of file.

unicode/two-nats-measure.lisp:

Lexicographic order measure for pairs of natural numbers