Defthm Consulting LLC came into being in 2013 and exists as a mechanism for funding projects of interest to the ACL2 community.  Please contact David Rager ( with any questions you may have.

Thanks to J Moore, Matt Kaufmann, and Bob Boyer for inspiring the name of the company.  And thanks to Pete Manolios for contributing the 2013 slogan: Pain is temporary; theorems are forever.  I like this slogan so much, that I’ve adapted part of it as the website’s motto.


Switched ACL2 from googlecode to github

We have completed the conversion from using svn on to using git on  The new repository is stored at  You can check it out using the following command:

git clone

We invite you to contribute to the repository by following (and improving) the guidance at

We will be moving the wikis and issue tracker to github over the next couple weeks.  Feel free to contribute to those on googlecode until we say that we’re about to move them (due to needing to be able to edit the wikis, committing to the googlecode repositories is still possible, but we do not recommend it).

You may notice that we have merged the Community Books (formerly acl2-books) and ACL2 System (formerly acl2-devel) repositories into one.  Nevertheless, changes should be made only to the books/ subdirectory unless you are Matt or J, since everything outside books/ is part of the ACL2 system.  (If you have suggestions for system changes, they should be sent to Matt or J, as has been done in the past.)

As always, feel free to ask questions via an ACL2 help email alias or the IRC channel #acl2.  We expect some questions on the best-practices for our community and how to use git and github.

If anyone is curious how this repository was created (it wasn’t trivial), and what tests were performed to ascertain its quality, you can view the scripts, supporting files, and logs at  I provide a summary below the
signature.  Thanks to David Rager for performing most of the work.
Also thanks to Jared Davis, Matt Kaufmann, and Keshav Kini for
help with many issues.

Creation Process:
— Dump both subversion repositories using svnsync and svnadmin
— Create a new svn repository with the books repo mounted in a books subdirectory
— Remove all branches and tags from the svn repository (but leaving their history)
— Convert the svn repo to git, canonicalizing emails to match github account email addresses
— Remove all references to branches and tags in the history using “bfg”
— “Rewrite” the git history to accommodate the move from uvnaimor-3 many years ago, the moving of the ACL2 system trunk up to root, and the moving of the books up a level
— Create a new repo and “cherry-pick” the 4000+ commits in order of timestamp to create a nicely ordered history
— Pushed the resulting repo to github

QA Process
— For each extension found in the svn repository, ensure that the number of files in the svn repository matches the number of files in the git repository.
— Did a diff to ascertain that everything that is in both repositories is the same (requires previous step for validity)
— Ran books “everything” target a couple times and also “manual” once.  I only did this using CCL and Hons.  I had a couple quicklisp issues, but they’re unrelated.
— Jared and I looked at the gitk output.
— David, Matt, and Jared performed diffs between the svn version and the git version and ascertained that the differences were reasonable.

(post shared after the fact and backdated)