Installing ACL2s on Mac

Installation instructions

1. Install VirtualBox. This is the VM we will be using to run ACL2s. We recommend that you use the latest version. We tested it with version 6.0.10.
2. Install the VirtualBox Extension Pack. Make sure the version number of the extension pack matches the version number of VirtualBox. You can open the extension file directly with VirtualBox, or you can download it first, and then 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 extensions 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. We recommend that you use the latest version. We tested it with version 2.2.5.
5. Create a directory (if you don't 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. Make sure there are no spaces in the full directory name. Download this 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 as various files are downloaded and your virtual machine is created. On Stavros' desktop it took 30 mins and on his laptop it took a bit more than 1 hour. Be patient. Do not close your computer, nor the VirtualBox until the entire process is done.
7. Once the above finishes, log into your new virtual machine (the VirtualBox VM window).

   login: vagrant
Password: vagrant


8. Now close VirtualBox using the "Power off machine" option.
9. Once VirtualBox is closed, bring it back up with the following command (using the xterm you opened previously)

   vagrant up

   and start ACL2s by typing the following commands in the same xterm, from the acl2 directory (not the VirtualBox window).

   vagrant ssh -- -X
/opt/eclipse/eclipse


10. 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.
11. To restart ACL2s later follow the instructions above starting with the vagrant up step.