Hi!
At the end of the class some of us were having problems with automatic proving in Rodin.
We were supposed to have installed Rodin Version: 3.4.0 and then install Atelier B Provers through "Help > Install New Software". I did that steps but it didn't work, Proof Obligations were still in brown.
I just tried to install again Atelier B Provers, and this time, a popup appear after agreeing terms of service asking if "I was really sure to install that software". This popup didn't appear in previous installations. After accepting (and a suggested restart), proofs were passing.
I don't know if this may be a solution for the ones who also have this same problem, but maybe double-checking that Atelier is installed can help.
Ignacio.
Just to make sure, these are my software versions: - Linux 5.5.5-arch1-1
_Name Version Id Provider_ Atelier B provers 2.2.1.r16701 com.clearsy.atelierb.provers.feature.group ClearSy Rodin Handbook v.2.5 2.5.0.201606291411 org.rodinp.handbook.feature.feature.group Formal Mind GmbH Rodin Platform 3.4.0.201802230927-6980ca1 org.rodinp.platform.product null Event-B Modeling Environment 3.4.0.201802230927-6980ca1 org.eventb.ide.feature.group ETH Zurich Rodin Platform Feature 3.4.0.201802230927-6980ca1 org.rodinp.platform.feature.group ETH Zurich
You can make sure of installed versions going to "Help > About Rodin Platform > Installation Details"