#830 atelierb installation fails

[Jonathan Prieto]

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?

[Guillaume Verdier]

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.

[Jonathan Prieto]

Do you use the x86 version of Rodin through Rosetta?

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.

[Guillaume Verdier]

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.

[Jonathan Prieto]

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:

arch -x86_64 zsh
curl -s "https://get.sdkman.io" | zsh
source ~/.sdkman/bin/sdkman-init.sh
sdk install java

Then,

 cat `which java` | file -
/dev/stdin: Mach-O 64-bit executable x86_64

Now, dowload the x86 Rodin's version and assuming you copy-paste the .app to Applications.

xattr -rc /Applications/rodin.app
arch -x86_64 
arch -x86_64 /Applications/rodin.app/Contents/MacOS/rodin

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.

[Guillaume Verdier]

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.

[Guillaume Verdier]

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

-vm
/Library/Java/JavaVirtualMachines/temurin-17.jre/Contents/Home/bin/java

As with all other Rodin releases for mac, regardless of the processor type, one also needs to execute xattr -rc Rodin.app.