ACL2 Installer for Windows
This program will install a complete ACL2 environment, including:
* ACL2 3.6 built on GCL
* GCL 2.6.7
* GNU Emacs 21.3
* Unix commands
* ACL2 sources
* Pre-certified books (with compiled files both for GCL)
ACL2 3.6 installer
We strongly recommend that you install ACL2 to the default location:
C:\ACL2-3.6. 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.6,
whereas previous versions would have been installed to other folders,
e.g., C:\ACL2-3.2 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.6\bin and ACL2-3.6\mingw\bin to your
path. So, you will be able to access the common Unix commands, e.g.,
ls, grep, and so forth from any windows command
prompt (CMD, a.k.a. "DOS").
Emacs will be installed to ACL2-3.6\emacs-21.3, and the
program is: ACL2-3.6\emacs-21.3\bin\runemacs.exe. You
can easily convince Explorer to open lisp files using runemacs.exe,
if you so desire.
- ACL2 in a Console Window. When you double-click acl2.exe,
ACL2 is run in a Windows console window, but this is really a
horrible way of interacting with ACL2, and you should probably use
Emacs (see below) or ACL2s instead.
- By default, the 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 CMD if you wish. To do so,
start up a CMD window and type
sh. Bash provides nice
automatic completion of commands, history, and greater scriptability
than CMD. If you prefer a Unix terminal to CMD, you may also type
and get a separate terminal with a running Bash shell.
But, you're still confined to a limited history and so forth,
so you might prefer to run Bash from within Emacs.
- ACL2 in Emacs. This is generally a much nicer way
to work than using CMD, 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.6\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 acl2-sources/emacs/emacs-acl2.el.
- Data Execution Prevention (DEP). If you are experiencing
mysterious "Fatal errors" or "Windows has closed this program" errors, this
could be due to DEP. Many versions of windows now support using the NX bit
of recent processors to prevent execution of dynamically generated code,
which is a problem for good Common Lisp implementations. You can either
make sure your system is only using DEP for "essential Windows programs and
services only" (a web search can quickly tell you how) or you can easily
install a compatibility profile available
through this link. (This was originally created for ACL2 Version
3.4 but we expect it to work with Version 3.6.)
Just unzip to a temporary location and run
install-DEP-fixes.exe, which will install
ACL2-3.4-DEP-Fixes.sdb. (You may then delete those files.)
boot.ini is setting
GCL and ACL2 images distributed with this installer should
then run without DEP.
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. We may put up the sources later; for
now, below is a link to the Version 3.4 installer sources.
Thanks to Jared Davis, Harsh Raju Chamarthi, David Rager, Alexander Spiridonov, and Peter Dillinger
for all their work in making available the ACL2 Installer for Windows!