How to build an ACL2 executable
This topic summarizes steps for building an ACL2 executable. For
more details see the ACL2
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).
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.
- (Advanced) how to get cert.pl to use save-exec images
to certify parts of your project.
- Installing Clozure Common Lisp (CCL)
- Installing Steel Bank Common Lisp (SBCL)