|
|
|---|
|
|
|
|---|
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
make LISP=<my-lisp>
You should find "Initialization SUCCEEDED." near the end 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.