ACL2s-installation-faq
FAQ related to ACL2s installation
FAQ
If you are running into a problem on Windows that is not covered by
the below FAQ items, please try removing your WSL acl2s installation
and going back through the instructions, ensuring that the output that
you see matches that shown in the installation video linked to in the
installation instructions.
Note that this will remove all of the
data in the WSL installation, so be sure to backup any files inside it
that you want to keep. You can remove your WSL Ubuntu installation
by running
wsl --unregister acl2s
. Then, follow the
installation instructions as normal, except that you do not need to
reinstall Xming if you already have it installed.
General FAQ
- I already have a version of Eclipse installed for another
class, can I use that?
We do not support using an
existing Eclipse installation. If you are using Windows, the
version of Eclipse that we install will be kept separate from
Eclipse that is installed directly on Windows (which is the
typical configuration). If you are using macOS, then when
installing Eclipse, you can drag and drop it to a different
location than your existing Eclipse installation (for example,
install Eclipse into a folder on your Desktop instead of to
Applications). These two Eclipses will coexist peacefully, and
will not interfere with each other.
Windows FAQ
- Double-clicking on run-acl2s.bat
doesn't open a window, or just
sits there forever without opening a window!
Ensure
that Xming is open and running (check your system tray by
clicking on the ^ button on the bottom right corner of your
screen). If it is, try exiting it (by right-clicking on the X
icon and selecting "Exit") and reopening it by running the
ACL2sXming xlaunch file. If that does not work, then ensure that
Xming has permissions to use both private and public
networks. You can do this by opening the Windows menu and
searching for "Allow an app through Windows Firewall". In the
window that comes up, scroll down to "Xming X Server" and ensure
that the checkbox to the left of it and the two checkboxes to
the right of it are all checked. You may need to click on the
"Change settings" button at the top right of the window to be
able to check the boxes.
- Double-clicking on the ACL2sXming file doesn't do
anything!
If you have no other issues, this is
OK. Double-clicking on the file will add an icon to your system
tray (click on the ^ button near the bottom-right corner of your
screen), but will not open a new window. If you are having
problems, or if no X icon is added to your system tray, try
downloading the ACL2sXming xlaunch file again, by right-clicking
on the "here" link in the Windows installation instructions and
choosing "Save Link As...".
- When I try to start a session, Eclipse tells me that an error
occurred and that it could not start a session!
Ensure that
you ran the wsl.sh script as a non-root user (see the Windows
install instructions for more information)
- In Windows, I can't find the folder that
corresponds to my Eclipse workspace!
- Get the workspace path you chose for Eclipse (File → Switch
Workspace → Other in Eclipse, and the path there will be
whatever workspace you are currently using), which should look
something like
/mnt/c/...
.
- Take that path and replace the /mnt/c/
with C:\, and replace all forward
slashes / with back-slashes \.
- Open the Windows run dialog (Windows key + R) and enter the
updated path, and then press enter.
This will open the Windows folder that corresponds to your Eclipse
workspace. You can then create a shortcut to this folder so it is
easier to get to next time.
- wsl works in an administrator terminal
but not in a non-administrator one!
Check that C:\Windows\system32 is in your Windows PATH. See
this page
for instructions on how to do this. Note that you may need to restart
your computer after you modify your PATH for Windows to pick it up.
macOS FAQ
- When I run
brew install acl2s/acl2s/acl2s --force-bottle
, Homebrew tells me there is no bottle available!
If
you are on a M1/M2 Mac and you are not running macOS Ventura, you
can either update to macOS Ventura and re-run the command, or you
can build ACL2s from scratch, which will take a fair amount of
time (at least an hour). To build ACL2s from scratch, run
brew install acl2s/acl2s/acl2s
.
If you are on an Intel Mac and
are running macOS Catalina or earlier, you can either update to
macOS Big Sur or later (if that is supported on your computer),
or build ACL2s from scratch using the instructions above.
- Eclipse is using the dark theme, and I can't read any of the
text!
Go to Eclipse → Preferences → General → Appearance
and select "Light" in the dropdown next to "Theme".
- When I try to start a session, Eclipse tells me that an error
occurred and that it could not start a session!
Ensure that
the brew install acl2s/acl2s/acl2s --force-bottle
command
succeeded. Try running it again to ensure that it worked.
- When I try to run any of the brew commands, I get a message
saying "command not found: brew".
When you install
brew, it sometimes will print out a message saying "Run these
two commands in your terminal to add Homebrew to your PATH". If
you don't run the two commands, Homebrew will not function
correctly. Assuming you are on a M1/M2 Mac, try running the command
echo 'eval $(/opt/homebrew/bin/brew shellenv)' >> ~/.zprofile
and opening a new Terminal window.
- When I double click on the Eclipse application, nothing happens!
Ensure that you have Java installed. To check, open
Terminal (e.g. by searching for it in Spotlight) and run java -version. If
a version number is printed, you have Java installed.
- When I double click on the Eclipse application, an error window opens that includes the text Code Signature Invalid or The application cannot be opened!
This often occurs after installing or updating an Eclipse plugin and then rebooting your computer. The fix is to run the following command:
codesign --force --deep --sign - /Applications/Eclipse.app
If you have installed Eclipse in a different location or with a different name, you should replace /Applications/Eclipse.app with the path to the appropriate
.app file. For more information about why this occurs, see this Eclipse issue.