Installing ACL2(r) on Windows Platforms
Installation of ACL2(r) is similar to that of ACL2, with some modifications. For these instructions, it is assumed that you have already installed Common Lisp and ACL2.
Shortcut: Download Binaries
You can skip Steps 1-3 below by downloading a set of prepared binary files for ACL2(r).
Note: This zip file contains only the top-level directory. It doesn't contain any other directories, such as documentation or books.
Step 1: Unpack ACL2(r)
Step 2: Compile ACL2(r) Files
This step is identical to Step 3 from the ACL2 installation, except for one line, marked in red below.
:q (in-package "lisp") (load "acl2r.lisp") (load "acl2.lisp") (in-package "ACL2") (compile-acl2) (maxima::$quit)
Step 3: Create an ACL2 Executable
This step is identical to Step 4 from the ACL2 installation.
:q (in-package "lisp") (load "initialize.lisp") (in-package "ACL2") (load-acl2) (initialize-acl2 (quote include-book) *acl2-pass-2-files* t t) (maxima::$quit)
:q (in-package "lisp") (load "initialize.lisp") (in-package "ACL2") (save-acl2 (quote (initialize-acl2 (quote include-book) *acl2-pass-2-files* t)) "saved_acl2")
Step 4: Certify Books
ACL2(r) uses the same books as the standard ACL2, but they behave differently (since the use conditional loading). You will therefore have to re-certify the books for ACL2(r). You should copy the books to a different directory, so as not to interfere with the standard ACL2.
:set-cbd "acl2r/books/cowles" (ld "certify.lsp"):set-cbd "acl2r/books/arithmetic" (ld "certify.lsp")