• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • How-to-contribute
        • Common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Mailing-lists
    • Interfacing-tools
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• About-ACL2

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 public GitHub repository. This will involve first creating a personal fork of the repository. Then, once you've committed your changes and tested the build, you may open the PR to merge your changes into the ACL2 repository. PRs should target the ``testing'' branch or similar (not the ``master'' branch).

Checking the Build

You should run a regression build to ensure that your code changes did 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.)

A successful regression build is a good indicator, but it may not tell the whole story. Be careful to avoid introducing code which may build on your local machine but fail in other environments. E.g., via dependence on environment variables or absolute pathnames, use of external tools without an appropriate cert_param, short timeouts which may fail on slower machines, etc.

Best Code Practices

See best-practices for recommended code practices.

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.

``Off-Limits'' Source Files

The community is invited to submit code contributions to the Community Books. Source files outside of the ``books'' directory should not be modified, except by system maintainers. For those interested in development of the ACL2 core system, see the developers-guide.

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 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, please send email to 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.