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)

• Extract all the files from acl2.tar.gz to a directory of your choosing.  Be careful not to overwrite your ACL2 files!  You may want to rename the resulting acl2-sources directory to something like acl2r.
• Create a file called acl2r.lisp in the same directory with the following contents:

  (or (member :non-standard-analysis *features*)

      (push :non-standard-analysis *features*))

  (Alternatively, download it from here.)

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. 

• Copy maxima-dir\src\saved_maxima.exe to the acl2r directory.
• Rename the file init.lsp in the acl2r directory to initialize.lisp.
• Type the command saved_maxima in your DOS window.  You should get an error message, which you will ignore, and the prompt "MAXIMA>>".  (If instead you see the prompt "(C1)", see the recovery instructions.)
• Type the following commands (the first one will change the prompt to "MAXIMA>"):

: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.

• Invoke saved_maxima again.  Type the following commands to Maxima:

: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)

• The initialization attempt in the previous Maxima session ends in error.  This is perfectly normal.  Now we can finally create the executable.  Invoke saved_maxima again.  Type the following commands to Maxima:

: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")

• Rename nsaved_acl2.exe to saved_acl2.exe.

• Rename the file initialize.lisp back to init.lsp.

• Delete the file saved_maxima.exe from the acl2r directory.

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.

• Copy the books directory from acl2-sources to acl2r\books.
• Download the file nonstd.tar.gz from the ACL2 web site.  Extract the files to acl2r\books.  (The top-level directory in the zip file is "nonstd", but for consistency we want all books in the "books" directory.  After extracting, move all the files from "nonstd" to "books" [you can answer "yes" to the question about overwriting files], then remove the now-empty "nonstd" directory.)
• Now you can certify the books.  This process is similar to the one in Step 7 of the ACL2 installation instructions.  For example, in order to certify the arithmetic book (which you are very likely to need), issue the following commands to ACL2(r):

:set-cbd "acl2r/books/cowles"
(ld "certify.lsp")

:set-cbd "acl2r/books/arithmetic"
(ld "certify.lsp")