Rodin Platform 2.5 Release Notes - Revision history

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

2012-05-02T17:32:02Z

What's New in Rodin 2.5?

← Older revision		Revision as of 17:32, 2 May 2012
Line 4:		Line 4:

	* General changes		* General changes
	~~This release mainly contains bug~~ fixes and code consolidation.		:* Support for '''Check for updates''': it will be possible to upgrade to further releases of the core Rodin platform directly from the tool.
			:* '''Bug fixes''' and '''code consolidation'''.


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

imported>Nicolas: /* Known Issues */

2012-04-27T15:05:19Z

Known Issues

← Older revision		Revision as of 15:05, 27 April 2012
Line 91:		Line 91:

	== 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 2531738: RODIN crash adding text to note or text box in class diagram
			Bug 2782243: BraveSansMono
			Bug 2817523: No paste in root contextual menu of explorer
			Bug 2824204: Change to Rodin Elements not reflected in editor
			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 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 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 3024811: Leaks in Event-B Explorer
			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 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 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 3419497: Hypothesis cache updated too often
			Bug 3430133: The working area doesn't automatically scroll
			Bug 3440270: java heap space
			Bug 3440688: Camille editor : Save Failed -1
			Bug 3459295: Camille Editor : guards/theorem
			Bug 3469731: Rodin crashes when adding an extends clause in Camille
			Bug 3474224: proof support for prj1 and prj2
			Bug 3483250: Incorrect fix to 3106728
			Bug 3483255: inadmissible datatypes
			Bug 3484421: Camille unable to open a context
			Bug 3484721: Unable to kill NewPP
			Bug 3488583: Duplicate PO for action WD
			Bug 3514920: Missing red line around first yellow box

	[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 */

2012-04-27T15:03:04Z

Fixed Bugs

@@ Line 60: / Line 60: @@
 {{:Rodin_Platform_2.5.0_External_Plug-ins}}
-== Fixed Bugs ==
+== Fixed Bugs and Implemented Feature Requests ==
-{{TODO | Add here a list of the fixed bugs.}}
 == Known Issues ==

imported>Nicolas at 14:34, 27 April 2012

2012-04-27T14:34:56Z

← Older revision		Revision as of 14:34, 27 April 2012
Line 1:		Line 1:
	~~RODIN 2.5 is planned for April 30th.~~

	~~N.B. Release notes are commented in this page.~~
	{{TOCright}}		{{TOCright}}

Line 40:		Line 37:
	: We have not noticed this problem for Linux 64-bit, nor for other platforms; however if you do, the same workaround applies.		: 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}}<br>~~
	~~{{TODO \| Inform here of some specific system requirements (version of Java, etc).}}~~

	~~== External plug-ins ==~~
	~~{{:Rodin_Platform_2.5.0_External_Plug-ins}}~~

	== Installing ==		== Installing ==
	~~{{TODO \| Add here a link to download the platform.}}~~

	=== Downloading ===		=== Downloading ===
Line 65:		Line 56:
	: accept license agreements then click "Finish": the software is updating, which can take a few minutes		: 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"		: click "OK" if the security warning appears, then accept to "Restart Now"

			== External plug-ins ==
			{{:Rodin_Platform_2.5.0_External_Plug-ins}}

	== Fixed Bugs ==		== Fixed Bugs ==
Line 70:		Line 64:

	== Known Issues ==		== Known Issues ==
	~~{{TODO \| COPY KNOWN ISSUES FROM PREVIOUS PAGES~~ / ~~VERIFY}}<br>~~
	~~{{TODO \| Add here a link to the~~ SourceForge ~~Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.2).}}~~		[https://sourceforge.net/tracker/?group_id=108850&atid=651669&status=1 Bugs on SourceForge]

	== Disclaimer ==		== Disclaimer ==
Line 77:		Line 71:

	== About ==		== About ==
	Rodin Platform up to ~~rxxxx~~.<br>		Rodin Platform up to r14636.<br>
	Developer Release date : dd/mm/~~yyyy~~.<br>		Developer Release date : 27/04/2012.<br>
	User Release date : dd/mm/~~yyyy~~.		User Release date : 02/05/2012.

	[[Category:Rodin Platform Release Notes]]		[[Category:Rodin Platform Release Notes]]

imported>Nicolas: /* External plug-ins */

2012-04-17T17:31:28Z

External plug-ins

← Older revision		Revision as of 17:31, 17 April 2012
Line 44:		Line 44:

	== External plug-ins ==		== External plug-ins ==
	~~{{TODO \| Link to the external page for plug-ins}}<br>~~		{{:Rodin_Platform_2.5.0_External_Plug-ins}}
	~~Link of the form:~~
	~~<nowiki>~~{{:Rodin_Platform_2.5.0_External_Plug-ins}}~~</nowiki>~~

	== Installing ==		== Installing ==

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

2012-04-17T17:20:53Z

What's New in Rodin 2.5?

← Older revision		Revision as of 17:20, 17 April 2012
Line 5:		Line 5:

	== What's New in Rodin 2.5? ==		== What's New in Rodin 2.5? ==
	~~{{TODO \| PLANS ARE : consolidation and auto-tactics (programmatic) extensibility...}}~~

	* General changes		* General changes

imported>Nicolas: /* Requirements - Compatibility */

2012-04-17T17:08:54Z

Requirements - Compatibility

← Older revision		Revision as of 17:08, 17 April 2012
Line 35:		Line 35:

	* Linux 64-bit:		* Linux 64-bit:
	: package libc6:i386 (and its dependencies) must be installed.		: 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:		* Windows 64-bit:

imported>Nicolas: /* Requirements - Compatibility */

2012-04-17T17:03:59Z

Requirements - Compatibility

← Older revision		Revision as of 17:03, 17 April 2012
Line 35:		Line 35:

	* Linux 64-bit:		* Linux 64-bit:
	: package ~~ia32-libs~~ (and its dependencies) must be installed.		: package libc6:i386 (and its dependencies) must be installed.

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

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

2012-04-17T13:17:17Z

Upgrading from Rodin 2.4.x

← Older revision		Revision as of 13:17, 17 April 2012
Line 57:		Line 57:
	=== Upgrading from Rodin 2.4.x ===		=== Upgrading from Rodin 2.4.x ===

	Use ~~rodin-2.5-repo.zip~~:		Use the core update site:

	* ~~download archive [http~~:~~//sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.5/rodin-2.5-repo.zip/download rodin-2.5-repo.zip]~~		* Window > Preferences > Install/Update > Available Software Sites:
	* launch Rodin ~~2.4.x~~		: remove Scala update site (no more exists): click "Scala" then "Remove" button, click "Yes" on the popup to confirm
	* Help > Install New Software... > Add... > enter a name (~~for instance~~ "Rodin ~~2.5~~") then		: 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"
	: ~~Archive... > select the~~ rodin-~~2.5~~-~~repo~~.~~zip archive~~		: click "OK"
	~~: Mac users may have to use Local~~.~~.. then point to archive root directory, in case the archive was automatically unzipped~~		* Help > Check for Updates:
	* set options in the bottom of the page:		: "Checking for updates" appears with a progress bar, it can take a few minutes
	~~:* check~~		: Available updates lists the Handbook and the Rodin Platform, click "Next" twice
	~~:** "Show only the latest versions of available software~~"		: accept license agreements then click "Finish": the software is updating, which can take a few minutes
	:** "~~Hide items that are already installed~~"		: click "OK" if the security warning appears, then accept to "Restart Now"
	:* ~~uncheck~~
	:** "Group items by category"
	:** "~~Contact all update sites...~~"
	: the ~~central area should now list many entries~~
	* select "Rodin Platform", click "Next"
	: ~~a message informs~~ "~~Your original request has been modified. See the details.~~"
	: ~~"Rodin Platform"~~ is ~~already installed~~, ~~so an update will be performed instead.~~
	* click ~~Next~~, accept ~~license, finish and restart~~

	== Fixed Bugs ==		== Fixed Bugs ==

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

2012-04-17T09:22:09Z

What's New in Rodin 2.5?

← Older revision		Revision as of 09:22, 17 April 2012
Line 7:		Line 7:
	{{TODO \| PLANS ARE : consolidation and auto-tactics (programmatic) extensibility...}}		{{TODO \| PLANS ARE : consolidation and auto-tactics (programmatic) extensibility...}}

	* General ~~Interface~~		* General changes
	~~{{TODO \|~~ .~~..}}~~		This release mainly contains bug fixes and code consolidation.

	* ~~Modelling~~		* Changes for plugin-developers
	~~{{TODO \| ...}}~~

	* ~~Proving~~		:* '''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''.
	~~{{TODO \|~~ ...}}

	* Changes for plugin-developers
	:* '''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.		:* '''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.		::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.

	:* '''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''.

	:* '''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.		:* '''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.