Logic and Computation
CS 2800 Spring 2022

Khoury College of Computer Sciences
Northeastern University
Installing ACL2s on macOS

Requirements

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

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. 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 "Warning: Installing unsigned software for which the authenticity or validity cannot be established. Continue with installation?", click "Install anyway".
    7. After the installation is complete, Eclipse will ask you if you would like to restart Eclipse Platform. Select "Restart Now". This will close Eclipse and reopen it.
  7. Get started with Eclipse
    1. Create a new Eclipse project by selecting New -> Project… -> General -> Project and giving it a name (whatever you would like)
    2. Right click on the project on the left hand side of the screen and select New -> Other… -> ACL2s -> ACL2s/Lisp file. Change the name of the file if you'd like, and leave the rest of the settings untouched. Click "Finish".
    3. Click on the green "play" button at the top of the screen: Image of the ACL2s Session Start button Eclipse will ask you if you want it to certify system books; click "Yes".
    4. After Eclipse pops up a window saying that certification is done, click on the green "play" button again.
    5. Type (+ 1 1) in the .lisp file that you created, and click on the icon with the single down arrow at the top of the screen. Confirm that 2 is eventually shown in the .lisp.a2s file that Eclipse generated. If so, your installation is working!