How to commit code to the books using direct push access
This guide is written for two groups of people:
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 .
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
To join the github project, please send email to one of the following individuals.
After you have joined the project, you can proceed as follows when you are ready to contribute.
git fetch --all git merge remotes/origin/master
(time nice make LISP=<your_lisp>) >& make.log
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
(time nice make -j 8 regression-fresh) >& make-regression.log
fgrep -a '**' make-regression.log
(time nice make -j 8 regression) >& make-regression-finish-1.logNote that the
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/masterIf 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.
The following commands will update the github repository on the web. The
git commit -a -m '<some message, with descriptive first line>' git push origin testing