New in Rodin 3.3.0 (Nov 26, 2017)
- Better support for the Theory plug-in:
- We have vastly improved the support for the Theory plug-in, which will allow to finally have a workable Theory plug-in compatible with Rodin 3.x.
- Improved interactive proving:
- The Generalized Modus Ponens reasoner no longer considers hidden hypotheses. This avoids leading the proof to a dead-end.
- The interface to external provers has been improved. Now, most mathematical extensions are translated to the external prover (e.g. as an uninterpreted function). This improves the rate of automated proofs when using theories.
- Better proof reuse:
- When a proof has become uncertain (colored in purple), the Rodin platform tries harder to salvage it by rebuilding a similar sound proof. This is particularly useful when restoring projects proved with an old version of Rodin (typically 2.x).
- Partial and total surjection shortcuts:
- Now, one can use the following shortcuts to enter the symbols for surjections:
- partial surjection: +>> and +->>
- total surjection: ->> and -->>
- Rule Details view gets refreshed:
- In some circumstances, the Rule Details view would not refresh in a timely fashion. One had to select another proof tree node, and then again the first node to trigger a refresh. Now, the view gets refreshed consistently as soon as the proof rule on the selected node changes.
- Changes for plug-in developers:
- Rodin 3.3 is built on top of Eclipse 4.6.2 (Neon), which requires Java 8. This shall not be an issue normally (Java is upward compatible), but can cause some glitch in places where code depends on the order of elements in a HashMap traversal, since the hashing algorithm is different.
- AST plug-in:
- The AST parser now supports infix binary relational predicates specified by the Theory plug-in. This allows to define new predicates looking like a = b.
- The ISpecialization class of the Event-B AST has been strengthened to detect more error cases (cases where the specialization would produce ill-typed formulas). It is thus not 100 % compatible with Rodin 3.2. But this should not be an issue in general.
- Event-B UI:
- The Rodin Math font is not loaded anymore during the startup of the Event-B UI plugin (this could cause deadlock).
- Rodin Editor:
- The enabling conditions for Rodin editor actions has changed from
- fr.systerel.editor.definition.inRodinEditor
- fr.systerel.editor.definition.editableStructuralMode
- which is more precise (and works around a bug in the previous condition).