ACL2 Installer for Windows

Download

ACL2 3.4 installer

Note: If you use ACL2's trace utility with the GCL executable, you may encounter a GCL bug. If so, send email to Matt Kaufmann at kaufmann@cs.utexas.edu to get a workaround.

Installer Notes

We strongly recommend that you install ACL2 to the default location: C:\Program Files\ACL2 3.4. 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:\Program Files\ACL2 3.4, 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.4\bin and ACL2 3.4\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.4\emacs-21.3, and the program is: ACL2 3.4\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.
  1. 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 want. To do so, start up a CMD window and type sh. Bash provides nice automatic completion of commands, history, and greater scriptability than CMD. But, you're still confined to the CMD window's history limits 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:
  1. Create a .lisp file and open it in emacs.
  2. Split your emacs window by first typing [ctrl + x] together, then typing 3.
  3. Create a shell buffer by first clicking on the right-hand window, then typing [alt + x] together, then type shell and hit enter.
  4. 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.4\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.

• SBCL version. SBCL for Windows is still in "prerelease" status. When it works at all, it seems to work well, with only one limitation: it does not support interruption. Thus, looping execution or divergent proofs cannot be interrupted with Ctrl+C (or C-c C-c in Emacs). Also, many systems refuse to run SBCL, showing some VirtualAlloc error. This is due to a limitation of SBCL in which virtual addresses for loading the image are hard-coded, and if your system already has those occupied (with DLLs, perhaps?) that build of SBCL will not run. Nevertheless, if it runs and you don't need interruption, it seems to work well.

• 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. 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.) Unless your boot.ini is setting /noexecute=AlwaysOn, GCL, SBCL, 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.

• NSIS Installer System home page (Get version 2.0 or later).
• ACL2 Installer Sources for customizing and maintenance.

Thanks to Jared Davis, David Rager, Alexander Spiridonov, and Peter Dillinger for all their work in making available the ACL2 Installer for Windows!