		Search-engine friendly clone of the ACL2 documentation.

Books-tour

Book-contents

Restrictions on the forms inside books

Example Book:

; This book defines my app function and the theorem that it is
; associative.  One irrelevant help lemma is proved first but
; it is local and so not seen by include-book.  I depend on the
; inferior book "weird-list-primitives" from which I get
; definitions of hd and tl.

(in-package "MY-PKG")

(include-book "weird-list-primitives")

(defun app (x y) (if (consp x) (cons (hd x) (app (tl x) y)) y))

(local
 (defthm help-lemma
   (implies (true-listp x) (equal (app x nil) x))))

(defthm app-is-associative
  (equal (app (app a b) c) (app a (app b c))))

The first form in a book must be (in-package "pkg") where "pkg" is some package name known to ACL2 whenever the book is certified. The rest of the forms in a book are embedded event forms, i.e., defuns, defthms, etc., some of which may be marked local. See embedded-event-form. The usual Common Lisp commenting conventions are provided. Note that since a book consists of embedded event forms, we can talk about the ``local'' and ``non-local'' events of a book.

Because in-package is not an embedded event form, the only in-package in a book is the initial one. Because defpkg is not an embedded event form, a book can never contain a defpkg form. Because include-book is an embedded event form, books may contain references to other books. This makes books structured objects.

When the forms in a book are read from the file, they are read with current-package set to the package named in the in-package form at the top of the file. The effect of this is that all symbols are interned in that package, except those whose packages are given explicitly with the ``::'' notation. For example, if a book begins with (in-package "ACL2-X") and then contains the form

(defun fn (x)
  (acl2::list 'car x))

then defun, fn, x, and car are all interned in the "ACL2-X" package. I.e., it is as though the following form were read instead:

(acl2-x::defun acl2-x::fn (acl2-x::x)
    (acl2::list 'acl2-x::car acl2-x::x)).

Of course, acl2-x::defun would be the same symbol as acl2::defun if the "ACL2-X" package imported acl2::defun.

If each book has its own unique package name and all the names defined within the book are in that package, then name clashes between books are completely avoided. This permits the construction of useful logical worlds by the successive inclusion of many books. Although it is often too much trouble to manage several packages, their judicious use is a way to minimize name clashes. Often, a better way is to use local; see local.

How does include-book know the definitions of the packages used in a book, since defpkgs cannot be among the forms? More generally, how do we know that the forms in a book will be admissible in the host logical world of an include-book? See certificate for answers to these questions.