View source for Rodin Platform 1.3 Release Notes

{{TOCright}}

== What's New in Rodin 1.3? ==

* Event-B Editor
:'''New in component popup menu'''. "New Event-B Project" and "New Event-B Component" wizards have been added to the "New" context menu of the event-B explorer. Right-clicking in a blank part or on a project in the Event-B explorer, a popup appears; then in the "New" section, these two actions are proposed.

:'''new preference/properties mechanism'''. A new preference/properties mechanism to handle and use prefix settings. It is now possible to set prefixes for a workspace scope or a project scope. Prefix settings are extended automatically by editor contributions.

:See also: [[Customize Prefixes]]

* Proving Perspective
:'''A new "Replay Proof" command'''. Right-clicking any element in the Event-B Explorer shows the contextual menu, which contains a new command "Proof Replay on Undischarged POs" next to "Retry Auto Provers" and "Recalculate Auto Status".
  
:See also: [[Proof Obligation Commands]]

:'''NewPP'''. Changed the name displayed in proofs to "NewPP" to avoid ambiguity with "PP". It used to be displayed as "Predicate Prover".

* Rodin Builder
:'''Direct children processing only'''. The builder now only processes direct children of project. Files located in subfolders are ignored.

* Changes for plugin-developers
:'''Added the origin of predicates in a proof'''. In the sequent of the root node of a IProofTree, the IAxiom, IInvariant, ..., a predicate (hypothesis or goal) comes from can be fetched through the origin of its source location.
:For instance: proofTree.getRoot().getSequent().goal().getSourceLocation().getOrigin()

:'''Knowing nature of proof obligations'''. The nature of a proof obligation (Theorem, Well-Definedness, Invariant Preservation, ...) can be known from a IPOSequent.
:See IPOGNature and IPOSequent#getPOGNature().

:'''NewPP Plug-in'''. The newPP tactic has been published. See PPCore#newPP()

:'''Added ExplorerPlugin#getSelectedStatuses()'''. Added a function ExplorerPlugin#getSelectedStatuses() to get the PS elements under the current explorer selection.

:'''Extensible pretty print'''. It is now possible to extend the pretty print page with the same kind of mechanism used to extend the structured editor.
:See also: [[Extending the Pretty Print Page]]

== Requirements ==
* It is recommended to run the Rodin platform with a Java 1.5 Runtime Environment. 
* Only a 32-bit version of the Rodin platform is provided. Some optional libraries dedicated to 32-bit support may be required in order to run it on a 64-bit OS. Moreover, you will have to install a 32-bit Java Virtual Machine (JVM), and then to set the -vm option to make sure that Rodin is run with the correct JVM.
:''eg.'' <tt>/usr/local/rodin/rodin -vm /usr/lib/jvm/ia32-java-1.5.0-sun/bin/java</tt> (You have to adjust paths to your system.)

== External plug-ins ==
{{TODO | Describe here the available plug-ins, and the supported versions for this release.}}
* [[UML-B - Statemachine Animation| UML-B - Statemachine Animation (version 0.1.3)]]
* [[UML-B | UML-B (version 1.0.1)]]
* [[Camille Editor | Camille Editor (version 1.1.4)]]
* [[Parallel_Composition_using_Event-B | Shared Event Composition plug-in (version 1.1.5)]]
* [[Refactoring Framework | Refactory plug-in (version 0.0.6)]]
* [[Records Extension | Records Extension (version 0.2.0.beta)]]

== Downloading ==
[https://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/1.3/ Download Now!]

== Fixed Bugs ==
{{TODO | Add here a list of the fixed bugs.}}

== Known Issues ==
{{TODO | Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.3).}}

[[Category:Rodin Platform Release Notes]]