Installing ACL2 on Windows Platforms
The following instructions are adapted from those in ACL2
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.)
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
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
- 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
- Type the following commands (the first one will change the prompt to
Step 4: Create an ACL2 Executable
- Invoke saved_maxima again. Type the
following commands to Maxima:
(initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)
- 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:
(save-acl2 (quote (initialize-acl2 (quote include-book) *acl2-pass-2-files* t))
- 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
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
- 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
- Inside Emacs, give the command M-x byte-compile-file, pointing it to the
- 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
or, if you are in the lisp prompt:
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):
- Now issue the following commands:
You are now ready to use ACL2.