		Search-engine friendly clone of the ACL2 documentation.

ACL2

Installation

Installation Guide

ACL2 is more than just the executable image. In particular, the system is distributed with libraries developed by the ACL2 community (see community-books) as well as the ACL2+Books User's Manual for the system and those libraries.

The installation guide consists of the following main parts.

See installation-summary for a summary of installation steps for Unix-like systems. That should usually suffice to get ACL2 ready for you to use.
See installation-requirements for how to obtain a Common Lisp implementation.
See installation-support for more details pertaining to obtaining and installing ACL2. You can probably ignore this topic and its subtopics.
See using-ACL2 for information about running ACL2 and about its documentation.

Also see copyright for information about copyright, license, and authorship of the ACL2 system, and see acknowledgments for sponsorship information.

For a variant of ACL2 that supports reasoning about the real numbers, see real.

See mailing-lists for information about mailing lists for ACL2 users, including how to post and how to access archives.

ACL2 may be exported to any countries except those subject to embargoes under various laws administered by the Office of Foreign Assets Control (“OFAC”) of the U. S. Department of the Treasury.

For more information about getting started with ACL2, see start-here.

Subtopics

Using-ACL2: Using ACL2
Installation-requirements: Obtaining Common Lisp
Installation-summary: ACL2 installation summary for Unix-like systems
Installation-support: Additional support for ACL2 installation