ACL2 System and Books as Maintained by the Community
Clone or download
acoglio Improve the Ethereum library.
Use FTY::DEFBYTE and FTY::DEFBYTELIST to introduce simpler names for Ethereum's
bytes and nibbles. Now several names use BYTE and NIBBLE instead of UBYTE8 and
UBYTE4. A byte is always 8 bits in Ethereum, so it's appropriate to use this
simpler terminology in the "ETHEREUM" package.
Latest commit 0b741c1 Oct 7, 2018
Permalink
Failed to load latest commit information.
acl2-customization-files Added capability to turn off serialize-write for files written by cer… Aug 27, 2016
bin Updated to a more recent date in purity script, for efficiency. Sep 26, 2018
books Improve the Ethereum library. Oct 22, 2018
doc ACL2 Version 8.1 release Sep 19, 2018
emacs Fixed bugs in proof-builder dv command and emacs support for dive Oct 14, 2018
graphics Made a couple of gif files not-executable, as suggested by Keshav. Oct 27, 2017
installation ACL2 Version 8.1 release Sep 19, 2018
.gitignore Added make clean-all. Extended .gitignore. Mar 9, 2017
GNUmakefile ACL2 Version 8.1 release Sep 19, 2018
LICENSE ACL2 Version 8.1 release Sep 19, 2018
Makefile Initial population of trunk (will check in books/tools/include-raw.li… Sep 1, 2014
README.md After communicating offline with Matt, adding README.md symlink to to… Sep 3, 2014
acl2-characters 1. Quoting :doc note-4-4: Sep 1, 2014
acl2-check.lisp ACL2 Version 8.1 release Sep 19, 2018
acl2-fns.lisp ACL2 Version 8.1 release Sep 19, 2018
acl2-init.lisp First commit past the 8.1 release. Sep 20, 2018
acl2.lisp ACL2 Version 8.1 release Sep 19, 2018
akcl-acl2-trace.lisp ACL2 Version 8.1 release Sep 19, 2018
all-files.txt ACL2 Version 8.0 release Dec 14, 2017
allegro-acl2-trace.lisp ACL2 Version 8.1 release Sep 19, 2018
apply-constraints.lisp ACL2 Version 8.1 release Sep 19, 2018
apply-prim.lisp ACL2 Version 8.1 release Sep 19, 2018
apply-raw.lisp ACL2 Version 8.1 release Sep 19, 2018
apply.lisp ACL2 Version 8.1 release Sep 19, 2018
axioms.lisp Replaced fix-true-list by a more efficient version, true-list-fix, ba… Oct 3, 2018
basis-a.lisp ACL2 Version 8.1 release Sep 19, 2018
basis-b.lisp ACL2 Version 8.1 release Sep 19, 2018
bdd.lisp ACL2 Version 8.1 release Sep 19, 2018
boot-strap-pass-2-a.lisp ACL2 Version 8.1 release Sep 19, 2018
boot-strap-pass-2-b.lisp ACL2 Version 8.1 release Sep 19, 2018
build-allegro-exe.cl Initial population of trunk (will check in books/tools/include-raw.li… Sep 1, 2014
defpkgs.lisp ACL2 Version 8.1 release Sep 19, 2018
defthm.lisp Replaced fix-true-list by a more efficient version, true-list-fix, ba… Oct 3, 2018
defuns.lisp ACL2 Version 8.1 release Sep 19, 2018
doc.lisp Fixed bugs in proof-builder dv command and emacs support for dive Oct 14, 2018
futures-raw.lisp ACL2 Version 8.1 release Sep 19, 2018
history-management.lisp ACL2 Version 8.1 release Sep 19, 2018
hons-raw.lisp ACL2 Version 8.1 release Sep 19, 2018
hons.lisp ACL2 Version 8.1 release Sep 19, 2018
induct.lisp ACL2 Version 8.1 release Sep 19, 2018
init.lisp ACL2 Version 8.1 release Sep 19, 2018
interface-raw.lisp ACL2 Version 8.1 release Sep 19, 2018
ld.lisp ACL2 Version 8.1 release Sep 19, 2018
linear-a.lisp ACL2 Version 8.1 release Sep 19, 2018
linear-b.lisp ACL2 Version 8.1 release Sep 19, 2018
mcl-acl2-startup.lisp ACL2 Version 6.0 release Sep 1, 2014
memoize-raw.lisp ACL2 Version 8.1 release Sep 19, 2018
memoize.lisp ACL2 Version 8.1 release Sep 19, 2018
multi-threading-raw.lisp ACL2 Version 8.1 release Sep 19, 2018
new.html ACL2 Version 8.1 release Sep 19, 2018
non-linear.lisp ACL2 Version 8.1 release Sep 19, 2018
openmcl-acl2-trace.lisp ACL2 Version 8.1 release Sep 19, 2018
other-events.lisp ACL2 Version 8.1 release Sep 19, 2018
other-processes.lisp ACL2 Version 8.1 release Sep 19, 2018
other-releases.html ACL2 Version 8.1 release Sep 19, 2018
parallel-raw.lisp ACL2 Version 8.1 release Sep 19, 2018
parallel.lisp ACL2 Version 8.1 release Sep 19, 2018
proof-builder-a.lisp ACL2 Version 8.1 release Sep 19, 2018
proof-builder-b.lisp Fixed bugs in proof-builder dv command and emacs support for dive Oct 14, 2018
proof-builder-pkg.lisp ACL2 Version 8.1 release Sep 19, 2018
prove.lisp ACL2 Version 8.1 release Sep 19, 2018
rewrite.lisp ACL2 Version 8.1 release Sep 19, 2018
save-gprof.lsp ACL2 Version 8.1 release Sep 19, 2018
serialize-raw.lisp ACL2 Version 8.1 release Sep 19, 2018
serialize.lisp ACL2 Version 8.1 release Sep 19, 2018
simplify.lisp ACL2 Version 8.1 release Sep 19, 2018
tau.lisp ACL2 Version 8.1 release Sep 19, 2018
translate.lisp Accommodate use of make-lambda-term in sublis-expr+, by adding guards… Sep 25, 2018
type-set-a.lisp ACL2 Version 8.1 release Sep 19, 2018
type-set-b.lisp ACL2 Version 8.1 release Sep 19, 2018
workshops.html Updated with 2018 slogan Apr 2, 2018

README.md

ACL2 System and Community Books

WARNING: On rare occasions development versions of ACL2 may be incomplete, fragile, or unable to pass the usual regression tests. You may choose to download an official ACL2 release as described on the ACL2 Home Page or below in this README.

The ACL2 theorem proving environment consists of two parts: The ACL2 System and The ACL2 Books. This repository contains both.

ACL2 System

The included version of the ACL2 System is the latest, under-development version of the ACL2 Theorem Prover. It is updated only by the ACL2 authors, Matt Kaufmann and J Moore.

ACL2 Books

The books/ directory of this repository comprises the Community Books, which are the canonical collection of open-source libraries for the ACL2 System. As the name suggests, they are updated by the ACL2 community.

Documentation

  • The Combined ACL2 + Books Manual has extensive documentation for the latest stable version of ACL2 and many of the community books that come with it.

  • There is also a development version of the manual which is updated reasonably frequently and corresponds to the development version of ACL2 and its books.

  • Finally there is the more compact ACL2-only manual which only documents the ACL2 system itself and not any books.

Each of these manuals can be downloaded for offline use by clicking the download button on the right hand side of the upper toolbar while browsing the manual.

Obtaining the Source Code

While active development of ACL2 occurs at the acl2/acl2 repo on GitHub, stable releases are officially distributed from the acl2-devel/acl2-devel fork, which exists for that purpose.

Latest Stable Release

You can download a gzipped tarfile or zip file for the latest release, which includes the ACL2 system and the community books, from the releases page on GitHub.

Alternatively you can obtain a copy of the latest release using git. Do the following, after changing /path/to/somewhere/ to some suitable path where the directory /path/to/somewhere/acl2/ does not already exist.

git clone -b 8.1 git://github.com/acl2-devel/acl2-devel.git /path/to/somewhere/acl2/

The new directory /path/to/somewhere/acl2/ will now contain a copy of ACL2 Version 8.1. Please see the ACL2 home page, specifically its installation instructions, for how to build an executable and certify books in your new directory.

Experimental Development Version

To check out the latest development version of the repository using git, do the following:

git clone git://github.com/acl2/acl2.git

Contributing

See the documentation for how to contribute.

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

Staying Informed

We invite anyone who is using this repository to join the acl2-books mailing list, which receives commit messages and other discussion related to ACL2 system- and book-related development.

Contributors wanted!

Everyone can contribute documentation and advice to our wiki and discuss problems and feature requests.

If you would like to contribute to this repository, see the documentation topic git-quick-start. Please note the guidelines for book development.