• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
      • Start-here
        • Gentle-introduction-to-ACL2-programming
        • ACL2-tutorial
          • Introduction-to-the-theorem-prover
          • Pages Written Especially for the Tours
          • The-method
          • Advanced-features
          • Interesting-applications
          • Tips
          • Alternative-introduction
          • Tidbits
          • Annotated-ACL2-scripts
          • Startup
          • ACL2-as-standalone-program
          • ACL2-sedan
            • Defunc
            • Cgen
            • Ccg
            • Defdata
            • ACL2s-user-guide
            • ACL2s-tutorial
            • ACL2s-implementation-notes
            • ACL2s-faq
            • Match
            • ACL2s-intro
            • ACL2s-defaults
            • Definec
            • ACL2s-utilities
            • ACL2s-installation
              • ACL2s-installation-faq
              • ACL2s-installation-windows
                • ACL2s-installation-macos
                • ACL2s-installation-linux
            • Talks
            • Nqthm-to-ACL2
            • Emacs
          • About-ACL2
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • ACL2s-installation

    ACL2s-installation-windows

    Installation instructions for ACL2s on Windows

    Description

    To run ACL2s on Windows, we will use WSL (the Windows Subsystem for Linux). This allows us to run the Linux version of Eclipse and ACL2s on Windows machines.

    If you run into any issues, check out the ACL2s-installation-faq topic.

    Requirements

    • at least 8GB of free hard drive space
    • at least 4GB of RAM
    • Windows 10 version 21H1 or greater. Windows 11 may also work.

    Installation should take less than an hour, though installation time will depend on your computer's specs and on the speed of your internet connection. You can use your computer while the installation is occurring.

    Instructions

    1. Install WSL
      1. Open an administrator terminal (either CMD or Powershell). This can be done by opening the Windows menu at the bottom left hand side of the screen and searching for cmd. Then, right click on the "Command Prompt" item and select "Run as administrator".
      2. Run dism.exe /online /enable-feature /featurename:Microsoft-Windows-Subsystem-Linux /all /norestart
      3. Run dism.exe /online /enable-feature /featurename:VirtualMachinePlatform /all /norestart
      4. Restart your computer. Select "Update and Restart" in the power menu if it appears.
      5. Reopen an administrator terminal as you did previously and run wsl --update
    2. Download and set up the ACL2s WSL image
      1. Download distro.tar.gz to your Downloads folder.
      2. Open up a new non-admininistrator terminal by opening the Windows menu at the bottom left hand side of the screen and searching for cmd.
      3. Run mkdir C:\wslDistroStorage
      4. Run wsl --import acl2s C:\wslDistroStorage\acl2s Downloads\distro.tar.gz. Note that this may take a while, somewhere between 5 and 15 minutes. Disabling any virus scanners may significantly speed this up.
      5. Run wsl -d acl2s and confirm that you get some output (e.g. not a blank line). If so, you can close the terminal. Note that this may take some time and you may see some errors about DISPLAY first.
    3. Install Xming and launch it
      1. Download the installer here and run it.
      2. Do not uncheck the option to associate .xlaunch files with Xming during installation! Do uncheck the option to launch Xming after the installation is complete.
      3. Download our Xming launch profile here and put it somewhere memorable. You may need to right-click on the link and select "Save As..." if your browser doesn't download it automatically.
      4. Double click on our Xming launch profile to start Xming. If Windows asks you which networks you want to allow Xming to access, make sure you allow it to access both private and public networks.Note that double clicking on ACL2sXming.xlaunch will not open a new window. It will add an item to the system tray on the right-hand side of the task bar, and you may need to click on the up caret (^) to see it.
    4. Create a folder for your CS2800 files on your C: drive
      1. Open File Explorer, select "This PC" on the left, double click on "Local Disk (C:)", right-click on an empty area inside of that folder, and select "New Folder". Name the folder whatever you would like.
    5. Run Eclipse
      1. Download run-acl2s.bat and save it somewhere memorable. Note that depending on your browser, you might get a warning when you download this file, but you should click "Keep" or "Download Anyways".
      2. Double click on run-acl2s.bat to launch a WSL terminal and Eclipse. A window titled "Windows protected your PC" may appear. If so, click on "More info" and then "Run anyways" at the bottom of the window.
      3. When Eclipse asks for a workspace, enter /mnt/c/<FOLDER>, where <FOLDER> should be replaced with the name of the folder that you just created.
    6. Get started with Eclipse by working through the ACL2s-tutorial.