Logic and Computation
CS 2800 Spring 2022

Khoury College of Computer Sciences
Northeastern University
Installing ACL2s on Linux

Requirements

Instructions

These instructions are known to work on Ubuntu 20.04, and may work on other platforms as well. If you run into any issues, feel free to reach out to Drew.

  1. Ensure the following software is installed on your machine. If not, install using your Linux distribution's package manager.
    • Java 11 or greater (OpenJDK is fine too) (openjdk-11-jre or newer on Ubuntu)
    • git
    • curl
    • procps
    • file
    • "Development tools" (build-essential on Ubuntu)
    1. If you are on an older version of Ubuntu, you may need to install libswt-gtk-4-jni and xutils-dev as well.
  2. Install Homebrew
    1. Go to brew.sh and copy-paste the command starting with /bin/bash on the top of that page into a terminal shell, 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 a terminal. Do not follow any of Homebrew's suggestions regarding installing gcc.
  4. Install Eclipse
    1. Download our Eclipse archive and unpack it somewhere on your computer.
    2. Run Eclipse by running ./eclipse/eclipse from the directory that you unpacked the Eclipse package inside of.
  5. 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!