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:
Tabs are not used. In Emacs, setting buffer-local variable
Periods that end sentences are followed by two spaces (useful for the
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
System state globals need to be included in
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,
(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