RODIN Changelog

What's new in RODIN 2.8

Sep 12, 2013

679 Changes ignored in parameterized profile editor
680 Changes ignored when cell not validated.
678 NPE on click after root selection
655 Strange Indentation generated in Rodin Editor
658 Do not add empty comment attributes to Elements when editing
665 Save is not propagated among all instances of the editor
668 Rodin Editor allows the edition of read-only elements
669 Rodin Editor allows modifying the machine name and NPE occurs
670 The refresh action does not refresh the Rodin EMF model
664 Repeated undo/redo generates RodinDBException
672 NPE when refreshing Rodin Editor
677 Rodin elements are upside down in browser on Java 7
671 Expansion rules from imported theories not available
666 Support multiple lines for formulas in theory editor
651 Event-B Editor - toolbar for add/move buttons
657 Refreshing the Rodin Editor too often
654 Rodin editor updates markers repeatedly after re-generation of machine
656 Implicit elements in not extended events
661 SIMP_SPECIAL_EQUAL_RELDOM unsound
660 B2Latex does not show (not-)theorem status
659 B2Latex problems with witnesses
647 machine renaming and indexer
652 Multiple exceptions in EventB Explorer when updating with Teamwork
648 proving does not work with Ubuntu 64bit
635 Inconsistent result of formula type-checking
644 Coding error in BecomesSuchThat#getSyntaxTree
255 RODIN crash adding text to note or text box in class diagram
467 Problem with Software Sites

New in RODIN 2.0 RC1 (Sep 27, 2010)

General Interface:
Improved Statistic View. The statistic view was simplified and unified, to make it clearer and easily resizable and be displayed at first click on every element.
Modelling:
Mathematical Extensions. Rodin was extended to allow definition of basic predicates, new operators or new algebraic types.
Better platform's behaviour. Some cumbersome behaviours where improved:
It is now possible to display statistics for a project without expanding it first.
The view on selected hypotheses is now correctly scrolled to bottom, to display freshly added ones.
Navigating through proof tree nodes is faster (useless refreshings of search hypotheses where removed to gain performance).
Independent quantified variables with the same name. It is now possible to use the same name for quantified variables which are independant.
Improved WD Lemma Generation . The WD Lemma Generation was improved to simplify unnecessarily complicated lemmas.Some old proofs could appear as undischarged, the "Proof Replay on Undischarged POs" commmand will discharge these proofs.
Proving:
Project Explorer's Actions now able to run in background. The "Proof Replay on Undischarged POs", "Retry Auto Provers" and "Recalculate Auto Status" commands are now able to run in background. The user is allowed to modify his models, and do interactive proving while such commands are running. Note that the "Save" action on interactively proved PO, which is concerned by such a command, might be delayed as concurrency occurs. The "Save" action will then be scheduled as a further task to be performed, and the user will have to wait or cancel the command. Those commands are accessible by right-clicking in the Event-B Explorer.
Proof details can now be displayed. It is now possible for the user to have a look at what a proof rule really did. A new view, the Rule Details View, was added to the proving perspective to show up the various operations performed by a rule on a proof tree node. It is for example possible, now, to look at instantiated hypotheses, or even, find hypotheses that where removed or hidden by a rule.
Changes for plugin-developers:
Rodin 2.0 is Helios based. Rodin 2.0 is based on the Eclipse 3.6 Helios release. A wiki page has been added to document main improvements that could be of interest to plug-in developpers.
Rodin 2.0 is Java 1.6 based.
Simplified addition of tactic providers for the proving UI. A new attribute ("any") can now be used to describe the tactic providers that both apply on hypotheses and goal (i.e. that have the same behavior for both hypothesis predicates and goal predicate).
A new mechanism to collect informations while traversing formulae. The IFormulaInspector interface has been added and published in order to ease the aggregation of informations (of type F) computed while traversing the AST of a formula. This mechanism replace the old one, where one should retrieve positions where such informations could take place and iterate in a second time on each positions to calculate and accumulate informations.

RODIN Changelog

What's new in RODIN 2.8

New in RODIN 2.0 RC1 (Sep 27, 2010)

New in RODIN 1.3 (May 4, 2010)