• 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
      • Obtaining-common-lisp
      • Installation-instructions
      • Using-ACL2
      • Installation-support
        • Creating-executable
        • Windows-installation
        • Summary-of-ACL2-system-distribution
        • Running-ACL2-without-executable
    • Mailing-lists
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Installation

Installation-support

Additional support for ACL2 installation

To install ACL2, it will generally suffice to see the installation-instructions. You should read the subtopics below only if those instructions were somehow not sufficient. They provide alternate and additional information for obtaining and installing ACL2 and associated libraries.

Subtopics

Creating-executable

Creating or obtaining an executable image

Windows-installation

Installing ACL2 on Windows

Summary-of-ACL2-system-distribution

Summary of ACL2 system distribution

Running-ACL2-without-executable

Running ACL2 without building an executable image