Helpful Instructions for Setting up ACL2 and Windows

I was able to get ACL2 3.6.1 to install and build most of the distributed books1 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 executable2)
    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
  7. You can now make the regression suite by typing
    make regression ACL2=c:/acl2-3.6.1/acl2-sources/saved_acl2.bat


1The "serialize" books directory did not build due to a problem with CCL on Windows. For information on how to obtain a version of the ACL2 books that builds on CCL for Windows, visit the ACL2 Books Project Page

2I have intentionally omitted instructions on how to set up a LISP on windows. However, I include one link that should suffice: Obtaining CCL

Home

Valid XHTML 1.1!