Installing ACL2s

For this lab, you have to bring your laptop.

One of the goals is to get ACL2s installed. Installation instructions are shown below. Do not use the installation instructions from the ACL2s Web page!

Try to complete as many of the installation steps as you can before the lab.

Installation instructions

Follow the installation instructions for your OS.

• Linux installation
• Windows installation
• Mac installation

Getting Started with ACL2s

• Documentation on ACL2s can be found here. In particular, see the Get Set section on how to set up Eclipse.
• ACL2s is built on top of ACL2, which has extensive documentation. I suggest that you download a local copy of the documentation. Save and expand the documentation file in a convenient location which will make looking up documentation easier.
• Once you have ACL2s up and running, you should:
  • Use ACL2s to define some simple functions in ACL2s mode. Only use ACL2s mode.
  • Explore the ACL2s GUI and keyboard shortcuts.
  Information on how to do all of this is available from the ACL2s Web page.

Running ACL2s on Khoury Virtual Desktops

You can run ACL2s using the Khoury Virtual Desktops Infrastructure (VDI). See the documentation. You have many options including using an HTML client that allows you to log into a virtual machine and run ACL2s using a browser. Use your Khoury CS account credentials and select "CCIS-WINDOWS"; then select "Linux Lab" and you will see a Desktop. Use the file explorer and click on "Other Locations", "Computer", "bin" and then "acl2s". Drap the acl2s icon to your Desktop while holding "Alt" or "Option" (on Mac) and when you release it, a menu will pop up; select "link here" and you will have a direct link to ACL2s in your Desktop. Double click on the acl2s icon in your desktop and this will start ACL2s on your VM.

FAQ

If you are running into a problem on Windows that is not covered by the below FAQ items, please try removing your WSL Ubuntu 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 Ubuntu. Then, follow the installation instructions as normal, except that you do not need to reinstall Xming if you already have it installed.

General FAQ

• Why can't I access the Khoury VDI system?
  Ensure that you are connected to the Northeastern network, or are using the Northeastern VPN. You cannot connect to the VDI system from outside of Northeastern's network without using the VPN.
  Check that you are using your Khoury account credentials to log in, which may be different from your Northeastern account credentials.
• 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

• ./eclipse/eclipse 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...".
• wsl --install gives me an error!
  Try installing the "Ubuntu" app on the Windows App Store, and then running it (search for Ubuntu in the Start Menu). If this works, you do not need to run wsl --install.
• 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.

macOS FAQ

• When I run brew install acl2s --force-bottle , Homebrew tells me there is no bottle available!
  If you are on a M1 Mac and you are not running macOS Monterey, you can either update to macOS Monterey 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.
  If you are on an Intel Mac and are running macOS Mojava or earlier, you can either update to macOS Catalina 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 --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 Mac, try running the command echo 'eval $(/opt/homebrew/bin/brew shellenv)' >> ~/.zprofile and opening a new Terminal window.