• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Miscellaneous
      • Output-controls
      • Bdd
      • Macros
      • Installation
        • Installation-instructions
        • Using-ACL2
        • Obtaining-common-lisp
        • Installation-support
      • Mailing-lists
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • ACL2

Installation

Installing ACL2

See the installation-instructions for steps to install ACL2.

If you encounter problems installing ACL2, or need more information, see installation-support.

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. Also see using-ACL2 for information about running ACL2 and about its documentation.

Subtopics

Installation-instructions
ACL2 installation instructions for Unix-like systems
Using-ACL2
Using ACL2
Obtaining-common-lisp
Obtaining Common Lisp
Installation-support
Additional support for ACL2 installation