• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Release-notes
        • Version
        • Acknowledgments
        • Common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
          • Using-extended-ACL2-images
          • Ccl-installation
          • Sbcl-installation
        • ACL2-help
        • Bibliography
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• About-ACL2

Building-ACL2

How to build an ACL2 executable

This topic summarizes steps for building an ACL2 executable. For more details see the ACL2 installation page.

To build an ACL2 executable, submit the following command while standing in the main ACL2 directory, where <my-lisp> invokes your Lisp executable (default: ccl).

make LISP=<my-lisp>

You should find "Initialization SUCCEEDED." near the end the of the log. Note: There may be ACL2 warnings, for example: "ACL2 Warning [Skip-proofs] in....". These may be safely ignored.

Note that you will want to certify books in order to take full advantage of ACL2. See books-certification.

See save-exec for how to build an ACL2 executable from a state resulting from the running of specified commands.

Subtopics

Using-extended-ACL2-images

(Advanced) how to get cert.pl to use save-exec images to certify parts of your project.

Ccl-installation

Installing Clozure Common Lisp (CCL)

Sbcl-installation

Installing Steel Bank Common Lisp (SBCL)