• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
      • Break-rewrite
        • Monitor
        • Brr
        • Dmr
        • Break-lemma
        • Why-brr
        • Brr@
        • Brr-commands
        • Cw-gstack
        • Ok-if
        • Windows-installation
          • Unmonitor
          • Monitor!
          • Monitored-runes
        • Proof-builder
        • Accumulated-persistence
        • Cgen
        • Proof-tree
        • Forward-chaining-reports
        • Print-gv
        • Dmr
        • Splitter
        • Guard-debug
        • Set-debugger-enable
        • Redo-flat
        • Set-check-invariant-risk
        • Time-tracker
        • Removable-runes
        • Efficiency
        • Tail-biting
        • Failed-forcing
        • Sneaky
        • Invariant-risk
        • Failure
        • Measure-debug
        • Dead-events
        • Remove-hyps
        • Type-prescription-debugging
        • Pstack
        • Set-register-invariant-risk
        • Trace
        • Walkabout
        • Disassemble$
        • Nil-goal
        • Cw-gstack
        • Set-guard-msg
        • Find-lemmas
        • Watch
        • Quick-and-dirty-subsumption-replacement-step
        • Profile-all
        • Profile-ACL2
        • Set-print-gv-defaults
        • Minimal-runes
        • Spacewalk
        • Try-gl-concls
        • Near-misses
      • Projects
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Break-rewrite

    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.

    • Fetch the ACL2 Sedan (ACL2s) — see ACL2-sedan — which is an extension and distribution of ACL2 integrated with the Eclipse IDE. If you wish to use ACL2s without the Eclipse front-end, see the information about ACL2s in the installation instructions, which explains how to obtain and use a pre-built ACL2 binary for Windows, Linux, or Mac.
    • 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 on a 64-bit version of Windows 10 (or later, once available). Within that subsystem, follow the setup and installation instructions for ACL2. (You might be the first to test this, but it will likely work.)

    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.