I'm getting the following error trying to install AlterierB from the Updates Help Window.
I'm using the last candidate realese (3.9) because the version 3.8 doesn't work on my Mac M2 amr64.
Cannot complete the install because some dependencies are not satisfiable
org.eclipse.equinox.p2.iu; com.clearsy.atelierb.provers.feature.group [2.3.0.r16736,2.3.0.r16736] cannot be installed in this environment because its filter is not applicable.
The update site I'm using is "Atelier B Provers - https://www.atelierb.eu/update_site/atelierb_provers"
for the rodin's : Rodin Plug-ins - https://rodin-b-sharp.sourceforge.net/updates
How can I fix this?
Do you use the x86 version of Rodin through Rosetta?
AtelierB provers are only distributed as x86 binaries, so they can't be installed on an ARM/Apple Silicon build of Rodin.
No, I don't.
Let me see if I can manage to install the x86 binaries. If you have some instructions for this, they're welcome.
I have an older Intel mac, but from what I've been told, you have to install an x86 version of Java and then you should be able to run an x86 Rodin.
However, someone else reported by email that the installation of AtelierB provers also fails with the x86 version of Rodin 3.9-rc1. We are investigating it.
If you want a stable and complete version of Rodin quickly, installing the x86 version of Rodin 3.8 is your safest bet.
Alright. I could install AtelierB provers on M2 and it was a bit trickier than expected.
- Install Java for arch-x86. For example, run in the terminal:
Then,
Now, dowload the x86 Rodin's version and assuming you copy-paste the .app to Applications.
No errors during the installation, all good. However, once it asks to restart Rodin, I got this in a fresh workspace, no project, no nothing.
Thanks for your detailed reports.
This is a known issue with the program checking the provers at startup (the first run of external programs can be much slower than the next ones due to various causes — the OS checking the binary, caches being empty, Rosetta doing some translation, and so on — so this first run timeouts and causes the error message, but there is nothing actually wrong).
The AtelierB provers should still work without any issue in actual proofs.
Here is a different, probably simpler, procedure to run the Intel version of Rodin (which can use AtelierB provers) on macs with Apple Silicon processors:
1. download https://github.com/adoptium/temurin17-binaries/releases/download/jdk-17.0.11%2B9/OpenJDK17U-jre_x64_mac_hotspot_17.0.11_9.pkg (it's a Java 17 runtime for Intel)
2. install it by double-clicking it; the Java runtime is installed in
/Library/Java/JavaVirtualMachines/temurin-17.jre
3. find the downloaded Rodin.app and modify
Rodin.app/Contents/Eclipse/rodin.ini
: add the next two lines just before the one with-vmargs
As with all other Rodin releases for mac, regardless of the processor type, one also needs to execute
xattr -rc Rodin.app
.