• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
      • Start-here
        • Gentle-introduction-to-ACL2-programming
        • ACL2-tutorial
        • About-ACL2
          • Release-notes
          • Version
          • Acknowledgments
          • Common-lisp
          • Git-quick-start
            • Github-commit-code-using-push
              • Github-commit-code-using-pull-requests
            • Copyright
            • Building-ACL2
            • ACL2-help
            • Bibliography
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Git-quick-start

    Github-commit-code-using-push

    How to commit code to the books using direct push access

    This guide is written for two groups of people:

    • Users of the ACL2 System and Books who do not plan to contribute to the books, and
    • Contributors who commit to the repository on a monthly or weekly basis. In this case, a contributor will typically begin with the github-commit-code-using-pull-requests method, and after they are familiar with the process and community, they will move to this method.

    (A) GETTING STARTED

    Start by obtaining an up-to-date copy of the web-based github repository. Here, we show how to put it into into a directory called ACL2 (but name it whatever you like).

    mkdir ACL2
    cd ACL2
    git clone https://github.com/acl2/acl2 .

    (B) UPDATING

    The following commands will update your directory to match the latest contents of the github repository (on the web).

    git fetch --all
    git merge remotes/origin/master

    (C) CONTRIBUTING (optional)

    To join the github project, please send email to one of the following individuals.

    • Jared Davis (jared.c.davis@gmail.com)
    • David Rager (ragerdl@gmail.com)
    • Sol Swords (sswords@gmail.com)

    After you have joined the project, you can proceed as follows when you are ready to contribute.

    Change and Test

    1. Update as in (B) above:
      git fetch --all
      git merge remotes/origin/master
    2. Build an executable.
      (time nice make LISP=<your_lisp>) >& make.log
    3. Make book changes. If you are creating any new books, tell git that you intend to add them (but the repository on the web won't change until the last step below is executed).
      git add file1 file2 ...
      Also, 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.
    4. Run a regression.
      (time nice make -j 8 regression-fresh) >& make-regression.log
    5. Look for failures, as indicated by ** in the log.
      fgrep -a '**' make-regression.log
    6. If there were failures, then go back to Step 1 above to make appropriate changes and re-test, but you can replace the 'make' step by replacing regression-fresh with regression, since 'make' is clever enough to avoid recertifying more than is necessary. For example:
      (time nice make -j 8 regression) >& make-regression-finish-1.log
      Note that the -j 8 option specifies the use of 8 hardware threads; feel free to omit it or use a more suitable number (especially if your computer has other than 8 hardware threads).

    Update, and Iterate If Necessary

    Update again as in (B) above:

    git fetch --all
    git merge remotes/origin/master

    The merge may fail if there have been remote updates, that is updates in the repository on the web. In that case, commit your changes locally and then try the merge again. You might want to use the -F option instead of -m; see the next section for more on those options.

    git commit -a -m '<some message, with descriptive first line>'
    git merge remotes/origin/master

    If the second command prompts you for a message, the empty message should suffice as a reasonable default. (In emacs, if vi tries to come up, just type :q and <RETURN>.

    You can now go on to the next step (Contribute Your Changes). But ideally: If the output indicates that anything has changed, then go back to ``Change and Test'' above. Of course, you can skip the build if no ACL2 sources have changed, and you can skip making book changes if you are still happy with your changes.

    Contribute Your Changes

    The following commands will update the github repository on the web. The -m ... option is a log message whose first line should be a summary of your changes and other lines may give more details. You are welcome to replace the -m ... option by -F <filename>, where <filename> is the name of a file that contains your log message.

    git commit -a -m '<some message, with descriptive first line>'
    git push origin testing