• 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-macos

    Installation instructions for ACL2s on macOS

    Requirements

    • at least 5GB of free hard drive space
    • at least 4GB of RAM
    • macOS Catalina (10.15), Big Sur (11), or Monterey (12)

    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.

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

    Instructions

    A video walking through installation is available here.

    1. Determine if your Mac uses an M1 processor and check your macOS version
      1. Click on the Apple icon at the top left of the screen and select "About This Mac". On the screen that pops up, check the text next to "Processor" or "Chip". If the text includes "Apple", you have an M1 processor in your Mac. Otherwise, if the text includes "Intel", you have an x86 Mac.
      2. In the "About This Mac" window, double check that you are running one of "macOS Catalina", "macOS Big Sur", or "macOS Monterey". If you are using a different version of macOS, you will likely need to use the Khoury Virtual Desktops Infrastructure (VDI).
    2. Install Homebrew
      1. Open the Terminal app, either by searching for it or via opening Finder and selecting Go -> Utilities in the menu bar, and opening Terminal in that folder.
      2. Go to brew.sh and copy-paste the command starting with /bin/bash on the top of that page into a Terminal window, then press enter. You only need to run that single command, and can safely ignore the other instructions on Homebrew's website. You may need to enter your password one or more times throughout the process.
    3. Tap and install ACL2s
      1. Run 
        brew tap mister-walter/acl2s
        and then 
        brew install acl2s --force-bottle
        inside of Terminal.
    4. Install Java
      1. Download and install Java 17 or 18. The easiest way to do this is to go to this link and download either the Arm64 DMG installer (if you are on a M1 Mac) or the x64 DMG installer. Then, open the DMG and run the installer inside of it.
    5. Install Eclipse
      1. Download the Eclipse version appropriate for your machine: M1 Mac or x86 Mac.
      2. Open the downloaded file and click and drag the Eclipse icon into your Applications folder.
      3. If you already have Eclipse installed, you should still install the version of Eclipse we provide here. If you need your existing Eclipse install for another class, you can install Eclipse for this class by dragging the Eclipse icon into a different folder (for example, a folder on your Desktop) rather than Applications.
    6. Install the ACL2s Eclipse Plugin
      1. Open Eclipse, either by searching for it or via opening Finder and selecting Go → Applications in the menu bar, and opening Eclipse in that folder.
      2. Select the folder that you want to keep all of your CS2800 ACL2 files in. You can use the default choice if you like. You may also want to check the box that says "Use this as the default and do not ask again". Then, click "Launch".
      3. In the menu bar, click on Help → Install New Software...
      4. Click on "Add..." in the screen that comes up. In the resulting window, enter ACL2s next to "Name:" and http://cs2800.atwalter.com/p2 next to "Location". Then, click "Add", which will close the pop-up.
      5. The middle of the window should now show "ACL2s Plugin Update Site". Click on the checkbox to the left of it and click "Next>" at the bottom of the window.
      6. In the next window, click "Finish" at the bottom right of the screen. If a pop-up appears that says "Trust" at the top and has two entries in a table at the top, click "Select All" and then "Trust Selected" at the bottom.
      7. After the installation is complete, Eclipse will ask you if you would like to restart Eclipse. Select "Restart Now". This will close Eclipse and reopen it.
    7. Get started with Eclipse by working through the ACL2s-tutorial.