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 because if 50 students try to download ACL2s at once, it will cripple the CCIS network.
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.
We will be using a virtual machine (VM). If you do not know what that is, find and read an introduction to virtual machines.
Installation instructions
Follow the installation instructions for your OS.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.
- 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
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.ping google.com - 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.