[Rodin-b-sharp-devel] Severe issue in Rodin 2.5

[Laurent V. <lau...@sy...>]

Dear All,

I would like to let you know that Damien from Systerel recently discovered an important bug in Rodin 2.5.

This bug occurs when one proves a project and then later adds mathematical extensions to the project. In Damien's case, he replaced an old style enumerate using the partition operator by a datatype with one constructor for each enumerated value.

The consequence of the bug is that the proof status reported by the platform cannot be trusted anymore, even after cleaning the project.

I've open a bug report on SourceForge which states that there are two possibilities for solving this bug.  I would like to know which options are preferred by Rodin users and developers.

Please feel free to comment on the bug report.  See https://sourceforge.net/tracker/?func=detail&aid=3534337&group_id=108850&atid=651669 .

Cheers,
Laurent.