		Search-engine friendly clone of the ACL2 documentation.

Developers-guide

Developers-guide-style

Style Guidelines for Developing ACL2 System Code

Here we set out some style guidelines that have traditionally been followed in the ACL2 sources. They can guide development to help maintain ACL2's quality by giving its source files a consistent look.

The right margin is 79. (In Emacs: set-fill-column 79.) Existing code with margin 70 is OK to leave as is, though it's nice to convert to a margin of 79 when modifying comments within a given function.

Tabs are not used. In Emacs, setting buffer-local variable indent-tabs-mode to nil will accomplish this. That can be accomplished automatically for Lisp files, as is done in distributed file emacs/emacs-acl2.el; search there for indent-tabs-mode, or simply load that file in your .emacs file.

Periods that end sentences are followed by two spaces (useful for the meta-e command in Emacs).

Comments for a function go immediately after its formal parameters (even before declare forms).

Comments generally consist of complete sentences, starting on the left margin, each line starting with a single semicolon followed by a space. An exception is very short comments to the right of code up to the end of the same line.

Use of the cond macro is generally preferred to the use of if, an exception being small expressions that are not at the top level of the if structure.

System state globals need to be included in *initial-global-table*.

Blank lines are avoided except in the usual circumstances, e.g., surrounding comments and between definitions. Avoid consecutive blank lines.

A multi-line argument is not followed by an argument on the same line. For example, there should be a linebreak before the argument, arg, after the string in this COND clause:

(t (er soft ctx
       "The value associated with a :SOME-NEW-HINT hint must be a positive ~
       integer, but ~x0 is not." arg))

We generally avoid capitalizing all letters in a single word, except perhaps for keywords or quoted constants.

There are no multi-line comments: #|| ... ||#.

NEXT SECTION: developers-guide-other