Helpful Instructions for Setting up ACL2 and Windows

We thank David Rager for providing the following instructions, which we include verbatim and expect apply to future versions. Note: We recommend using CCL for Windows builds, in part so that interrupts (Control-C) will work. If you are using Windows, please note that there have been stalls using CCL 1.5 on Windows, though not with CCL 1.4. We have been told by a CCL implementor that this bug has been fixed, and people running CCL 1.5 under Windows at a revision less than 13900 should update.

I was able to get ACL2 3.6.1 to install and build the regression suite on Windows 7 with the following steps. I did not have to install cygwin.

1. Install MinGW. At the time of this writing, the following direct link works
   MinGW-5.1.6.exe

   If that direct link doesn't work, click on "Automated MinGW Installer" on the more general MinWG project files page.

2. Install MSys. At the time of this writing, the following direct link works
   MSYS-1.0.11.exe

   If that direct link doesn't work, click on "MSYS Base System" on the more general MinWG project files page.

3. Add "C:\msys\1.0\bin" to my environment variable "path". The way you do this varies with each Windows XP/Vista/7. Roughly speaking, you need to go to the control panel, and open up your system settings. Get to the advanced system settings and click on environment variables. Edit the "path" environment variable and add ";C:\msys\1.0\bin" to it. At this point you might need to restart your computer, but I did not have to do so on Windows 7. I did, however, have to restart my emacs.

4. Realize that using "\" to indicate paths in windows confuses some linux programs and that you might need to use "/" sometimes.

5. After expanding the ACL2 sources, cd to that directory and type something similar to the following (modify it to set LISP to your LISP executable¹)
   make LISP=c:/ccl/wx86cl64.exe
   The "make.exe" that will be used is intentionally the MSys version, not the MinGW version.

6. After your ACL2 image builds, make acl2 executable, specifically
   • Remove the "$*" from the saved_acl2 script (because Windows does not understand $*). Consequently, any arguments you pass to ACL2 via the command line will be ignored.
   • Rename saved_acl2 to saved_acl2.bat, for example by executing the following command: rename saved_acl2 saved_acl2.bat

7. You can now make the regression suite by typing
   make regression ACL2=c:/acl2-3.6.1/acl2-sources/saved_acl2.bat

   [Note added later: you may need to add `make' option ACL2_CENTAUR=skip, for example if you have issues with Perl.]

¹I have intentionally ommitted instructions on how to setup a LISP on windows. However, I include one link that should suffice: Obtaining CCL