Committing code: guidelines - acl2/acl2 GitHub Wiki

#Suggested guidelines to observe when committing code.

  • Document what you have changed when you commit with a good commit message.
  • Avoid breaking the build, by certifying the books (ideally including the workshop books).
  • Make sure all parens are balanced. File acl2-sources/emacs/emacs-acl2.el distributed with ACL2 defines a command meta-x find-unbalanced-parentheses for this purpose (you'll probably want to load this file via your ~/.emacs file anyway).
  • Books should target the version of ACL2 corresponding to the branch or trunk to which they are being committed.
  • Try to avoid adding Makefiles, instead relying upon the top-level GNUMakefile (and transitively cert.pl). Also see :doc books-certification.
  • Avoid non-local in-theory events except when there is good reason for them (e.g., modifying the theory for events defined in that book).
  • When using include-book for any book that is not part of your submission, use :dir :system (see :doc include-book). Do not use absolute pathnames, and only use pathnames relative to the book when including books that are part of the library (e.g., it is good for arithmetic-5/top.lisp to include arithmetic/"lib/basic-ops/top.lisp" using a relative path).
  • Include a copyright and license for each book, either directly or by pointing to a license file.
  • Comment all non-trivial changes with your name.
  • Document your submission

##Documenting the Submission

  • We highly recommend that you document your library using the XDOC system. See :DOC topic "xdoc" in the manual.
  • Include your documentation into the manual by including your top-level (or documentation) book from books/doc/top.lisp.

#Licensing

It is very important that no files are falsely claimed to be in the public domain or released under a particular license when the copyright holder has not granted such release. If it is too tricky to contribute and coordinate with the appropriate lawyers to obtain an official release, please make sure that you do not place a false license on the code. Companies that use such falsely-licensed code may be liable for patent-infringement and other IP-related claims. So, please don't mislead the community by placing an unapproved license. No license is better than a misleading license.

People on the various ACL2 mailing lists may be willing to provide offline advice on how to convince legal departments that contributing to the ACL2 community is a good value proposition.

#Integration of Version Control and Issue-tracking

There are commit-log commands to:

  • Easily set an issue's status to Fixed.
  • Update any aspect of the issue, and add a comment.

The issue tracker handles an easy-to-use "short form" syntax to set an issue's status to Fixed. This would be used when the source code change you are committing completely fixes a defect or implements a requested enhancement. The syntax is the following:

Fixes #9999

There is also syntax for flagging a commit as part of fixing an issue.

Update #NNN

See ACL2 repo git tips for more information.