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"
Another colleague (with a Mac) had a similar solution : wait until a dialog asking for a restart appears, and acknowledge.
PS I'm pretty sure the "sure to install unsigned software?" dialog should appear always.
Sent from phone. Please excuse brevity.
Manuel Carro IMDEA Software Institute, director software.imdea.org Assoc. professor, Tech. Univ. of Madrid - UPM www.upm.es
Sent from TypeApp
On Feb 26, 2020, 21:06, at 21:06, Ignacio Ballesteros i.ballesterosg@alumnos.upm.es wrote:
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