Difference between revisions of "Rodin Platform 1.2 Release Notes"
From Event-B
Jump to navigationJump to searchimported>Nicolas m (→Known Issues) |
imported>Pascal |
||
(17 intermediate revisions by 3 users not shown) | |||
Line 2: | Line 2: | ||
== What's New in Rodin 1.2? == | == What's New in Rodin 1.2? == | ||
− | + | * Event-B Editor | |
+ | :'''Section expanding'''. A preference has been added for section expanding (See "Window > Preferences > Event-B > Modelling UI"). More precisely, this new option allows to specify that the sections shall not be expanded when unfolding an element of the Event-B editor. By default, any section of an element is expanded (as in previous releases). | ||
+ | :'''Generated elements'''. The generated elements (''e.g.'', produced by UML-B or the decomposition plug-in) cannot be edited, and appear grayed in the Event-B editor. This feature concerns whole generated contexts/machines, as well as other Event-B elements such as events, variables, ... | ||
− | * [[ | + | * Proving Perspective |
+ | :'''Easily creating new projects or components'''. Shortcuts have been added to the "File > New" menu of the Proving perspective to create a new Event-B project or a new Event-B component. | ||
+ | :'''Copying from the proof skeleton to the proof tree'''. It is now possible to copy a subtree of a stored proof from the proof skeleton view to an edited proof tree. See also [[Proof_Skeleton_View#Copy.2FPaste_to_Proof_Tree | Copy/Paste to Proof Tree]]. | ||
+ | :'''Hypothesis View'''. A dropdown list is now included to the Hypothesis view, to toggle the "Consider hidden hypotheses" preference directly from the hypothesis view. A quick search field and its related buttons have been added. | ||
+ | |||
+ | * Rewriting Rules and Inference Rules | ||
+ | The existing rules have been reviewed and several implemented rules have been fixed. | ||
+ | :'''FIN_FUN1_R, FIN_FUN2_R, FIN_FUN_IMG_R, FIN_FUN_RAN_R and FIN_FUN_DOM_R'''. The well-definedness condition was not implemented. See also [[Inference_Rules | Inference Rules]]. | ||
+ | :'''DISTRI_RANSUB_BUNION_R, DISTRI_RANSUB_BINTER_R, DISTRI_DOMSUB_BUNION_L and DISTRI_DOMSUB_BINTER_L'''. These rules were wrongly defined and wrongly implemented. See the history of the [[Relation_Rewrite_Rules | Relation Rewrite Rules]] page for details. | ||
+ | |||
+ | * Migration to Eclipse 3.5 (Galileo) | ||
+ | :The extension point <tt>org.eclipse.core.contenttype.contentTypes</tt> is now used instead of the deprecated <tt>org.eclipse.core.runtime.contentTypes</tt>. | ||
+ | :The method "org.osgi.service.prefs.Preferences.flush" is used instead of the deprecated <tt>org.eclipse.core.runtime.Plugin.savePluginPreferences</tt>. | ||
* [[Predicate_variables|Predicate variables extension]] | * [[Predicate_variables|Predicate variables extension]] | ||
+ | :Added support for predicate variables in the AST library. | ||
− | * | + | * [[Generated Model Elements | Generated elements]] |
+ | :In the previous release, it was possible to mark an Event-B machine/context as generated, in order to prevent users from inadvertently modifying it. | ||
+ | :In this release, more fine-grained "read only" restrictions are enforced and any internal element may be tagged as generated (<tt>org.eventb.core.generated="true"</tt>). | ||
== Requirements == | == 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 | + | == External Plug-ins == |
{{TODO | Describe here the available plug-ins, and the supported versions for this release.}} | {{TODO | Describe here the available plug-ins, and the supported versions for this release.}} | ||
+ | * [[Decomposition_Release_History|Decomposition Plug-in 1.0]] | ||
+ | * [[Camille_Release_History|Camille Text Editor Plug-in 1.1]] | ||
+ | |||
+ | === 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 == | ||
− | + | [https://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/1.2/ Download Now!] | |
− | == Fixed | + | == Bugs Fixed and Feature Requests Implemented == |
− | + | ||
+ | Bug 1819316: Existential PO does not discharge | ||
+ | Bug 1820566: Problem with naming in Windows | ||
+ | Bug 1824569: Error Markers in Synthesis view do not update | ||
+ | Bug 1922694: Crazy Copy/Paste | ||
+ | Bug 1977355: Edit tab does not reflect changes made by other programs | ||
+ | Bug 2031274: Rename problem | ||
+ | Bug 2657540: Synthesis view: elements inverted | ||
+ | Bug 2815882: Primed identifiers are allowed | ||
+ | Bug 2818587: Machine renaming not propagated to extends clauses | ||
+ | Bug 2880858: Wrong arithmetic simplification | ||
+ | Bug 2883204: Symbols View not directly accessible | ||
+ | Bug 2884511: Rewritten formula should be type checked exception | ||
+ | Bug 2884753: Oftype makes assert exception errors in hypotheses page | ||
+ | Bug 2884774: No indication of Theorem guards in pretty print tab | ||
+ | Bug 2891365: Unexpected Error (possibly stack overflow) | ||
+ | Bug 2893379: Can't edit Refinement if var and event have the same name | ||
+ | Bug 2900389: Event-B keyboard does not translate "or" | ||
+ | Bug 2900456: Empty Goal Window | ||
+ | Bug 2901018: "distinct variable" requirement in lambda abstraction | ||
+ | Bug 2908239: id (identity function) ill-typed in rodin | ||
+ | Bug 2909409: Unavoidably too many open handles? | ||
+ | Bug 2916130: The lasso command selects hidden hypotheses | ||
+ | Bug 2931424: NPE in SearchHypothesis view | ||
+ | Bug 2936324: Extends clauses in pretty print | ||
+ | Bug 2938707: instable Event B machine editor (v1.2RC1) | ||
+ | Bug 2939467: SWTException: Graphic is disposed when saving proofs | ||
+ | Bug 2940139: org.eventb.core.seqprover.totalDom:0 unsound | ||
+ | Bug 2941295: Race condition in XProverCall and descendants | ||
+ | |||
+ | FR 1614997: Theorems following event guards | ||
+ | FR 1866809: Rewriting automatically dom(f) = S | ||
+ | FR 1942714: Set comprehension rewrite | ||
+ | FR 2073763: Support for "new" sets of relations | ||
+ | FR 2740294: Functions on finite set are finite | ||
+ | FR 2844800: Copy from Proof Skeleton to Proof Tree | ||
+ | FR 2922261: Launch prover(s) automatically on added hypothesis | ||
+ | FR 2937100: Traces for Simplification Rewriter | ||
+ | FR 2937127: Symbol Table view | ||
== Known Issues == | == Known Issues == | ||
− | |||
− | |||
* 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: | ||
-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner-1.9.0.14 | -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 | + | where "/usr/lib/xulrunner-1.9.0.14" must be replaced with your actual XULRunner 1.9.0 installation directory. |
* Using Rodin on GNOME desktop may result in a situation where buttons lock windows. To avoid this situation, it is needed to launch Rodin with | * Using Rodin on GNOME desktop may result in a situation where buttons lock windows. To avoid this situation, it is needed to launch Rodin with | ||
GDK_NATIVE_WINDOWS=1 /path_to_rodin/rodin | GDK_NATIVE_WINDOWS=1 /path_to_rodin/rodin | ||
− | It's a GTK bug, referenced for Eclipse at [[https://bugs.eclipse.org/bugs/show_bug.cgi?id=291257]] | + | It's a GTK bug, referenced for Eclipse at [[https://bugs.eclipse.org/bugs/show_bug.cgi?id=291257]]<br />See also [[Gnome and broken buttons]]. |
* 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: | ||
Line 41: | Line 103: | ||
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: | ||
+ | |||
+ | 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 1813657: Refactoring menu is not related to refactoring | ||
+ | Bug 1818464: Trivial PO does not discharge | ||
+ | Bug 1824177: B4free prover translation for <<-> fails | ||
+ | Bug 1841129: Incorrect proof status | ||
+ | Bug 1897572: Error in Proof Obligation Generator | ||
+ | Bug 1919546: P1,PP,M0-M3 not available as post tactic | ||
+ | Bug 1948095: importing existing projects | ||
+ | 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 2414463: Builder called on non-Rodin files | ||
+ | Bug 2433212: Poor performance under KDE | ||
+ | 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 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 2782243: BraveSansMono | ||
+ | Bug 2817523: No paste in root contextual menu of explorer | ||
+ | Bug 2824204: Change to Rodin Elements not reflected in editor | ||
+ | Bug 2827806: Zombie files in buffer | ||
+ | Bug 2835692: Text Editor exception | ||
+ | Bug 2836774: Text Editor unable to save (exception) | ||
+ | Bug 2844786: Invisible icons in Proof Control coolbar | ||
+ | Bug 2844797: The Proof Skeleton View does not adapt to the container | ||
+ | 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 2895507: MH and other rules are ill-defined | ||
+ | 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 | ||
+ | |||
+ | [http://sourceforge.net/tracker/?limit=10&func=&group_id=108850&atid=651669&status=1&artgroup=1050841&submit=Filter Post Release Bugs] | ||
[[Category:Rodin Platform Release Notes]] | [[Category:Rodin Platform Release Notes]] |
Latest revision as of 10:06, 28 July 2010
What's New in Rodin 1.2?
- Event-B Editor
- Section expanding. A preference has been added for section expanding (See "Window > Preferences > Event-B > Modelling UI"). More precisely, this new option allows to specify that the sections shall not be expanded when unfolding an element of the Event-B editor. By default, any section of an element is expanded (as in previous releases).
- Generated elements. The generated elements (e.g., produced by UML-B or the decomposition plug-in) cannot be edited, and appear grayed in the Event-B editor. This feature concerns whole generated contexts/machines, as well as other Event-B elements such as events, variables, ...
- Proving Perspective
- Easily creating new projects or components. Shortcuts have been added to the "File > New" menu of the Proving perspective to create a new Event-B project or a new Event-B component.
- Copying from the proof skeleton to the proof tree. It is now possible to copy a subtree of a stored proof from the proof skeleton view to an edited proof tree. See also Copy/Paste to Proof Tree.
- Hypothesis View. A dropdown list is now included to the Hypothesis view, to toggle the "Consider hidden hypotheses" preference directly from the hypothesis view. A quick search field and its related buttons have been added.
- Rewriting Rules and Inference Rules
The existing rules have been reviewed and several implemented rules have been fixed.
- FIN_FUN1_R, FIN_FUN2_R, FIN_FUN_IMG_R, FIN_FUN_RAN_R and FIN_FUN_DOM_R. The well-definedness condition was not implemented. See also Inference Rules.
- DISTRI_RANSUB_BUNION_R, DISTRI_RANSUB_BINTER_R, DISTRI_DOMSUB_BUNION_L and DISTRI_DOMSUB_BINTER_L. These rules were wrongly defined and wrongly implemented. See the history of the Relation Rewrite Rules page for details.
- Migration to Eclipse 3.5 (Galileo)
- The extension point org.eclipse.core.contenttype.contentTypes is now used instead of the deprecated org.eclipse.core.runtime.contentTypes.
- The method "org.osgi.service.prefs.Preferences.flush" is used instead of the deprecated org.eclipse.core.runtime.Plugin.savePluginPreferences.
- Added support for predicate variables in the AST library.
- In the previous release, it was possible to mark an Event-B machine/context as generated, in order to prevent users from inadvertently modifying it.
- In this release, more fine-grained "read only" restrictions are enforced and any internal element may be tagged as generated (org.eventb.core.generated="true").
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
TODO: Describe here the available plug-ins, and the supported versions for this release.
B Method Update Site
Downloading
Bugs Fixed and Feature Requests Implemented
Bug 1819316: Existential PO does not discharge Bug 1820566: Problem with naming in Windows Bug 1824569: Error Markers in Synthesis view do not update Bug 1922694: Crazy Copy/Paste Bug 1977355: Edit tab does not reflect changes made by other programs Bug 2031274: Rename problem Bug 2657540: Synthesis view: elements inverted Bug 2815882: Primed identifiers are allowed Bug 2818587: Machine renaming not propagated to extends clauses Bug 2880858: Wrong arithmetic simplification Bug 2883204: Symbols View not directly accessible Bug 2884511: Rewritten formula should be type checked exception Bug 2884753: Oftype makes assert exception errors in hypotheses page Bug 2884774: No indication of Theorem guards in pretty print tab Bug 2891365: Unexpected Error (possibly stack overflow) Bug 2893379: Can't edit Refinement if var and event have the same name Bug 2900389: Event-B keyboard does not translate "or" Bug 2900456: Empty Goal Window Bug 2901018: "distinct variable" requirement in lambda abstraction Bug 2908239: id (identity function) ill-typed in rodin Bug 2909409: Unavoidably too many open handles? Bug 2916130: The lasso command selects hidden hypotheses Bug 2931424: NPE in SearchHypothesis view Bug 2936324: Extends clauses in pretty print Bug 2938707: instable Event B machine editor (v1.2RC1) Bug 2939467: SWTException: Graphic is disposed when saving proofs Bug 2940139: org.eventb.core.seqprover.totalDom:0 unsound Bug 2941295: Race condition in XProverCall and descendants FR 1614997: Theorems following event guards FR 1866809: Rewriting automatically dom(f) = S FR 1942714: Set comprehension rewrite FR 2073763: Support for "new" sets of relations FR 2740294: Functions on finite set are finite FR 2844800: Copy from Proof Skeleton to Proof Tree FR 2922261: Launch prover(s) automatically on added hypothesis FR 2937100: Traces for Simplification Rewriter FR 2937127: Symbol Table view
Known Issues
- 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.
- Using Rodin on GNOME desktop may result in a situation where buttons lock windows. To avoid this situation, it is needed to launch Rodin with
GDK_NATIVE_WINDOWS=1 /path_to_rodin/rodin
It's a GTK bug, referenced for Eclipse at [[1]]
See also Gnome and broken buttons.
- 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. Information found there: [[2]]
- 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: [[3]]
- 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 1813657: Refactoring menu is not related to refactoring Bug 1818464: Trivial PO does not discharge Bug 1824177: B4free prover translation for <<-> fails Bug 1841129: Incorrect proof status Bug 1897572: Error in Proof Obligation Generator Bug 1919546: P1,PP,M0-M3 not available as post tactic Bug 1948095: importing existing projects 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 2414463: Builder called on non-Rodin files Bug 2433212: Poor performance under KDE 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 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 2782243: BraveSansMono Bug 2817523: No paste in root contextual menu of explorer Bug 2824204: Change to Rodin Elements not reflected in editor Bug 2827806: Zombie files in buffer Bug 2835692: Text Editor exception Bug 2836774: Text Editor unable to save (exception) Bug 2844786: Invisible icons in Proof Control coolbar Bug 2844797: The Proof Skeleton View does not adapt to the container 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 2895507: MH and other rules are ill-defined 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