• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • 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
          • 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
            • Match
            • ACL2s-faq
            • ACL2s-intro
            • ACL2s-defaults
            • Definec
            • ACL2s-utilities
            • ACL2s-interface
            • ACL2s-installation
              • ACL2s-installation-faq
                • ACL2s-installation-windows
                • ACL2s-installation-macos
                • ACL2s-installation-linux
                • ACL2s-updating-windows
                • ACL2s-updating-macos-or-linux
            • Talks
            • Nqthm-to-ACL2
            • Tours
            • Emacs
          • About-ACL2
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Mailing-lists
        • Interfacing-tools
      • Macro-libraries
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • ACL2s-installation

    ACL2s-installation-faq

    FAQ related to ACL2s installation

    FAQ

    If you are running into a problem on Windows that is not covered by the below FAQ items, please try removing your WSL acl2s installation and going back through the instructions, ensuring that the output that you see matches that shown in the installation video linked to in the installation instructions. Note that this will remove all of the data in the WSL installation, so be sure to backup any files inside it that you want to keep. You can remove your WSL Ubuntu installation by running
    wsl --unregister acl2s
    . Then, follow the installation instructions as normal, except that you do not need to reinstall Xming if you already have it installed.

    General FAQ

    • I already have a version of Eclipse installed for another class, can I use that?
      We do not support using an existing Eclipse installation. If you are using Windows, the version of Eclipse that we install will be kept separate from Eclipse that is installed directly on Windows (which is the typical configuration). If you are using macOS, then when installing Eclipse, you can drag and drop it to a different location than your existing Eclipse installation (for example, install Eclipse into a folder on your Desktop instead of to Applications). These two Eclipses will coexist peacefully, and will not interfere with each other.

    Windows FAQ

    • Double-clicking on run-acl2s.bat doesn't open a window, or just sits there forever without opening a window!
      Ensure that Xming is open and running (check your system tray by clicking on the ^ button on the bottom right corner of your screen). If it is, try exiting it (by right-clicking on the X icon and selecting "Exit") and reopening it by running the ACL2sXming xlaunch file. If that does not work, then ensure that Xming has permissions to use both private and public networks. You can do this by opening the Windows menu and searching for "Allow an app through Windows Firewall". In the window that comes up, scroll down to "Xming X Server" and ensure that the checkbox to the left of it and the two checkboxes to the right of it are all checked. You may need to click on the "Change settings" button at the top right of the window to be able to check the boxes.
    • Double-clicking on the ACL2sXming file doesn't do anything!
      If you have no other issues, this is OK. Double-clicking on the file will add an icon to your system tray (click on the ^ button near the bottom-right corner of your screen), but will not open a new window. If you are having problems, or if no X icon is added to your system tray, try downloading the ACL2sXming xlaunch file again, by right-clicking on the "here" link in the Windows installation instructions and choosing "Save Link As...".
    • When I try to start a session, Eclipse tells me that an error occurred and that it could not start a session!
      Ensure that you ran the wsl.sh script as a non-root user (see the Windows install instructions for more information)
    • In Windows, I can't find the folder that corresponds to my Eclipse workspace!
      1. Get the workspace path you chose for Eclipse (File → Switch Workspace → Other in Eclipse, and the path there will be whatever workspace you are currently using), which should look something like
        /mnt/c/...
        .
      2. Take that path and replace the /mnt/c/ with C:\, and replace all forward slashes / with back-slashes \.
      3. Open the Windows run dialog (Windows key + R) and enter the updated path, and then press enter.
      This will open the Windows folder that corresponds to your Eclipse workspace. You can then create a shortcut to this folder so it is easier to get to next time.
    • wsl works in an administrator terminal but not in a non-administrator one!
      Check that C:\Windows\system32 is in your Windows PATH. See this page for instructions on how to do this. Note that you may need to restart your computer after you modify your PATH for Windows to pick it up.

    macOS FAQ

    • When I run
      brew install acl2s/acl2s/acl2s --force-bottle
      , Homebrew tells me there is no bottle available!

      If you are on a M1/M2 Mac and you are not running macOS Ventura, you can either update to macOS Ventura and re-run the command, or you can build ACL2s from scratch, which will take a fair amount of time (at least an hour). To build ACL2s from scratch, run
      brew install acl2s/acl2s/acl2s
      .
      If you are on an Intel Mac and are running macOS Catalina or earlier, you can either update to macOS Big Sur or later (if that is supported on your computer), or build ACL2s from scratch using the instructions above.
    • Eclipse is using the dark theme, and I can't read any of the text!
      Go to Eclipse → Preferences → General → Appearance and select "Light" in the dropdown next to "Theme".
    • When I try to start a session, Eclipse tells me that an error occurred and that it could not start a session!
      Ensure that the
      brew install acl2s/acl2s/acl2s --force-bottle
      command succeeded. Try running it again to ensure that it worked.
    • When I try to run any of the brew commands, I get a message saying "command not found: brew".
      When you install brew, it sometimes will print out a message saying "Run these two commands in your terminal to add Homebrew to your PATH". If you don't run the two commands, Homebrew will not function correctly. Assuming you are on a M1/M2 Mac, try running the command
      echo 'eval $(/opt/homebrew/bin/brew shellenv)' >> ~/.zprofile
      and opening a new Terminal window.
    • When I double click on the Eclipse application, nothing happens!
      Ensure that you have Java installed. To check, open Terminal (e.g. by searching for it in Spotlight) and run java -version. If a version number is printed, you have Java installed.
    • When I double click on the Eclipse application, an error window opens that includes the text Code Signature Invalid or The application cannot be opened!
      This often occurs after installing or updating an Eclipse plugin and then rebooting your computer. The fix is to run the following command:
      codesign --force --deep --sign - /Applications/Eclipse.app
      If you have installed Eclipse in a different location or with a different name, you should replace /Applications/Eclipse.app with the path to the appropriate .app file. For more information about why this occurs, see this Eclipse issue.