		Search-engine friendly clone of the ACL2 documentation.

ACL2s-installation

ACL2s-installation-macos

Installation instructions for ACL2s on macOS

Requirements

at least 5GB of free hard drive space
at least 4GB of RAM
macOS Monterey (12), Ventura (13), or Sonoma (14) on a Mac with an Intel processor, or macOS Ventura (13) or Sonoma (14) on a Mac with an M1/M2 processor

Installation should take less than an hour, though installation time will depend on your computer's specs and on the speed of your internet connection. You can use your computer while the installation is occurring.

If you run into any issues, check out the ACL2s-installation-faq topic.

Instructions

A video walking through installation is available here.

Determine if your Mac uses an M1/M2 processor and check your macOS version
1. Click on the Apple icon at the top left of the screen and select "About This Mac". On the screen that pops up, check the text next to "Processor" or "Chip". If the text includes "Apple", you have an M1/M2 processor in your Mac. Otherwise, if the text includes "Intel", you have an x86 Mac.
2. In the "About This Mac" window, double check that you are running one of "macOS Monterey", "macOS Ventura", or "macOS Sonoma". If you are using a different version of macOS, you may need to build the ACL2s package from scratch on your machine, which will take some time.
Install Homebrew
1. Open the Terminal app, either by searching for it or via opening Finder and selecting Go -> Utilities in the menu bar, and opening Terminal in that folder.
2. Go to brew.sh and copy-paste the command starting with /bin/bash on the top of that page into a Terminal window, then press enter. You only need to run that single command, and can safely ignore the other instructions on Homebrew's website. You may need to enter your password one or more times throughout the process. If the installer tells you that you'll need to add a line to your .zprofile file, you should follow the instructions it provides to do this.
Tap and install ACL2s
1. Run
```
brew tap acl2s/acl2s
```
  and then
```
brew install acl2s/acl2s/acl2s --force-bottle
```
  inside of Terminal.
2. Note: if the above command fails with an error like --force-bottle passed but acl2s/acl2s/acl2s has no bottle!, then your macOS version is probably older than our supported version for your processor. If you can update your macOS version, you should do so. If you cannot update or do not wish to, please follow the instructions in the first entry of the macOS FAQ section of ACL2s-installation-faq.
3. Note: if you get command not found when running brew, you likely missed the instructions that the installer printed out when installing Homebrew. Run the following commend to resolve this:
```
echo 'eval $(/opt/homebrew/bin/brew shellenv)' >> $HOME/.zprofile && source $HOME/.zprofile
```
Install Java
1. Download and install Java 17 or 18. The easiest way to do this is to go to this link and download either the Arm64 DMG installer (if you are on a M1/M2 Mac) or the x64 DMG installer. Then, open the DMG and run the installer inside of it.
Install Eclipse
1. Download the Eclipse version appropriate for your machine: M1/M2 Mac or x86 Mac.
2. Open the downloaded file and click and drag the Eclipse icon into your Applications folder.
3. If you already have Eclipse installed, you should still install the version of Eclipse we provide here. If you need your existing Eclipse install for another class, you can install Eclipse for this class by dragging the Eclipse icon into a different folder (for example, a folder on your Desktop) rather than Applications.
Install the ACL2s Eclipse Plugin
1. Open Eclipse, either by searching for it or via opening Finder and selecting Go → Applications in the menu bar, and opening Eclipse in that folder.
2. Select the folder that you want to keep all of your CS2800 ACL2 files in. You can use the default choice if you like. You may also want to check the box that says "Use this as the default and do not ask again". Then, click "Launch".
3. In the menu bar, click on Help → Install New Software...
4. Click on "Add..." in the screen that comes up. In the resulting window, enter ACL2s next to "Name:" and https://cs2800.atwalter.com/p2 next to "Location". Then, click "Add", which will close the pop-up.
5. The middle of the window should now show "ACL2s Plugin Update Site". Click on the checkbox to the left of it as well as the "Handproof" item and click "Next>" at the bottom of the window.
6. In the next window, click "Finish" at the bottom right of the screen. If a pop-up appears that says "Trust" at the top and has two entries in a table at the top, click "Select All" and then "Trust Selected" at the bottom.
7. After the installation is complete, Eclipse will ask you if you would like to restart Eclipse. Select "Restart Now". This will close Eclipse and reopen it.
Re-sign the Eclipse app
- After installing or updating the ACL2s Eclipse plugin or any other plugin in Eclipse and rebooting your computer, you may get a popup saying "The application "Eclipse" can't be opened." the next time you open up Eclipse. To avoid this issue, or to fix it if it has already occurred, you should do the following:
- Run the following command in Terminal:
```
sudo codesign --force --deep --sign - /Applications/Eclipse.app
```
  Replace /Applications/Eclipse.app with the appropriate path to your Eclipse installation if you happened to move it or rename it.
- You may need to repeat the above command in the future if you run into the same issue again, regardless of whether or not you perform a plugin update. For more information about why this occurs, see this Eclipse issue.
Get started with Eclipse by working through the ACL2s-tutorial.