#628 Lost Prove Tree after rebuild workspace


When using rodin to prove proof obligations, sometimes the prove tree will lost after rebuild.

The workspace is attached and you can reproduce the problem very easily.
There are one project in the workspace: MathematicalObjects.
There are 3 machines and 6 Theories in the project.
Some of the proof obligations are proved with the help of theories.

To reproduce the problem:
1. Initially all the proof obligations of the 3 machines are successfully proved.
2. Then I clean all the projects in the workspace. After rebuild, I deploy the 6 Theories.
3. A lot of previously proved proof obligations are now marked as unproved.

This bug was initially reported by Shawn Zhang <sure.zhang@gmail.com> on the user mailing list.

Unfortunately, an archive of the workspace is too large to be attached to this bug report. It is available from me.


  • Laurent Voisin

    Laurent Voisin - 2012-07-19

    A reduced archive has been attached to this bug report yesterday.


Log in to post a comment.

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:

JavaScript is required for this form.

No, thanks