Rodin Platform 2.4 Release Notes - Revision history

imported>Tommy: /* Requirements - Compatibility */

2012-03-01T08:35:43Z

Requirements - Compatibility

← Older revision		Revision as of 08:35, 1 March 2012
Line 24:		Line 24:
	== Requirements - Compatibility ==		== Requirements - Compatibility ==

	* ~~Configuration~~		* Configurations supported (and for which binaries are provided)
	** Linux 32-bit		** Linux 32-bit
	** Linux 64-bit		** Linux 64-bit

imported>Nicolas: /* Requirements - Compatibility */

2012-02-03T13:48:28Z

Requirements - Compatibility

← Older revision		Revision as of 13:48, 3 February 2012
Line 31:		Line 31:
	** Mac 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.		* 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 [http://sourceforge.net/projects/rodin-b-sharp/files/Font_%20Brave%20Sans%20Mono/0.12/ here].		* 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 [http://sourceforge.net/projects/rodin-b-sharp/files/Font_%20Brave%20Sans%20Mono/0.12/ here].

imported>Nicolas: /* What's New in Rodin 2.4? */

2012-02-03T13:40:11Z

What's New in Rodin 2.4?

← Older revision		Revision as of 13:40, 3 February 2012
Line 16:		Line 16:
	:'''Auto Tactic''': a new tactic combinator 'Attempt after Lasso' is available in Auto Tactic profile editor.		:'''Auto Tactic''': a new tactic combinator 'Attempt after Lasso' is available in Auto Tactic profile editor.
	:'''Import/export profiles''': from the tactic preference page, profiles can be exported and imported to/from the file system		:'''Import/export profiles''': from the tactic preference page, profiles can be exported and imported to/from the file system
	:'''Preference Scope''': the ~~shorcut~~ to Auto Tactic Preference in Proof Control now indicates whether the current project has specific tactic settings or uses the global workspace settings		:'''Preference Scope''': the shortcut to Auto Tactic Preference in Proof Control now indicates whether the current project has specific tactic settings or uses the global workspace settings

	* Changes for plugin-developers		* Changes for plugin-developers

imported>Nicolas: /* What's New in Rodin 2.4? */

2012-02-03T11:09:36Z

What's New in Rodin 2.4?

← Older revision		Revision as of 11:09, 3 February 2012
Line 3:		Line 3:
	== What's New in Rodin 2.4? ==		== What's New in Rodin 2.4? ==

	From this release on, the Rodin platform is also provided for 64-bit Windows and Linux OSes.		From this release on, the Rodin platform is also provided for [[Rodin 64 bit\|64-bit]] Windows and Linux OSes.

	* Modelling		* Modelling

imported>Nicolas: /* Requirements - Compatibility */

2012-02-02T11:48:38Z

Requirements - Compatibility

← Older revision		Revision as of 11:48, 2 February 2012
Line 36:		Line 36:

	* 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: 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 ia32-libs (and its dependencies) must be installed.

	* Windows 64-bit:		* Windows 64-bit:

imported>Nicolas: /* Upgrading from Rodin 2.3.x */

2012-02-02T10:58:35Z

Upgrading from Rodin 2.3.x

← Older revision		Revision as of 10:58, 2 February 2012
Line 44:		Line 44:

	=== Upgrading from Rodin 2.3.x ===		=== Upgrading from Rodin 2.3.x ===

			Note: if you installed the Rodin Editor in Rodin 2.3, you have to uninstall it before upgrading to Rodin 2.4. The Rodin Editor is now part of Rodin 2.4 and it will be installed during the upgrade.

	Use rodin-2.4-repo.zip:		Use rodin-2.4-repo.zip:

imported>Nicolas: /* Known Issues */

2012-02-01T17:23:31Z

Known Issues

← Older revision		Revision as of 17:23, 1 February 2012
Line 88:		Line 88:

	== Known Issues ==		== Known Issues ==

			Bug 1441596: Tool conflicts caused by identically named files
			Bug 1824177: B4free prover translation for <<-> fails
			Bug 1949927: newPP is too sensitive to unused hyps
			Bug 1954442: Too many handles used by Edit page on Windows
			Bug 2531738: RODIN crash adding text to note or text box in class diagram
			Bug 2573332: Long formulas get truncated
			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 2844813: Turnstile unicode character
			Bug 2869663: Changing the font in the pretty print view
			Bug 2882318: Error while entering symbol from symbol table
			Bug 2883199: Fix "new" actions
			Bug 2894645: Error on context named "axioms"
			Bug 2900427: Problems parsing complex expressions
			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 2952134: conversion to mathematical symbols generates trailing spaces
			Bug 2952705: Progress bar running too fast
			Bug 2952758: Highlighting of bound variables
			Bug 2957980: Proof Skeleton View : \n displayed as squares
			Bug 2968560: Dependence of Explorer & eventb.ui
			Bug 2974867: Camille text editor - doesn't allow non alphanumeric chars
			Bug 2987749: Axioms in classtypes not quantified
			Bug 2988294: Nested elaborated transitions produce conflicting actions
			Bug 2997510: undo behaviour
			Bug 3005167: Inherited elements
			Bug 3005170: Becomes such that
			Bug 3005202: Renaming and provers
			Bug 3005204: Cumbersome popup
			Bug 3007792: Theorems in Guards - Syntax Error
			Bug 3007793: Issue with refines clauses of events
			Bug 3009555: Search Hypothesis refresh
			Bug 3009838: Order of variables and invariants not preserved
			Bug 3014775: partition operator is not accepted by Camille
			Bug 3019063: Error on Double Click
			Bug 3020776: Issue with indentation
			Bug 3022742: Problem with Software Sites
			Bug 3024811: Leaks in Event-B Explorer
			Bug 3052238: Saving failed caused by AssertionError in rebuild
			Bug 3054228: Proof simplification too slow
			Bug 3075420: Unable to save project after renaming invariants
			Bug 3085129: Rename file and update occurrences can fail
			Bug 3086511: camille editor refuses to save
			Bug 3086755: Tacticals are not cancelable
			Bug 3106603: Theory plugin inherits unsoundness bug from rbp
			Bug 3106789: Rule based prover does not properly match set extensions
			Bug 3112508: Camille can not be installed on Rodin 2.0.1
			Bug 3112539: Proof status after theory change
			Bug 3122147: newPP can't do modus ponens
			Bug 3126433: the parser accepts a+-1
			Bug 3151805: inconsistencies in importing of events
			Bug 3154319: Unacceptable handling of unsupported expressions
			Bug 3164791: Error and missing page in help contents
			Bug 3166636: newPP unable to reason with finite definition
			Bug 3206302: Records plugin: sloppy type checking with nasty consequences
			Bug 3216967: No AtelierB tactics if user profiles before installation
			Bug 3234433: Internal name collisions
			Bug 3275889: Heterogenous cursors in proving GUI
			Bug 3275897: scrolling too slow in Search Hypothesis view
			Bug 3275902: Navigation in yellow boxes
			Bug 3314101: Camille NullPointer
			Bug 3325133: Silent java.lang.Exception when expanding a project
			Bug 3354151: Theorems in event guards not supported
			Bug 3354372: I can't type "<=v"!
			Bug 3379632: useless missing hypotheses prevent replay
			Bug 3382200: POs do not appear under model nodes in explorer
			Bug 3383270: Prover UI editor improperly registered
			Bug 3384700: Statistics view counts POs only from contexts and machines
			Bug 3385671: Vanishing proof work
			Bug 3392038: Rodin Editor does not handle contributed attributes
			Bug 3419497: Hypothesis cache updated too often
			Bug 3429766: Contents in Symbol palette becomes invisible when scrolling
			Bug 3430133: The working area doesn't automatically scroll
			Bug 3440270: java heap space
			Bug 3440688: Camille editor : Save Failed -1
			Bug 3454414: Problems when merging events
			Bug 3459295: Camille Editor : guards/theorem
			Bug 3469731: Rodin crashes when adding an extends clause in Camille
			Bug 3472979: B2Latex doesn't handle more than one paragraph in a Comment
			Bug 3473014: B2LaTeX doesn't escape maths symbols in comments
			Bug 3473022: B2LaTeX silently produces nothing

	[https://sourceforge.net/tracker/?group_id=108850&atid=651669&status=1 Bugs on SourceForge]		[https://sourceforge.net/tracker/?group_id=108850&atid=651669&status=1 Bugs on SourceForge]

imported>Nicolas: /* Fixed Bugs and Implemented Feature Requests */

2012-02-01T17:22:11Z

Fixed Bugs and Implemented Feature Requests

← Older revision		Revision as of 17:22, 1 February 2012
Line 75:		Line 75:
	== Fixed Bugs and Implemented Feature Requests ==		== Fixed Bugs and Implemented Feature Requests ==

			Bug 2105507: too difficult to work with explicit set expressions
			Bug 3027387: Proof simplification does not remove useless rules
			Bug 3384398: ML unsound
			Bug 3419467: Decorate closed project !
			Bug 3422250: True and false symbols fail to parse in init action
			Bug 3423068: Class cast exception in OnePointRule
			Bug 3441526: Wrong WD for COND
			Bug 3469348: Bug in INITIALISATION FIS PO
			Bug 3478644: Missing WWD PO

			FR 3092835: search function in goal window

	== Known Issues ==		== Known Issues ==

imported>Nicolas: /* Requirements - Compatibility */

2012-02-01T15:57:03Z

Requirements - Compatibility

← Older revision		Revision as of 15:57, 1 February 2012
Line 35:		Line 35:
	* 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 [http://sourceforge.net/projects/rodin-b-sharp/files/Font_%20Brave%20Sans%20Mono/0.12/ here].		* 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 [http://sourceforge.net/projects/rodin-b-sharp/files/Font_%20Brave%20Sans%20Mono/0.12/ 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); xulrunner-1.9.x must be installed.		* 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.

			* 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: [http://sourceforge.net/projects/rodin-b-sharp/files/DefaultAuto_ML800 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.

	== Installing ==		== Installing ==

imported>Nicolas: /* Requirements - Compatibility */

2012-02-01T15:21:16Z

Requirements - Compatibility

← Older revision		Revision as of 15:21, 1 February 2012
Line 25:		Line 25:

	* Configuration		* Configuration
	** ~~? Only a '''~~32-bit~~''' version of the Rodin platform is provided for '''PC'''s ?~~		** Linux 32-bit
	** ~~Only a '''~~64-bit~~''' version of the Rodin platform is provided for '''MAC'''~~		** 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.		* 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.