Lab 1: Install ACL2s

For this lab, you have to bring your laptop.

The main goal of this lab 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 because if 50 students try to download ACL2s at once, it will cripple the CCIS network. Your objective should be to finish installing ACL2s on your own before the lab. If you do that and you get the sample hello.lisp ACL2s file running, you should be fine, in that case you don't need to come to the lab.

If you are not already familiar with basic unix commands, find and read one of the many online tutorials so that you can create directories, rename files, etc. from an xterm/console.

Installation instructions

Follow the installation instructions for your OS.

• Linux installation
• Mac installation
• Windows installation
• I prefer to use ACL2s by logging into a Northeastern server

Once you are done with the steps above, you should be running an Eclipse window in your VM. Follow then the steps below to do a basic test of your installation. For more details on how to use ACL2s, stay tuned in this course, or see the "Getting started" section below.

1. Create a new project in Eclipse: File → New → Project → General → Project → Next → Use default location and type project name, say fooproject. This should create a new directory fooproject under the workspace directory above.
2. On the host machine (not the VM) download this hello.lisp file and place it in the workspace/fooproject/ directory.
3. Go back to Eclipse and right-click on the fooproject on the list of projects to the left, then hit "Refresh". Now you should see the file hello.lisp listed under the project.
4. Open the file and follow its instructions to run it through ACL2s.

Are you done with all steps above? Congrats! Here's some useful tips on using the VM:

• To enable copy-paste between the VM and the host, select Devices → Shared clipboard → Bidirectional
• Using alt-tab while on the VM switches between the windows running on the VM. If you want to switch between the VM window itself and other windows running on the host, first press the right control key, then alt-tab.

FAQ

• The resolution of eclipse is horrible. What can I do?
  Adjust your display settings as described here.
• I did not follow the installation instructions/I am in a weird state. What should I do?
  Just start over and go through the instructions carefully. Delete the whole directory with the ACL2s installation and start again. Make sure to download the Vagrantfile again in case you have an old version.
• I am getting error messages about permissions. What should I do?
  Make sure you have administrative permissions so that you can install software on your machine.
• I tried to install ACL2s on a Mac in the /Applications directory. It isn't working; what should I do?
  Install ACL2s in your home directory (say in Desktop) because installing software in /Applications/ on a Mac involves extra work.
• When I try saving the state of the VM, I get errors when I try to start it up again. Now what?
  Just use the "Power off machine" option. It is more stable and that should resolve your issues.
• How do I use the synced workspace directory?
  Only create directories in workspace using ACL2s because eclipse will not recognize a project directory it did not create. Once you create a project directory, you can add files to the directory from you OS using the synced directory. Don't add files to the workspace directory from your OS in any other way! Once you have added files (say homework files you downloaded), then in eclipse, in the project explorer, refresh the project and you will now see and will be able to access the files you added.
• VirtualBox is telling me that there is a new version of a box. What should I do?
  The box ubuntu/bionic64 gets updated routinely, but there is no reason for you to upgrade, destroy or recreate the machine. Assuming you have a working installation, there is no need to update unless we explictly tell you to do so.
• I tried everything and I am getting timeout error messages.
  Make sure that your VM can access the network. A firewall or some other kind of software you have installed may be stopping VirtualBox from accessing the internet. You can check if you have internet access by logging into your VM and typing

  ping google.com

  If you see timeout messages that means you do not have networking capabilities. How to resolve this depends on your configuration and is not something we can help you with.
• I am getting errors about VT-x being disabled. What should I do?
  You have to to enable virtualization technology in your bios. See the Windows installation instructions.
• Once the VM starts I am getting an empty screen. How can I login?
  This seems to happen sometimes when the VM window is maximized. Take its window out of maximized mode, and you should see the login option. Login and then you can maximize it again.

Getting Started with ACL2s

• Documentation on ACL2s can be found here.
• ACL2s is built on top of ACL2, which itself 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.