		Search-engine friendly clone of the ACL2 documentation.

Books

Best-practices

Recommended best practices for ACL2 books.

Here we summarize various style and formatting principles commonly accepted and employed across the ACL2 repository. The goal is to avoid opinionated rules and only highlight conventions which are widely agreed upon. The advice included here is intended to apply to the majority of cases. There may be exceptions in which a given rule ought be ignored. Use your best judgment.

See the developers-guide-style for a more specific style guide for changes to the core ACL2 system (not necessary if you are just developing books).

Whitespace and Special Characters

Avoid using tabs, as they may render inconsistently across machines and editors. Use spaces instead.
Do not leave ``trailing whitespace'' at the end of your lines (see remove-whitespace). Trailing whitespace can add noise to Git commits and disrupt navigation in the editor.
Unicode characters should be avoided in identifiers, but are permissible in comments and strings. (Keep in mind that some string utilities may not behave as expected, for instance length may return the number of bytes instead of the number of unicode code points.)
Avoid consecutive blank lines.
Line breaks should use the posix-style newline (i.e. "\n", not "\r\n"). Linux and Mac developers should not need to worry about this. Windows developers may need to be more careful that their editor or other tools uses posix-style newlines.
Files should end with a newline. (Note, we mean a newline, not a blank line.) This is a posix-standard. Most editors should handle this automatically.

Comments

Comments should begin with a single space. E.g.:
```
; This is a comment.
```
not
```
;This is a comment.
```
Books should begin with a copyright and licensing header (which may just point to the repository's top-level LICENSE file).
Use two semicolons for inline comments which should be indented as a form would be. This is a standard practice in Common Lisp, and editors like Emacs will indent such comments appropriately.
Avoid commented code which would disrupt the s-expression balance if uncommented. For instance, instead of this:
```
(let ((x foo)
      ;; (y bar))
      )
  baz
  )
```
do this:
```
(let ((x foo)
      ;; (y bar)
      )
  baz
  )
```
Consider whether comments would be more appropriate as XDOC documentation.

Documentation

XDOC short forms should be in ``sentence case,'' not ``title case.'' They should end with a period, even if they are not a full sentence.
XDOC short forms should not span multiple paragraphs, or include code blocks, tables, headers, etc.

Naming Conventions

Consider ending predicates with ``p'' (or ``-p,'' especially if needed for clarity). This is a convention inherited from Common Lisp.
For ordinary identifiers, avoid uppercase and use hyphens to delimit words (a style sometimes called ``dash-case'', ``kebab-case'', or ``lisp-case''). E.g., ``my cool function'' would be rendered my-cool-function.
See naming-rewrite-rules for recommendations regarding the naming of rewrite rules.

Formatting

Multiline if forms should be formatted as follows:
```
(if x
    y
  z)
```
That is, 4 spaces for the ``then'' term, and 2 spaces for the ``else'' term. If your Emacs auto-indents such forms incorrectly, consider adding the following to your Emacs configuration:
```
(eval-after-load 'cl-indent
  '(put 'if 'common-lisp-indent-function 2))
```

Packages

The use of packages is highly encouraged. This helps to avoid name clashes and polluting the default namespace. See working-with-packages for further guidance.
If you are defining a new package name, check to see that the name is not already in use. You can list all packages defined across the repository using the following grep command:
```
grep -hr --include='*.lsp' --include='*.acl2' -E '\(defpkg "[^"]*"' . \
  | sed -n 's/[^"]*"\([^"]*\)".*/\1/p' \
  | sort | uniq
```

Theory Events

Top-level include-book and in-theory events should be at the top of the book. Intermixing include-book and in-theory events with function definitions and theorems can make it more difficult for the maintainer to understand the state of the current theory.
include-book and in-theory events should be local where possible, unless they support the main purpose of the book and are intended to be ``exported.'' This allows libraries to be more modular and avoids cluttering the end-user's world.
Most functions (especially non-recursive function) should be disabled by default, unless they are best understood as simple aliases/wrappers.
Sets of rules which are known to cause rewrite loops should be declared incompatible as a theory-invariant.
See also theory-management.

Proofs

Try to avoid subgoal hints. These can make proofs brittle and difficult to maintain. If it is not sufficient to apply hints to the top-level goal, consider factoring out a subgoal into an auxiliary lemma.
Generally speaking, the less hints for a proof, the better. Consider whether :use or :expand hints may suggest good general-purpose rules (this is not always the case).
Try to avoid brittle proof-builder instructions (given as an argument to the :instructions keyword argument of either defthm or a goal hint) which may be difficult to maintain.
Avoid short proof timeout windows which could fail on slower machines (e.g. via with-prover-time-limit, ACL2s::set-defunc-timeout, etc.). If possible, avoid timeout windows altogether, or use step limits instead (e.g. with-prover-step-limit).

Book Style Consistency

There are certain styles which are not universal across the repository, but which should be consistent within a given book or library. Book style should be respected when making edits.
Try to match the line width of a file. Common line widths are 79 or 80.
A book should use either defun or define, not both.
A book should use either defthm or defrule, not both.

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.