Difference between revisions of "Rodin Platform 1.3 Release Notes"

From Event-B
Jump to navigationJump to search
imported>Tommy
imported>Jens
 
(31 intermediate revisions by 5 users not shown)
Line 3: Line 3:
 
== What's New in Rodin 1.3? ==
 
== What's New in Rodin 1.3? ==
  
* Event-B Editor
+
* General Interface
:'''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.
+
: '''Error log view''' is now available among the other ''General'' views. It is accessible through ''Window'' > ''Show view'' > ''Error Log'' and shows the contents of the log file. This provides very useful informations to developers for correcting bugs, and is intended to be copy/pasted by users when posting bug reports.
  
:'''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.
+
* Modelling
 +
:'''Unified creation of new projects and event-B components'''. Whatever the way a "New" action is triggered ("File > New" in menubar, button in the toolbar, context menu or buttons in the "Event-B Explorer", etc.), the same wizard is used.
  
 +
:'''Easier renaming of modelling element labels'''. The "Rename" menu replaces the "Refactor" menu. Label prefixes can now be customized either globally (workspace scope) or locally (project scope).
 
:See also: [[Customize Prefixes]]
 
:See also: [[Customize Prefixes]]
  
* Proving Perspective
+
* Building
:'''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".
+
:'''Direct children processing only'''. Project subfolders and their contents are now considered non Rodin contents. As a consequence, models placed in subfolders are not checked for errors and no POs are generated for them.
 
+
 
 +
* Proving
 +
:'''A new "Replay Proof" command'''. A new "Proof Replay" command that tries to prove undischarged POs by reusing older proofs of these POs, when they exist. In former releases, it happened that one opened an undischarged PO and it was immediately proved. Then one had to manually go through all undischarged POs, just to see them in turn be proved. The "Proof Replay on Undischarged POs" command does it in a single step. It is accessible by a right-click in the Event-B Explorer.
 
:See also: [[Proof Obligation Commands]]
 
:See also: [[Proof Obligation Commands]]
 +
 +
: The '''simplification rewrites''' reasoner version has been incremented. As this reasoner is extensively used by auto provers, many proofs will be marked as broken after cleaning projects, but correct ones will replay successfully.
  
 
:'''NewPP'''. Changed the name displayed in proofs to "NewPP" to avoid ambiguity with "PP". It used to be displayed as "Predicate Prover".
 
:'''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
 
* 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.
+
:'''Added the origin of predicates in proofs'''. The origin of a predicate is its corresponding IAxiom, IInvariant, ... It can be fetched by <tt> predicate.getSourceLocation().getOrigin()</tt> where predicate is a hypothesis or goal of a proof sequent. Note: it works for root sequents only.
: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.
 
:'''Knowing nature of proof obligations'''. The nature of a proof obligation (Theorem, Well-Definedness, Invariant Preservation, ...) can be known from a IPOSequent.
Line 29: Line 31:
 
:'''NewPP Plug-in'''. The newPP tactic has been published. See PPCore#newPP()
 
:'''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.
+
:'''Added ExplorerPlugin#getSelectedStatuses()'''. Added a function ExplorerPlugin#getSelectedStatuses() to get currently selected POs.
  
 
:'''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.
 
:'''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.
Line 39: Line 41:
 
:''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.)
 
:''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 ==
+
== 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)]]
 
* [[Camille Editor | Camille Editor (version 1.1.4)]]
* [[Parallel_Composition_using_Event-B | Shared Event Composition plug-in (version 1.1.5)]]
+
* [[Parallel_Composition_using_Event-B | Shared Event Composition plug-in (version 1.1.6)]]
* [[Refactoring Framework | Refactory plug-in (version 0.0.6)]]
+
* [[Refactoring Framework | Refactory plug-in (version 0.0.8)]]
* [[Records Extension | Records Extension (version 0.2.0.beta)]]
+
* [[Decomposition Plug-in User Guide | Decomposition plug-in (version 1.0.2)]]
 +
* [[ProB]]
 +
 
 +
=== Rodin Update Site ===
 +
* [[UML-B_release_notes_for_1.1.0| UML-B (version 1.1.0)]]
 +
* [[UML-B_Statemachine_Animation_Release_History| UML-B - Statemachine Animation (version 1.0.1)]]
 +
* [[Event-BEMF_ReleaseHistory|Event-B EMF Framework ?]]
 +
* [[Feature_Composition_Release_History|Feature Composition Plug-in ?]]
 +
* [[Refactoring_Framework_Release_History|Refactoring Framework Plug-in (version 0.0.8)]]
 +
* [[Shared Event Composition_Release_History|Shared Event Composition Plug-in (version 1.1.6)]]
 +
* [[Decomposition_Release_History|Decomposition Plug-in (version 1.0.2)]]
 +
* [[Records Extension Release History | Records Extension (version ?.beta)]]
 +
 
 +
=== B Method Update Site ===
 +
* [http://bmethod.com/update_site/atelierb_provers Atelier B Provers]
 +
* [http://bmethod.com/update_site/b2rodin B2Rodin]
 +
* [http://bmethod.com/update_site/brama Brama]
  
 
== Downloading ==
 
== Downloading ==
Line 52: Line 67:
  
 
== Bugs Fixed and Feature Requests Implemented ==
 
== Bugs Fixed and Feature Requests Implemented ==
   Bug 1813657: Refactoring menu is not related to refactoring.
+
   Bug 1813657: Refactoring menu is not related to refactoring
   Bug 2945276: Rodin keyboard view displayed untimely.
+
  Bug 1818464: Trivial PO does not discharge
   Bug 2952087: Rodin 1.2 reuses erroneous Rodin 1.1 proof.
+
  Bug 1897572: Error in Proof Obligation Generator
   Bug 2952090: Added renaming of proof files.
+
  Bug 1919546: P1,PP,M0-M3 not available as post tactic
   Bug 2952705: Progress bar running too fast.
+
  Bug 1948095: importing existing projects
   Bug 2952959: Disabling auto-provers doesn't work.
+
  Bug 2414463: Builder called on non-Rodin files
 +
  Bug 2433212: Poor performance under KDE
 +
  Bug 2648946: Predicate Provers (newPP, P0) unable to discharge simple PO
 +
  Bug 2656831: saving proofs does not always work
 +
  Bug 2694492: proB widget do not display on second proB launch
 +
  Bug 2744052: NullPointerException in Builder on cyclic refinement
 +
  Bug 2782126: Your platform does not support SWT Browser widget.
 +
  Bug 2827806: Zombie files in buffer
 +
  Bug 2836774: Text Editor unable to save  (exception)
 +
  Bug 2844797: The Proof Skeleton View does not adapt to the container
 +
  Bug 2895507: MH and other rules are ill-defined
 +
   Bug 2945276: Rodin keyboard view displayed untimely
 +
   Bug 2952087: Rodin 1.2 reuses erroneous Rodin 1.1 proof
 +
   Bug 2952090: when renaming a context, the proofs are gone
 +
   Bug 2952143: EB-Editor refuses to save
 +
   Bug 2952959: Disabling auto-provers doesn't work
 +
  Bug 2958878: Associative Predicate does not accept <=>
 
   Bug 2961115: Pipe as internal name
 
   Bug 2961115: Pipe as internal name
 +
  Bug 2961857: p ∈ dom(prj1) causes internal error in New PP
 
   Bug 2962503: PPTrans throws NPE
 
   Bug 2962503: PPTrans throws NPE
 
   Bug 2962688: Clean with AutoProve on works the second time
 
   Bug 2962688: Clean with AutoProve on works the second time
   Bug 2977104: Editors still opened when deleting a project.
+
  Bug 2964353: Rule based prover does not properly match set extensions.
 +
  Bug 2964360: unsound inference rule
 +
  Bug 2976578: Invalid Thread Access in EventB Editor Manager
 +
   Bug 2977104: Editors still opened when deleting a project
 +
  Bug 2987050: Incoherences in proof statistics
 +
  Bug 2988112: Plugin not found on ProB update site
 +
  Bug 2990491: SM animation sub-folder breaks navigator for UML-B projects
  
   FR 2682079: Renaming issue.
+
  FR 1834561: auto-provers on discharged proof obligations
   FR 2926238: extensible pretty print.
+
  FR 1834715: Interactively proving A <<: B
   FR 2942210: Make SC symbolFactory visible.
+
  FR 1834725: copy and paste
   FR 2949606: Add a replay proof command in event-B explorer.
+
  FR 2543189: Rename proof file together with component
 +
   FR 2682079: Renaming issue
 +
  FR 2822916: How to add proof rules
 +
  FR 2891163: One Point on reversed equality
 +
   FR 2926238: extensible pretty print etc.
 +
   FR 2942210: Make SC symbolFactory visible
 +
  FR 2942231: provide child creation in attribute manipulator
 +
   FR 2949606: Add a replay proof command in event-B explorer
 +
  FR 2952709: Meaning of Retry auto-provers / Recalculate auto-status
 +
  FR 2979236: oftype everywhere
 +
  FR 2979325: Make symbolTable classes visible
 +
  FR 2979446: using a newly deployed theory without restart
 +
  FR 2990974: Error Log
  
 
== Known Issues ==
 
== Known Issues ==
{{TODO | Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.3).}}
+
[[https://sourceforge.net/tracker/?limit=100&func=&group_id=108850&atid=651669&assignee=&status=1&category=&artgroup=&submitter=&keyword=&artifact_id=&submit=Filter&mass_category=&mass_priority=&mass_resolution=&mass_assignee=&mass_artgroup=&mass_status=&mass_cannedresponse=|Open bugs page]]
  
 
* Early releases of XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). More recent releases fix this bug (works fine with xulrunner-1.9.1.7). Alternatively, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:
 
* Early releases of XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). More recent releases fix this bug (works fine with xulrunner-1.9.1.7). Alternatively, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:
Line 77: Line 127:
 
* A warning like the following one is displayed to the standard output when platform starts on GNOME desktop:
 
* A warning like the following one is displayed to the standard output when platform starts on GNOME desktop:
 
  (rodin:17254): GLib-WARNING **: g_set_prgname() called multiple times
 
  (rodin:17254): GLib-WARNING **: g_set_prgname() called multiple times
  It's a GNOME bug, referenced at: [[https://bugzilla.gnome.org/show_bug.cgi?id=563627]]
+
:It's a GNOME bug, referenced at: [[https://bugzilla.gnome.org/show_bug.cgi?id=563627]]
  
 
* The error log shows the following problem:
 
* The error log shows the following problem:
Line 83: Line 133:
 
  at org.eclipse.osgi.framework.internal.core.AbstractBundle.getResolverError(AbstractBundle.java:1313)
 
  at org.eclipse.osgi.framework.internal.core.AbstractBundle.getResolverError(AbstractBundle.java:1313)
 
  ...
 
  ...
It's an Eclipse 3.5 bug. Information found there: [[http://www.eclipse.org/forums/index.php?t=msg&goto=131264]]
+
:It's an Eclipse 3.5 bug. Information found there: [[http://www.eclipse.org/forums/index.php?t=msg&goto=131264]]
  
 
* The list of the currently open bugs is given below:
 
* The list of the currently open bugs is given below:
{{TODO | List open bugs}}
+
 
 +
  Bug 1441596: Tool conflicts caused by identically named files
 +
  Bug 1737819: WD properties are not fully propagated
 +
  Bug 1766826: Error messages from math parser incomprehensible
 +
  Bug 1824177: B4free prover translation for <<-> fails
 +
  Bug 1841129: Incorrect proof status
 +
  Bug 1949927: newPP is too sensitive to unused hyps
 +
  Bug 1954442: Too many handles used by Edit page on Windows
 +
  Bug 2082375: input file write-protection a problem to Rodin
 +
  Bug 2105507: too difficult to work with explicit set expressions
 +
  Bug 2174629: No PO generated for unrefined event
 +
  Bug 2371318: Unable to apply equality from left to right
 +
  Bug 2510307: Proof information window empty for grd/WD
 +
  Bug 2531738: RODIN crash adding text to note or text box in class diagram
 +
  Bug 2573332: Long formulas get truncated
 +
  Bug 2630205: reasoning with "finite" clause
 +
  Bug 2782243: BraveSansMono
 +
  Bug 2817523: No paste in root contextual menu of explorer
 +
  Bug 2824204: Change to Rodin Elements not reflected in editor
 +
  Bug 2835692: Text Editor exception
 +
  Bug 2844786: Invisible icons in Proof Control coolbar
 +
  Bug 2844813: Turnstile unicode character
 +
  Bug 2869663: Changing the font in the pretty print view
 +
  Bug 2871281: Bad display of marked math symbols
 +
  Bug 2871290: Comments are still editable in a generated model
 +
  Bug 2882318: Error while entering symbol from symbol table
 +
  Bug 2883199: Fix "new" actions
 +
  Bug 2886026: "Overflow" in partition rewriting
 +
  Bug 2893782: error when building new project with a context
 +
  Bug 2894645: Error on context named "axioms"
 +
  Bug 2900427: Event-B keyboard does not translate "or"
 +
  Bug 2916134: Atelier-B PP does not understand S /= {}
 +
  Bug 2931450: editor extension - clause names defined in wrong element
 +
  Bug 2934585: animB : impossible to start animation
 +
  Bug 2937124: Symbol Table and Properties
 +
  Bug 2937132: newPP unresponsive
 +
  Bug 2940315: mod operator should be compatible with itself
 +
  Bug 2940575: some fomulas are truncated
 +
  Bug 2941496: NewPP outputs incorrect set of required Hypotheses
 +
  Bug 2942182: unparsing then parsing gives a different expression
 +
  Bug 2949652: Event-B editor doesn't refresh
 +
  Bug 2952091: newPP is unsound
 +
  Bug 2952134: conversion to mathematical symbols generates trailing spaces
 +
  Bug 2952645: Unable to parse ||
 +
  Bug 2952705: Progress bar running too fast
 +
  Bug 2952758: Highlighting of bound variables
 +
  Bug 2957980: Proof Skeleton View : \n displayed as squares
 +
  Bug 2958877: {1 | true} --> Error Running Tool
 +
  Bug 2964346: RBP: illegal theory directory leads to strange behaviour
 +
  Bug 2964350: RBP allows to generate theory with same name as a context
 +
  Bug 2964359: Rule based prover allows me to define unsound rule
 +
  Bug 2968560: Dependence of Explorer & eventb.ui
 +
  Bug 2974863: Camille text editor -  Class cast exception when saving a sm
 +
  Bug 2974867: Camille text editor -  doesn't allow non alphanumeric chars
 +
  Bug 2979365: Auto completion in wizards
 +
  Bug 2979444: Matching ;
 +
  Bug 2987749: Axioms in classtypes not quantified
 +
  Bug 2988294: Nested elaborated transitions produce conflicting actions
 +
  Bug 2989932: SM translation flow-down buttons KO
 +
  Bug 2990934: UML-B Cannot add statemachines to refined Class
 +
  Bug 2991364: Project explorer jumps to first element
  
 
[[Category:Rodin Platform Release Notes]]
 
[[Category:Rodin Platform Release Notes]]

Latest revision as of 13:21, 28 July 2010

What's New in Rodin 1.3?

  • General Interface
Error log view is now available among the other General views. It is accessible through Window > Show view > Error Log and shows the contents of the log file. This provides very useful informations to developers for correcting bugs, and is intended to be copy/pasted by users when posting bug reports.
  • Modelling
Unified creation of new projects and event-B components. Whatever the way a "New" action is triggered ("File > New" in menubar, button in the toolbar, context menu or buttons in the "Event-B Explorer", etc.), the same wizard is used.
Easier renaming of modelling element labels. The "Rename" menu replaces the "Refactor" menu. Label prefixes can now be customized either globally (workspace scope) or locally (project scope).
See also: Customize Prefixes
  • Building
Direct children processing only. Project subfolders and their contents are now considered non Rodin contents. As a consequence, models placed in subfolders are not checked for errors and no POs are generated for them.
  • Proving
A new "Replay Proof" command. A new "Proof Replay" command that tries to prove undischarged POs by reusing older proofs of these POs, when they exist. In former releases, it happened that one opened an undischarged PO and it was immediately proved. Then one had to manually go through all undischarged POs, just to see them in turn be proved. The "Proof Replay on Undischarged POs" command does it in a single step. It is accessible by a right-click in the Event-B Explorer.
See also: Proof Obligation Commands
The simplification rewrites reasoner version has been incremented. As this reasoner is extensively used by auto provers, many proofs will be marked as broken after cleaning projects, but correct ones will replay successfully.
NewPP. Changed the name displayed in proofs to "NewPP" to avoid ambiguity with "PP". It used to be displayed as "Predicate Prover".
  • Changes for plugin-developers
Added the origin of predicates in proofs. The origin of a predicate is its corresponding IAxiom, IInvariant, ... It can be fetched by predicate.getSourceLocation().getOrigin() where predicate is a hypothesis or goal of a proof sequent. Note: it works for root sequents only.
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 currently selected POs.
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. /usr/local/rodin/rodin -vm /usr/lib/jvm/ia32-java-1.5.0-sun/bin/java (You have to adjust paths to your system.)

External Plug-ins

Rodin Update Site

B Method Update Site

Downloading

Download Now!

Bugs Fixed and Feature Requests Implemented

  Bug 1813657: Refactoring menu is not related to refactoring
  Bug 1818464: Trivial PO does not discharge
  Bug 1897572: Error in Proof Obligation Generator
  Bug 1919546: P1,PP,M0-M3 not available as post tactic
  Bug 1948095: importing existing projects
  Bug 2414463: Builder called on non-Rodin files
  Bug 2433212: Poor performance under KDE
  Bug 2648946: Predicate Provers (newPP, P0) unable to discharge simple PO
  Bug 2656831: saving proofs does not always work
  Bug 2694492: proB widget do not display on second proB launch
  Bug 2744052: NullPointerException in Builder on cyclic refinement
  Bug 2782126: Your platform does not support SWT Browser widget.
  Bug 2827806: Zombie files in buffer
  Bug 2836774: Text Editor unable to save  (exception)
  Bug 2844797: The Proof Skeleton View does not adapt to the container
  Bug 2895507: MH and other rules are ill-defined
  Bug 2945276: Rodin keyboard view displayed untimely
  Bug 2952087: Rodin 1.2 reuses erroneous Rodin 1.1 proof
  Bug 2952090: when renaming a context, the proofs are gone
  Bug 2952143: EB-Editor refuses to save
  Bug 2952959: Disabling auto-provers doesn't work
  Bug 2958878: Associative Predicate does not accept <=>
  Bug 2961115: Pipe as internal name
  Bug 2961857: p ∈ dom(prj1) causes internal error in New PP
  Bug 2962503: PPTrans throws NPE
  Bug 2962688: Clean with AutoProve on works the second time
  Bug 2964353: Rule based prover does not properly match set extensions.
  Bug 2964360: unsound inference rule
  Bug 2976578: Invalid Thread Access in EventB Editor Manager
  Bug 2977104: Editors still opened when deleting a project
  Bug 2987050: Incoherences in proof statistics
  Bug 2988112: Plugin not found on ProB update site
  Bug 2990491: SM animation sub-folder breaks navigator for UML-B projects
  FR 1834561: auto-provers on discharged proof obligations
  FR 1834715: Interactively proving A <<: B
  FR 1834725: copy and paste
  FR 2543189: Rename proof file together with component
  FR 2682079: Renaming issue
  FR 2822916: How to add proof rules
  FR 2891163: One Point on reversed equality
  FR 2926238: extensible pretty print etc.
  FR 2942210: Make SC symbolFactory visible
  FR 2942231: provide child creation in attribute manipulator
  FR 2949606: Add a replay proof command in event-B explorer
  FR 2952709: Meaning of Retry auto-provers / Recalculate auto-status
  FR 2979236: oftype everywhere
  FR 2979325: Make symbolTable classes visible
  FR 2979446: using a newly deployed theory without restart
  FR 2990974: Error Log

Known Issues

[bugs page]

  • Early releases of XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). More recent releases fix this bug (works fine with xulrunner-1.9.1.7). Alternatively, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:
-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner-1.9.0.14

where "/usr/lib/xulrunner-1.9.0.14" must be replaced with your actual XULRunner 1.9.0 installation directory.

  • A warning like the following one is displayed to the standard output when platform starts on GNOME desktop:
(rodin:17254): GLib-WARNING **: g_set_prgname() called multiple times
It's a GNOME bug, referenced at: [[1]]
  • The error log shows the following problem:
org.osgi.framework.BundleException: The bundle could not be resolved. Reason: Missing Constraint: Import-Package: org.eclipse.equinox.internal.util.event; version="1.0.0"
at org.eclipse.osgi.framework.internal.core.AbstractBundle.getResolverError(AbstractBundle.java:1313)
...
It's an Eclipse 3.5 bug. Information found there: [[2]]
  • The list of the currently open bugs is given below:
  Bug 1441596: Tool conflicts caused by identically named files
  Bug 1737819: WD properties are not fully propagated
  Bug 1766826: Error messages from math parser incomprehensible
  Bug 1824177: B4free prover translation for <<-> fails
  Bug 1841129: Incorrect proof status
  Bug 1949927: newPP is too sensitive to unused hyps
  Bug 1954442: Too many handles used by Edit page on Windows
  Bug 2082375: input file write-protection a problem to Rodin
  Bug 2105507: too difficult to work with explicit set expressions
  Bug 2174629: No PO generated for unrefined event
  Bug 2371318: Unable to apply equality from left to right
  Bug 2510307: Proof information window empty for grd/WD
  Bug 2531738: RODIN crash adding text to note or text box in class diagram
  Bug 2573332: Long formulas get truncated
  Bug 2630205: reasoning with "finite" clause
  Bug 2782243: BraveSansMono
  Bug 2817523: No paste in root contextual menu of explorer
  Bug 2824204: Change to Rodin Elements not reflected in editor
  Bug 2835692: Text Editor exception
  Bug 2844786: Invisible icons in Proof Control coolbar
  Bug 2844813: Turnstile unicode character
  Bug 2869663: Changing the font in the pretty print view
  Bug 2871281: Bad display of marked math symbols
  Bug 2871290: Comments are still editable in a generated model
  Bug 2882318: Error while entering symbol from symbol table
  Bug 2883199: Fix "new" actions
  Bug 2886026: "Overflow" in partition rewriting
  Bug 2893782: error when building new project with a context
  Bug 2894645: Error on context named "axioms"
  Bug 2900427: Event-B keyboard does not translate "or"
  Bug 2916134: Atelier-B PP does not understand S /= {}
  Bug 2931450: editor extension - clause names defined in wrong element
  Bug 2934585: animB : impossible to start animation
  Bug 2937124: Symbol Table and Properties
  Bug 2937132: newPP unresponsive
  Bug 2940315: mod operator should be compatible with itself
  Bug 2940575: some fomulas are truncated
  Bug 2941496: NewPP outputs incorrect set of required Hypotheses
  Bug 2942182: unparsing then parsing gives a different expression
  Bug 2949652: Event-B editor doesn't refresh
  Bug 2952091: newPP is unsound
  Bug 2952134: conversion to mathematical symbols generates trailing spaces
  Bug 2952645: Unable to parse ||
  Bug 2952705: Progress bar running too fast
  Bug 2952758: Highlighting of bound variables
  Bug 2957980: Proof Skeleton View : \n displayed as squares
  Bug 2958877: {1 | true} --> Error Running Tool
  Bug 2964346: RBP: illegal theory directory leads to strange behaviour
  Bug 2964350: RBP allows to generate theory with same name as a context
  Bug 2964359: Rule based prover allows me to define unsound rule
  Bug 2968560: Dependence of Explorer & eventb.ui
  Bug 2974863: Camille text editor -  Class cast exception when saving a sm
  Bug 2974867: Camille text editor -  doesn't allow non alphanumeric chars 
  Bug 2979365: Auto completion in wizards
  Bug 2979444: Matching ;
  Bug 2987749: Axioms in classtypes not quantified
  Bug 2988294: Nested elaborated transitions produce conflicting actions
  Bug 2989932: SM translation flow-down buttons KO
  Bug 2990934: UML-B Cannot add statemachines to refined Class
  Bug 2991364: Project explorer jumps to first element