Logic and Computation
CS 2800 Spring 2020

Khoury College of Computer Sciences
Northeastern University
Installing ACL2s on Mac

Installing ACL2s on Mac

Installation instructions

Note: You need about 9GB of free space on your hard drive to install and run the VM
  1. Install VirtualBox. This is the VM we will be using to run ACL2s. We recommended that you use version is 6.0.14 because we have tested with this version, so other versions may cause installation problems later. Similarly, the latest version 6.1 is not supported by vagrant, so do not use it.
    Note that on the latest version of OSX the installation may fail the first time you try it.
    To fix this, go to System Preferences -> Security & Privacy -> General tab and click the "allow" button at the bottom of the screen. This button should have some text to the left of it about Oracle Software. If you can't click on the button, you may need to unlock the settings (click on the lock icon). You may need to do something similar for any software you install.
  2. Install the VirtualBox extensions. Maku sure the version number of the extension pack matches the version number of VirtualBox. The above link is for 6.0.14. After downloading the file, you have to open VirtualBox and install the extensions. If you click on "Preferences" and "Extensions" you will see a green "+" icon that allows you to add extensions. Select the file you downloaded.
  3. Install Xquartz. Open Xquart and click on "Applications" and "Terminal" to open an xterm. Use this xterm for all the xterm commands we ask you to perform below.
  4. Install vagrant.The recommended version is Vagrant 2.2.6.
  5. Create a directory (if you do not know what this is, read an introduction to basic unix commands, as suggested above) on your machine, say acl2s, where you want ACL2s to reside. It is safest to put this directory right inside your home folder. Putting it on your Desktop or in your Documents or Downloads folders can cause problems with permissions in the latest OSX versions! Make sure there are no spaces in the full directory name. Place the following Vagrantfile. Rename the file to just Vagrantfile (do this in an xterm to make sure that that ".txt" extension is gone). In the same acl2s directory create a subdirectory with the name workspace. This will be a synced directory, allowing you to access your ACL2s files outside of the virtual machine. (Read about virtual machines if you do not know what a synced directory is.)
  6. In the acl2s directory enter the following command (using the xterm you opened previously)

    vagrant up

    This will take a while (~10 minutes) as various files are downloaded and your virtual machine is created. Do not close the VirtualBox or move on to the next step until the process is done. You will know the process is done when the terminal in which the vagrant up command was run prints your shell prompt again.
  7. Once the above finishes, start ACL2s by typing the following commands in the same xterm, from the acl2 directory (not the VirtualBox window).

    vagrant ssh -- -X
    eclipse

    If you get errors about not being able to set the display, then use the Startx Option. This error may occur when you change wireless networks and can often be fixed by restarting Xquartz and using a new xterm.
  8. Make sure that you choose the default workspace location so that the synced directories work mentioned above work. Also, when you close the VirtualBox machine choose the "Power off machine" option. You have other options, but this is the most robust.
  9. To restart ACL2s later follow the instructions above starting with the vagrant up step.

Startx Option

This is optional, but potentially useful if you have display problems with vagrant ssh. To run ACL2s inside the VM, then after following the above installion instructions.
  1. If the VM is not running, start it by going to the acl2s directory and enter the following command (using an xterm)

    vagrant up

    Then log into the VirtualBox VM window. If the text in the VM is very small, you can change the scaling of the virtual screen (View -> Virtual Screen 1 -> 200% (or whatever value you want)). You can also use the VirtualBox menu Machine, then Settings to chage display settings.

    login: vagrant
    Password: vagrant

    At the command line type

    startx

    This will open up a window manager Click on "eclipse.sh" on your desktop.
  2. Make sure that you choose the default workspace location so that the synced directories work mentioned above work. Also, when you close the VirtualBox machine choose the "Power off machine" option. You have other options, but this is the most robust.