ACL2 Installer for Windows
This program will install a complete ACL2 environment, including:
* ACL2 3.2
* GCL 2.6.7
* GNU Emacs 21.3
* Unix commands
* ACL2 sources
* Pre-certified books
Feedback: firstname.lastname@example.org or email@example.com.
ACL2 3.2 installer
We strongly recommend that you install ACL2 to the default location:
C:\ACL2-3.2\. This will allow you to take advantage of the pre-certified
books provided by the installer. If you choose a different installation
directory, see the instructions for installing
in a non-standard location.
Compatibility with Older Versions
You should have little trouble installing this alongside older versions
of ACL2 if you used previous versions of this installer. Essentially,
everything here gets installed to C:\ACL2-3.2,
whereas previous versions would have been installed to other folders,
e.g., C:\ACL2-3.1 and so forth.
Mainly, be aware that your PATH variable will determine which
version will be loaded when you type "acl2". You may wish to rename the
acl2.exe programs to distinguish between versions, i.e., v32.exe and
v31.exe, or something along those lines.
Tips for Using ACL2 in Windows
- Paths. The installers will automatically add
ACL2-3.2\bin and ACL2-3.2\mingw\bin to your
path. So, you will be able to access the common Unix commands, e.g.,
ls, grep, and so forth from anywhere in DOS.
Emacs will be installed to ACL2-3.2\emacs-21.3, and the
program is: ACL2-3.2\emacs-21.3\bin\runemacs.exe. You
can easily convince Explorer to open lisp files using runemacs.exe,
if you so desire.
- ACL2 in DOS. DOS is really a horrible way of interacting
with ACL2, and you should probably use Emacs instead.
- The default DOS window will let you scroll back only 300 lines.
You can extend this (in Windows 2000, at least) up to 9999 lines.
To do so, start ACL2, then go to the well
hidden properties window. Choose the layout
tab and increase the height of the screen buffer size. If you invoke
ACL2 from a shortcut, you will have the option to
modify the shortcut so that it will
always have more history at startup.
- You can use Bash instead of DOS if you want. To do so,
start up a DOS window and type
sh. Bash provides nice
automatic completion of commands, history, and greater scriptability
than DOS. But, you're still confined to the DOS window's history
limits and so forth, so you might prefer to run Bash from within
- ACL2 in Emacs. This is generally a much nicer way
to work than using DOS, because you have virtually unlimited,
clearable history and can copy/paste much more easily. You can
set up a very nice split screen with your file and ACL2 session visible
at the same time:
- Create a .lisp file and open
it in emacs.
- Split your emacs
window by first typing [ctrl + x] together, then typing
- Create a shell buffer by first
clicking on the right-hand window, then typing [alt + x]
together, then type shell and hit enter.
- Invoke ACL2 in the shell buffer
by typing acl2.
- Using the ACL2-Emacs Environment. If you choose to install
the ACL2 sources, then the usual emacs-acl2.el file is installed to
ACL2-3.2\sources\emacs. You can load this file from your
.emacs file just as you would on a Unix system. The
.emacs file is apparently created in your HOME directory
(as specified by the environment variable HOME), or defaults
to C:\ if no HOME is specified. On my system, there
is no HOME set, so I just use C:\.emacs. You can
also explicitly load this at run-time using M-x load-file,
then putting in the path to sources/emacs/emacs-acl2.el.
About These Installers
Source code for these installers is available under the GNU General
Public License. It is quite easy to add new components, if for
instance you have some extension to ACL2 that you would like to
distribute for Windows systems.