Recommended best practices for ACL2 books.
This is a preliminary document. Feedback is very much welcome and
appreciated. Please direct feedback to the acl2-books list or to Jared
We recommend the use of the Standard Libraries (std) to ease your
burden of modeling and reasoning in a formal sytem. See other subtopics below
for other best practices.
If you expect your library to be used at all by other people, put your code
in a package. Jared, Rager, and Kaufmann spend a large amount of time just
dealing with name clashes, and it leaves them grumpy. See working-with-packages.
- How to set up new package and portcullis files.
- Recommendations related to enabling and disabling functions and
- Recommendations for writing understandable rule names.
- Recommendations for respecting global conventions that the ACL2 books
authors have agreed to.
- How to decide where in the books directory structure to place your book
- Restrictions to follow for naming books, directories, and other
- Conventions to follow for choosing file extensions like .lisp,
.lsp, and .acl2 files.
- How to find and remove whitespace from .lisp files
- Use gl to reason about finitely bounded values.