Rodin Platform 2.5 Release Notes

RODIN 2.5 is planned for April 30th.

N.B. Release notes are commented in this page.

What's New in Rodin 2.5?

TODO: PLANS ARE : consolidation and auto-tactics (programmatic) extensibility...

• General changes

This release mainly contains bug fixes and code consolidation.

• Changes for plugin-developers

• Dynamic auto tactic providers: enables to programmatically contribute additional auto tactics, making them available for selection in the combined profile editor. See extension point org.eventb.core.seqprover.autoTactics, element dynTacticProvider and interface org.eventb.core.seqprover.IDynTacticProvider.

• IUserSupport API simplification: some operations of the user support work only on the proof tree in main memory. Therefore, they cannot raise any RodinDBException, as they are not accessing the Rodin database at all. Therefore, all throws declaration for these methods have been removed. This change is fully binary compatible, as stated in §13.4.21 of the Java Language Specification 3.0, as throws declaration are checked only at compile time.

However, the default settings of the Java compiler will produce errors where one attempts to catch RodinDBException in places where these exceptions cannot occur. Consequently, when compiling against the new version of IUserSupport, you will have to remove catch blocks around these exceptions.

• Math Syntactical Groups: published enum org.eventb.core.ast.extension.StandardGroup that lists the syntactical groups in the mathematical language. Prefer referencing them instead of their ids as bare strings.

Requirements - Compatibility

• Configurations supported (and for which binaries are provided)
  • Linux 32-bit
  • Linux 64-bit
  • Windows 32-bit
  • Windows 64-bit
  • Mac 64-bit

• You need to have a Java JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE.

• To enhance your proving experience, the eclipse font settings (size, aspect...) are available from the preferences (General > Appearance > Colors and Fonts > Rodin). These settings allow you to modify the properties set on the Event-B Keyboard Text Font which is used in many views of the Proving UI. However, to enjoy these functionnalities, you need to install the Brave Sans Mono font on your system. You can download this font from the link here.

• Linux: the internal browser does not work with xulrunner-2.0 (for instance, it causes the welcome page to display a link instead of a html page and the Pretty Printer does not work); xulrunner-1.9.x must be installed.

• Linux 64-bit:

package 'libc6:i386' (and its dependencies) must be installed. For some distributions (Ubuntu <= 11.04 for instance), the package is 'ia32-libs'.

• Windows 64-bit:

Atelier B provers work more slowly; it can cause ML to not automatically discharge some sequents that it discharges on windows 32-bit, due to its timeout. A workaround is to download a custom profile: DefaultAuto_ML800, then Window > Preferences > Event-B > Sequent Prover > Auto/Post Tactic > Profiles (tab) > Import..., point to the downloaded file, 'Select All' profiles (there are 2), OK. Then in 'Auto/Post Tactic' tab, select 'Default Auto Tactic Profile (ML 800)' profile for auto-tactics. It is the same as the 'Default Auto Tactic Profile', except ML has a longer timeout (800 ms). You can of course change this timeout by editing the 'ML (800)' profile.

We have not noticed this problem for Linux 64-bit, nor for other platforms; however if you do, the same workaround applies.

TODO: VERIFY REQUIREMENTS ABOVE
TODO: Inform here of some specific system requirements (version of Java, etc).

External plug-ins

TODO: Link to the external page for plug-ins
Link of the form:

{{:Rodin_Platform_2.5.0_External_Plug-ins}}

Installing

TODO: Add here a link to download the platform.

Downloading

Download Rodin 2.5 now !

Upgrading from Rodin 2.4.x

Use the core update site:

• Window > Preferences > Install/Update > Available Software Sites:

remove Scala update site (no more exists): click "Scala" then "Remove" button, click "Yes" on the popup to confirm

add Core Rodin update site: click "Add..." button, enter a name ("Core Rodin Updates" for instance), then in "Location" put "http://rodin-b-sharp.sourceforge.net/core-updates"

click "OK"

• Help > Check for Updates:

"Checking for updates" appears with a progress bar, it can take a few minutes

Available updates lists the Handbook and the Rodin Platform, click "Next" twice

accept license agreements then click "Finish": the software is updating, which can take a few minutes

click "OK" if the security warning appears, then accept to "Restart Now"

Fixed Bugs

TODO: Add here a list of the fixed bugs.

Known Issues

TODO: COPY KNOWN ISSUES FROM PREVIOUS PAGES / VERIFY
TODO: Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.2).

Disclaimer

Since Rodin is continuously maintained, several unsoundness bugs which have been encountered were investigated and fixed. However, despite the total commitment of our teams to insure the soundness of the platform, some unexpected and unknown soundness issues could remain. We would be grateful if you would report these issues to the development mailing list.

About

Rodin Platform up to rxxxx.
Developer Release date : dd/mm/yyyy.
User Release date : dd/mm/yyyy.