Best-practices
Recommended best practices for ACL2 books.
DRAFT
This is a preliminary document. Feedback is very much welcome and
appreciated. Please direct feedback to the acl2-books list or to Jared
Davis.
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.
Subtopics
- Working-with-packages
- How to set up new package and portcullis files.
- Theory-management
- Recommendations related to enabling and disabling functions and
theorems.
- Naming-rewrite-rules
- Recommendations for writing understandable rule names.
- Conventional-normal-forms
- Recommendations for respecting global conventions that the ACL2 books
authors have agreed to.
- Where-do-i-place-my-book
- How to decide where in the books directory structure to place your book
- File-names
- Restrictions to follow for naming books, directories, and other
files.
- File-extensions
- Conventions to follow for choosing file extensions like .lisp,
.lsp, and .acl2 files.
- Remove-whitespace
- How to find and remove whitespace from .lisp files
- Finite-reasoning
- Use gl to reason about finitely bounded values.
