How to build an ACL2 executable
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)