Windows Installation

 

Home
Announcements
Handouts
Windows Installation
Installing ACL2(r)
Recovery Instructions

Installing ACL2 on Windows Platforms

The following instructions are adapted from those in ACL2 installation page.

Step 1: Install Common Lisp

ACL2 is built on top of Common Lisp, so you will first need to obtain and install Common Lisp.  We will use the free Gnu Common Lisp (GCL), and in fact use Maxima, which is built on top of GCL.  (Maxima is a descendant of the famous Macsyma system, which had a great influence of the development of computer algebra systems as well as on the development of Lisp.)

  • Download Maxima.  This link is an executable file that installs Maxima. Run the executable which will result in Maxima being installed in the directory of your choosing, say maxima-dir.
  • Open a DOS command window.  Add maxima-dir\gcc\bin to your path, and define the environment variable LD_LIBRARY_PATH with the value maxima-dir\gcc\i386-mingw32msvc\include.

Shortcut: Download Binaries

You can skip Steps 2-4 below by downloading a set of prepared binary files.

Step 2: Download ACL2

  • Download the file acl2.tar.gz.  This is a gzip-compressed Unix tar file.  If you have trouble with gzipped files, it is possible to download the full uncompressed distribution from ftp://ftp.cs.utexas.edu/pub/moore/acl2/v2-6/acl2-sources.  However, this may require you to restart download in the middle if the connection breaks (which happened to me a number of times).  It is much better to obtain a program such as WinZip that can open this file.  If you want free (but non-windowed) applications, see ftp://ftp.gnu.org/gnu/windows/emacs/utilities/i386.  
  • Extract all the files to a directory of your choosing.  Be sure that your program doesn't convert LF characters to CR/LF!  In WinZip you need to disable "smart cr/lf conversion" before extracting sources.  If when you try to compile ACL2 you get a message saying that the string "ab\ncd" has 6 characters instead of 5, you got it wrong in this step.
    Warning: it seems that GCL has trouble with pathnames that contain spaces, such as "Program Files".  You will save yourself some agony by choosing a pathname without spaces.
  • You should now have a directory called acl2-sources, created in the previous step.  Change your DOS window to that directory.
  • The following two files contain fixes to the ACL2 Version 2.6 distribution.  Download these two files into the same directory you uncompressed the acl2-sources directory:

Step 3: Compile ACL2 Files

  • Copy maxima-dir\src\saved_maxima.exe to the acl2-sources directory.
  • Rename the file init.lsp in the acl2-sources 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 "acl2.lisp")
(in-package "ACL2")
(compile-acl2)
(maxima::$quit)

Step 4: Create an ACL2 Executable

  • 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 acl2-sources directory.

Step 5: Prepare Settings for Running ACL2

  • When you run ACL2, you will need two directories on your path: the gcc directory from the Maxima distribution, maxima-dir\gcc\bin, and the acl2-sources directory.  You can add those permanently to your path in the autoexec.bat file or in the Environment Variables dialog of Windows NT/2000, or you can create a batch file for more selective use.  Once these settings are in effect, you can run ACL2 by typing saved_acl2 at the command prompt.

Step 6 (Optional): Install Emacs

If you have an operating system with scrollable DOS windows, you are all set.  However, if you don't, or if you want search facilities (and believe me, you do), then you need a shell with history and search.  You can use any such shell you like; my own favorite is Emacs (which, of course, is useful for much more than that).  Follow the following instructions to download and install Emacs, and your life will never be the same again!  (You can also see the full instructions and lots more.)

  • Download the latest version of Emacs from ftp://ftp.gnu.org/gnu/windows/emacs/latest/.  Now that you are proficient in opening gzipped files, get the single emacs-xx.yy-fullbin-i386.tar.gz file, and extract its contents to a directory of your choice.  This will create a directory called emacs-xx.yy.
  • Now run the program emacs-xx.yy\bin\addpm.exe.  This will create an entry for Emacs on your start menu; activate it to start Emacs.
  • Edit the file acl2-sources/emacs/emacs-acl2.el, and change the definition of the variable *acl2-sources-dir* (under the heading "EDIT THIS SECTION!") to reflect the location of your acl2-sources directory.
  • Inside Emacs, give the command M-x byte-compile-file, pointing it to the file acl2-sources/emacs/emacs-acl2.el.
  • You now can invoke ACL2 inside Emacs by giving the command M-x load file, pointing it to the file acl2-sources/emacs/emacs-acl2.elc.  This will open a shell buffer from which you can invoke ACL2.  This buffer is searchable, has a command history, and much more.  See the documentation in the file for more information.

Note: in order to avoid Windows shutdown problems, be sure to always exit ACL2 by typing

:good-bye

or, if you are in the lisp prompt:

(maxima::$quit)

and then type exit at the DOS prompt.  Do not be tempted to answer "yes" to the Emacs question "Active processes exist; kill them and exit anyway?".  Instead type "no", and exit according to the above procedure.

Step 7: Test ACL2 Installation

  • Invoke ACL2 and give it the command :mini-proveall.  This should produce a lot of output, proving various theorems.
  • Issue the following commands (where acl2-sources is the full path to the acl2-sources directory, with backslashes replaced by forward slashes):
:set-cbd "acl2-sources/books/cowles"
(ld "certify.lsp")
  • Now issue the following commands:
:set-cbd "acl2-sources/books/arithmetic"
(ld "certify.lsp")

You are now ready to use ACL2.