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"

cbc mailing list
cbc@software.imdea.org
https://software.imdea.org/mailman/listinfo/cbc