		Search-engine friendly clone of the ACL2 documentation.

How-to-contribute

Guide to contributing code to ACL2.

The main way to contribute code to ACL2 is to open a pull request (PR) to the ACL2 GitHub repository. First create a personal fork of the repository and commit your changes/additions there. Then open a PR to merge your changes into the main ACL2 repository. Please ensure your PR follows these guidelines:

Required: Make Changes Only Within the books/ Directory

While the community is invited to submit contributions to the Community Books, source files outside of the books/ directory should not be modified, except by system maintainers.

Suggestions for system changes can be emailed to Matt Kaufmann. (Prospective system developers should see the developers-guide.)

New developments that do not clearly belong in an existing directory are often put into the projects subdirectory of books/.

Required: Avoid Problematic Constructs

Avoid introducing code that may fail on machines/environments other than your own. In particular, avoid the following:

Dependence on any files not included in your PR. In particular, any book that depends on an external tool, such as an SMT solver, should include an appropriate cert_param.
Dependence on environment variables that will not be set in other users' environments.
Use of absolute pathnames (e.g., mentions of your home directory). These are likely to cause problems for other users. To bring in other Community Books, use the :dir :system option of include-book.
Constructs with timeouts that cause proof attempts to be aborted after a short time. These may cause failures on slower or heavily loaded machines.

Required: Check the Build

Before making your PR, you should run a regression to ensure that your changes/additions do not break the build. To do so, run the following make command in the ``books'' directory:

make -j 8 regression

(Note: the -j 8 option in the above command is only illustrative. It instructs make to use 8 hardware threads. You may use a higher or lower number to align with your system. See books-certification for an extended discussion on community book certification.)

Required: Change the Base Branch of your PR to testing

When opening your PR to merge changes into the main ACL2 repository, set the base branch to the testing branch (or similar) (not the master branch). Once your PR is accepted into the testing branch, it will be tested and merged automatically into the master branch if all tests pass.

Suggested: Follow Best Practices for ACL2 Code

See best-practices for recommended code practices.

Suggested: Document Your New Books

Consider creating documentation using the xdoc system. Then, to ensure your new topics appear in the manual, ensure they are included by books/doc/top.lisp, perhaps via another book that it includes, such as books/projects/top-doc.lisp.

Suggested: Update the Release Notes

Consider adding some high-level information about your changes to the Community Books' release notes — i.e., the appropriate release-notes-books XDOC topic in books/doc/relnotes.lisp.

Resources for Git/GitHub

For those new to Git (the version control system) or GitHub (the platform on which the ACL2 Git repository is hosted), see git-quick-start.

Frequent Contributors

Frequent contributors may request to join the ACL2 GitHub project. Such contributors may push directly to various testing branches without opening a PR (although it is still good practice to open a PR when modifying a widely used book or one primarily authored by someone else).

To request to join the project, email one of the following individuals:

Eric Smith (eric.smith@kestrel.edu)
David Rager (ragerdl@gmail.com)
Sol Swords (sswords@gmail.com)

See also the community topic for other ways to connect with the ACL2 community, and ways to get help.