Installing ACL2s on Windows

Installation instructions

1. Install VirtualBox. This is the VM we will be using to run ACL2s. We recommended that you use version is 6.0.0 because we have tested with this version, so other versions may cause installation problems later.
2. Install the VirtualBox extensions. Maku sure the version number of the extension pack matches the version number of VirtualBox. 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 vagrant.The recommended version is Vagrant 2.2.3.
4. 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. 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.)
5. In the acl2s directory enter the following command (using an xterm/terminal/powershell)

   vagrant up

   This will take a while as various files are downloaded and your virtual machine is created. Do not close the VirtualBox until the process is done. If you get errors about VT-x being disabled, look see this. You have to enable virtualization technology in your bios.
6. Once the above finishes, log into your new machine (the VirtualBox VM window).

   login: vagrant
Password: vagrant


7. Now close VirtualBox using the "Power off machine" option.
8. Once VirtualBox is closed, bring it back up with the following command (using an xterm/terminal/powershell).

   vagrant up

9. Next, log into VirtualBox. Alternatively, see the XServer option.

   login: vagrant
Password: vagrant


   At the command line type

   startx

   This will open up a window manager Click on the "File System" icon, then "opt", then "eclipse" and then double-click (open) 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.

Xserver option

This is optional, but for those of you who you have an Xserver on your machine, such as Xming, you can run ACL2s using your Xserver, by typing the following commands in an xterm/terminal/powershell from the acl2 directory, instead of logging into the VM.

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