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"