Ways to contribute - acl2/acl2 GitHub Wiki

A few ideas for ways to improve the books

#Documentation

There is always more work to be done on documentation.

Many libraries have no documentation at all. Even a brief page that just says what the library is, where it's located, and briefly what it provides would be a real service (and a way to learn about what's available).

Improving the existing documentation by adding examples, links to other materials, clarifying things, etc., would also be valuable. Note that the ACL2 User's Manual is now (as of late October, 2013) editable by the community as the book system/doc/acl2-doc.lisp.

#Interoperability

Sometimes, libraries have name clashes that make them incompatible with one another. A hard to achieve (but laudable) initial goal might be to simply include all the (non-workshop) books together.

Beyond that, truly integrating libraries to make them play well together might be a lot of work, but could be valuable.

A "bookdata" tool may be helpful for finding name conflicts in books. This tool is included with ACL2 after Version 6.3, starting with acl2-devel svn copies obtained after October 4, 2013. Dave Greve has begun (in October 2013) investigating the use of this tool to avoid name conflicts, but welcomes help. See :DOC bookdata.

#System function guards

It would be nice to have additional ACL2 theorem prover functions brought into logic mode and guard-verified. Some functions that might be nice:

  • output functions like fmt
  • genvar
  • find-first-bad-arg
  • cons-tag-trees
  • strip-branches
  • clausify
  • if-tautologyp
  • expand-some-non-rec-fns (if you'd like a challenge involving mutual-recursion)
  • rewrite-solidify
  • loop-stopperp
  • equal-mod-alist (this one's termination is trivial, but its guards are undefined)

There may be cases in which a built-in definition needs modification, e.g. by adding guards or changing a null test to an endp test; Matt Kaufmann is interesting in cooperating by incorporating such modifications into the ACL2 sources.

New proofs along these lines can be included in system/top.lisp. The ACL2 build/maintenance process ensures that all built-in functions that are guard-verified after executing (include-book "system/top" :dir :system) are in fact guard-verified in the normal ACL2 build.