|
|
|---|
|
|
|
|---|
Guide for ACL2 developers
This guide is NOT intended for the full ACL2 user community. Rather, it is intended for experienced ACL2 users who may wish to become ACL2 developers, that is, to contribute to the maintenance and enhancement of the ACL2 source code. Don't waste your time here unless you're an ACL2 developer, or intending to become one!
ACL2 is maintained solely by Matt Kaufmann and J Moore, although for some time they have occasionally vetted code written by others, ultimately incorporating it into the system. Although this is anticipated to remain the case for some time, a process is underway towards gradually turning maintenance over to some other small group of trusted, reliable, responsible people. This guide was motivated by the desire to begin to support the eventual development of such a group.
(Of course, given the permissive license of ACL2, anyone is allowed to modify a copy of its source code. Here we are talking about what is generally called ``ACL2'', which is distributed from github and from the University of Texas at Austin.)
The first step towards contributing to ACL2 development is to join the
The website for the (first) Developer's Workshop has quite a bit of useful information. It is at:
http://www.cs.utexas.edu/users/moore/acl2/workshop-devel-2017/
Note that for the second Developer's Workshop, some colors were added to
this Guide to help guide the discussion. (Colors show up in the web version
but not in the ACL2-doc browser.) This
Prospective ACL2 developers are advised to read the paper, “Abbreviated Output for Input in ACL2”, which has a lot of discussion about ACL2 development.
[...SOME NOTES FOR THE WORKSHOP...]
For a small list of potential ACL2 development tasks, see community books
file
The subtopics listed below are sometimes referred to as ``chapters'' of this (Developer's) Guide. They can be read in any order, but on a first read, you may find it helpful to read them in the order in which they appear below.
NEXT SECTION: developers-guide-introduction