• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
        • Gentle-introduction-to-ACL2-programming
        • ACL2-tutorial
        • About-ACL2
          • Recursion-and-induction
          • Operational-semantics
          • Soundness
          • Release-notes
          • Workshops
          • ACL2-tutorial
          • Version
          • How-to-contribute
          • Acknowledgments
          • Using-ACL2
          • Releases
          • Pre-built-binary-distributions
          • Common-lisp
          • Installation
            • Obtaining-common-lisp
            • Installation-instructions
            • Using-ACL2
            • Installation-support
              • Creating-executable
              • Windows-installation
                • Windows-installation-gcl
              • Summary-of-ACL2-system-distribution
              • Running-ACL2-without-executable
          • Mailing-lists
          • Git-quick-start
          • Copyright
          • ACL2-help
      • Miscellaneous
      • Output-controls
      • Bdd
      • Macros
      • Installation
        • Obtaining-common-lisp
        • Installation-instructions
        • Using-ACL2
        • Installation-support
          • Creating-executable
          • Windows-installation
            • Windows-installation-gcl
          • Summary-of-ACL2-system-distribution
          • Running-ACL2-without-executable
      • Mailing-lists
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Installation-support

Windows-installation

Installing ACL2 on Windows

Windows users will probably want to do one of the following to install and run ACL2 on their systems. Thanks to David Rager for his help with this topic.

  • Use a Virtual Machine platform, such as VMware Player (free for non-commercial use) or Oracle Virtualbox (free even for commercial use) to install Linux, and then follow the normal installation-instructions to install ACL2. As of 2014, at least a couple of our power users are very happy with this solution, as it provides first-class access to utilities relevant to maintaining the ACL2 system and books (like GNU Make and perl).
  • Set up Windows Subsystem for Linux (WSL) on a 64-bit version of Windows 10 (or later, once available). Within that subsystem, follow the normal installation-instructions for ACL2. See the below section regarding the ACL2 Sedan Windows installation instructions for more info, as that involves installing the ACL2 Sedan in WSL on Windows.
  • Use the ACL2 Sedan (ACL2s) Windows installation instructions — see ACL2s::ACL2s-installation for more details. This will install ACL2 and the ACL2s system (including a copy of the Eclipse IDE with ACL2s support) in a Windows Subsystem for Linux distro. This distro is configured to automatically open Eclipse when the distro starts up, but one can start the distro without Eclipse by running wsl -d acl2s -e /bin/bash --noprofile.

You are welcome to obtain a Windows installer for a previous ACL2 release, which mimics some of Linux and provides Emacs. Updated ACL2 binaries have been successfully installed in such an environment.

When installing ACL2 on Windows without a Unix-like environment, consider at least downloading a utility such as djtarnt.exe to use with the -x option on gzipped tarfiles.

Gnu tar is preferred, as there have been some problems with long file names when using at least one other tar program. You may want to use the -i option, tar xpvfi ..., if you have problems with other than Gnu tar. You can see if you have Gnu tar by running tar -v.

WARNING: At least one user experienced CR/LF issues when using WinZIP, but we have received the suggestion that people untarring with that utility should probably turn off smart cr/lf conversion.

Here are links to some older documentation topics, possibly out of date, that provide additional information for installing ACL2 on Windows.

  • See windows-installation-gcl for building an executable image on a Windows system using GCL
  • Click here for some older instructions for building ACL2 on Windows.
  • Click here for yet older instructions for building ACL2 on Windows using mingw.

Subtopics

Windows-installation-gcl
Building an executable image on a Windows system using GCL