Difference between pages "Template:Dev News" and "Theory Release History"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Mathieu
m (1.0.0 release + some archive)
 
(Theory plug-in release 4.0.3)
 
Line 1: Line 1:
<noinclude>
+
Back to [[Theory Plug-in]].
[http://wiki.event-b.org/index.php?title=Template:Dev_News/Archives&action=edit Edit Archives]
 
== Displayed as follow on the Main Page ==
 
<div style="margin:0;width:50%;border:1px solid #AAAAAA;background:#FFFFFF;">
 
</noinclude><!--- News to add here below : ==== --->
 
<div style="font-size:90%;">
 
* 31/07/09 : UML-B plugin released for Rodin 1.0.0
 
* 27/07/09 : Fixed requirement plug-in for rodin 1.0.0
 
* 01/07/09 : [https://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/1.0/ Release 1.0.0] of Rodin is now available ([http://sourceforge.net/project/shownotes.php?release_id=693928 changelog])
 
* 15/06/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/17ebfa Fix] bug 2806135: ''DB exception when creating new ISeesContext''
 
* 14/06/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/17e3b2 Fix] bug 2805521: ''Erroneous paste in ProofControl made the input area a StyledText''
 
* 12/06/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/17c0e7 Fix] bug 2804046: ''AssertionError in Indexer''
 
* 05/06/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/1762f1 Fix] in added feature #2564322: ''the state of the buttons did not correctly refresh.''
 
* 05/06/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/171bff Fix] bug #2800402: ''Exception when opening a proof obligationRemoved unneeded select actions''
 
* 03/06/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/17094f Fix] bug #2800545: ''Reordering is global but should be local''
 
* 02/06/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/16e8c3 Fix] bug #2798407: ''Events can have an empty label''
 
* 29/05/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/1603ae Fix] bug #2684839: ''Statistics view doesn't refresh''
 
* 28/05/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/15f594 Fix] bug #2798042: ''Deadlock of the indexer when closing a project''
 
* xx/05/09 : Several bug corrections not reported here. See [http://cia.vc/stats/project/rodin-b-sharp/ cia.vc]
 
* 04/05/09 : [http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714&release_id=687381 Release Candidate] ''Rodin 1.0RC1 now available''
 
* 09/04/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/e10e0 Fix] ''Inconsistency in label generation in the INITIALISATION event.'' bug
 
* 09/04/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/dffc7 Fix] ''Broken universal instantiation in proving UI'' bug
 
* 09/04/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/e10e0 Fix] ''Scrollbar in instantiation boxes'' bug
 
* 04/04/09: [http://cia.vc/stats/project/rodin-b-sharp/.message/d4da9 Major update] [[Mathematical Language Evolution Design|implementing]] the [[Changes to the Mathematical Language of Event-B|mathematical language V2]], while retaining full backward compatibility. New plug-in version is 1.0.0.
 
* 02/04/09: [http://cia.vc/stats/project/rodin-b-sharp/.message/d4557 Fix] ''Event-B editor dead slow'' [http://sourceforge.net/tracker/?func=detail&aid=2691183&group_id=108850&atid=651669 Bug]
 
* 02/04/09: [http://cia.vc/stats/project/rodin-b-sharp/.message/d2122 Fix] ''Already executed event can not be executed'' bug in [[AnimB]].
 
* 02/04/09: [http://cia.vc/stats/project/rodin-b-sharp/.message/d2d99 Fix] ''Silent formula normalization in event-B editor'' [http://sourceforge.net/tracker/?func=detail&aid=2689863&group_id=108850&atid=651669 Bug]
 
* 01/04/09: [http://cia.vc/stats/project/rodin-b-sharp/.message/d1cda Fix] ''Having space in Rodin path will fail AtelierB Provers'' [http://sourceforge.net/tracker/?func=detail&aid=2682104&group_id=108850&atid=651669 Bug]
 
* 31/03/09: [http://cia.vc/stats/project/rodin-b-sharp/.message/cfb16 Fix] ''Indexer forget some elements'' [http://sourceforge.net/tracker/index.php?func=detail&aid=2721800&group_id=108850&atid=651669 bug]
 
  
</div>
+
Follow this page for the latest on the Theory plug-in. The user manual is also provided together with the installation details.
<noinclude>
+
 
</div>
+
===News===
[[Category:Main page templates]]
+
* ''29th September 2021'': [[#Version_4.0.3|Version 4.0.3]] is released. It requires Rodin 3.5.
</noinclude>
+
* ''4th June 2021'': [[#Version_4.0.2|Version 4.0.2]] is released. It requires Rodin 3.5.
 +
* ''22th December 2020'': [[#Version_4.0.1|Version 4.0.1]] is released. It requires Rodin 3.5.
 +
* ''19th December 2014'': [[#Version_3.0.0|Version 3.0.o]] is released. It requires Rodin 3.1.
 +
* ''10th July 2014'': [[#Version_2.0.2|Version 2.0.2]] is released. It requires Rodin 2.8.
 +
* ''24th June 2014'': [[#Version_2.0.1|Version 2.0.1]] is released. It requires Rodin 2.8.
 +
* ''30th April 2014'': [[#Version_2.0.0|Version 2.0.0]] is released. It requires Rodin 2.8. This release contains major changes in the features and accessibilities.
 +
* ''20th April 2012'': [[#Version_1.3.2|Version 1.3.2]] is released. It requires Rodin 2.4.
 +
* ''15th August 2011'': [[#Version_1.2|Version 1.2]] is released. It requires Rodin 2.2.2.
 +
* ''6th August 2011'': [[#Version_1.1|Version 1.1]] is released. It requires Rodin 2.2.2.
 +
* ''8th July 2011'': [[#Version_1.0|Version 1.0]] is released. It requires Rodin 2.2.
 +
* ''22nd May 2011'': [[#Version_0.8|Version 0.8]] released. It is based on Rodin 2.1.1.
 +
* ''11th April 2011'': [[#Version_0.7|Version 0.7]] released. It is based on Rodin 2.1.1.
 +
* ''6th January 2011'': [[#Version_0.6|Version 0.6]] released. It is based on Rodin 2.0.1.
 +
* ''28th October 2010'': [[#Version_0.5|Version 0.5]] released. It is based on Rodin 2.0.
 +
 
 +
===Releases===
 +
===== Version 4.0.3 =====
 +
''29th September 2021''
 +
 
 +
Release target: Rodin 3.5
 +
* Bug fixes:
 +
** Operators that have parameters with the same name but different types are now handled correctly in both the editor and the prover (for rewriting the definition)
 +
** Theorems instantiated during proof are now correctly typed (in some cases, some type information was missing)
 +
 
 +
===== Version 4.0.2 =====
 +
''4th June 2021''
 +
 
 +
Release target: Rodin 3.5
 +
* Bug fixes:
 +
** Datatypes that have several type parameters are now serialized in the right order; it fixes some issues with proofs and proof replay.
 +
** Manually applied inference and rewrite rules are now replayed correctly (in some cases, their replay was displayed as uncertain).
 +
 
 +
===== Version 4.0.1 =====
 +
''22th December 2020''
 +
 
 +
Release target: Rodin 3.5
 +
* Bug fixes:
 +
** The theory plugin now takes into account updates in theories, as well as creating a theory after using it (there was a cache issue).
 +
** The error messages at launch about rule-based provers failing to find the context of the proof have been removed.
 +
** The dropdown list in theory imports is now usable (there was an off-by-one issue when selecting an element in the list).
 +
** Manually applying an inference rule no longer throws a NullPointerException.
 +
** It is now possible to rename theories.
 +
** The TheoryPath creation dialog box has been simplified.
 +
* Optimizations:
 +
** The proving interface is now much more responsive, even when a theory contains a lot of rewrite rules (we have implemented a cache of the places where a rewrite rule can apply).
 +
** The theory plugin now generates much simpler WD conditions, especially for the pred, succ, prj1, prj2, and id operators.
 +
 
 +
===== Version 4.0.0-RC1 =====
 +
''10th April 2017''
 +
 
 +
Release target: Rodin 3.2
 +
* AST Extensions (4.0.0) Major API change.
 +
** Compatibility upgrade to Rodin 3.2
 +
** Support for get operator position for INFIX extended predicate operators.
 +
** Improve pattern matching for associative operators.
 +
* Theory plug-in Branding (0.0.1) Initial version
 +
* Theory Core (4.0.0) Internal implementation changes.
 +
** Compatibility upgrade to Rodin 3.2
 +
** Support for INFIX extended predicate operators.
 +
** Various bugs fixed.
 +
* Theory help (2.0.0) User documentations.
 +
* Theory Keyboard (0.0.1) Initial version (A special plug-in for typesetting Theory).
 +
** Support for typesetting Real arithmetics (plus, unary minus, multiply, divide, less than, less than or equal, greater than, greater than or equal).
 +
* Theory Rule-based Prover (4.0.0)
 +
** Reasoners' input does not contain the proof-obligation context.
 +
** Use the current sequent's origin to get the proof-obligation context.
 +
** Bug fixed: translate formula to ensure they have the same formula factory.
 +
** Added version numbers for reasoners.
 +
** Automatic rewrite and inference tactics are re-implemented so that each rule application is visible in proof trees.
 +
* Theory UI (3.0.0)
 +
 
 +
===== Version 3.0.0 =====
 +
''17th December 2014''
 +
 
 +
Release target : Rodin 3.1
 +
* migration changes to Rodin 3.1
 +
 
 +
===== Version 2.0.2 =====
 +
''10th July 2014''
 +
 
 +
Release target : Rodin 2.8
 +
* bug fixes.
 +
 
 +
===== Version 2.0.1 =====
 +
''24th June 2014''
 +
 
 +
Release target : Rodin 2.8
 +
* bug fixes.
 +
 
 +
===== Version 2.0.0 =====
 +
''30th April 2014''
 +
 
 +
Release target : Rodin 2.8
 +
* Major changes in the usability.
 +
* Important bug fixes.
 +
 
 +
===== Version 1.3.2 =====
 +
''20th April 2012''
 +
 
 +
Release target : Rodin 2.4
 +
* Important bug fixes.
 +
* Improvement of deployment and un-deployment wizards
 +
 
 +
===== Version 1.2 =====
 +
''15th August 2011''
 +
 
 +
Release target : Rodin 2.2.2
 +
* Bug fixes.
 +
* Added capability to instantiate multiple theorems at once.
 +
* Added automatic tactic for expanding operator definitions RbPxd·
 +
 
 +
===== Version 1.1 =====
 +
''6th August 2011''
 +
 
 +
Release target : Rodin 2.2.2
 +
* Theory library first version.
 +
* Bug fixes.
 +
* Improved UI.
 +
 
 +
===== Version 1.0 =====
 +
''8th July 2011''
 +
 
 +
Release target : Rodin 2.2
 +
 
 +
* Bug fixes.
 +
* Added import relationships between theories.
 +
* Added experimental support for recursive definitions.
 +
* Improved project as well as workspace scope for mathematical and prover extensions.
 +
* Added tactic (xd) to expand all definitions.
 +
* Fixed support for polymorphic theorems.
 +
 
 +
===== Version 0.8 =====
 +
''22nd May 2011''
 +
 
 +
Release target : Rodin 2.1.1
 +
 
 +
* Bug fixes.
 +
* Added import relationships between theories.
 +
* Added experimental support for recursive definitions.
 +
* Added project as well as workspace scope for mathematical and prover extensions.
 +
 
 +
===== Version 0.7 =====
 +
''11th April 2011''
 +
 
 +
Bug fixes. Fixed for Rodin 2.1.1.
 +
 
 +
===== Version 0.6 =====
 +
''6th January 2011''
 +
 
 +
Minor bug fixes and improvements to theories pretty printer.
 +
 
 +
===== Version 0.5 =====
 +
''28th October 2010''
 +
 
 +
This is the first release of the Theory plug-in with support for mathematical as well as prover extensions.
 +
 
 +
===Features Requests and Bugs===
 +
Please do not hesitate to raise any issues with regards to usability as well as efficiency. Finally, please remember to report any bugs through the SourceForge portal.
 +
 
 +
[[Category:Theory Plug-in]]

Revision as of 13:11, 29 September 2021

Back to Theory Plug-in.

Follow this page for the latest on the Theory plug-in. The user manual is also provided together with the installation details.

News

  • 29th September 2021: Version 4.0.3 is released. It requires Rodin 3.5.
  • 4th June 2021: Version 4.0.2 is released. It requires Rodin 3.5.
  • 22th December 2020: Version 4.0.1 is released. It requires Rodin 3.5.
  • 19th December 2014: Version 3.0.o is released. It requires Rodin 3.1.
  • 10th July 2014: Version 2.0.2 is released. It requires Rodin 2.8.
  • 24th June 2014: Version 2.0.1 is released. It requires Rodin 2.8.
  • 30th April 2014: Version 2.0.0 is released. It requires Rodin 2.8. This release contains major changes in the features and accessibilities.
  • 20th April 2012: Version 1.3.2 is released. It requires Rodin 2.4.
  • 15th August 2011: Version 1.2 is released. It requires Rodin 2.2.2.
  • 6th August 2011: Version 1.1 is released. It requires Rodin 2.2.2.
  • 8th July 2011: Version 1.0 is released. It requires Rodin 2.2.
  • 22nd May 2011: Version 0.8 released. It is based on Rodin 2.1.1.
  • 11th April 2011: Version 0.7 released. It is based on Rodin 2.1.1.
  • 6th January 2011: Version 0.6 released. It is based on Rodin 2.0.1.
  • 28th October 2010: Version 0.5 released. It is based on Rodin 2.0.

Releases

Version 4.0.3

29th September 2021

Release target: Rodin 3.5

  • Bug fixes:
    • Operators that have parameters with the same name but different types are now handled correctly in both the editor and the prover (for rewriting the definition)
    • Theorems instantiated during proof are now correctly typed (in some cases, some type information was missing)
Version 4.0.2

4th June 2021

Release target: Rodin 3.5

  • Bug fixes:
    • Datatypes that have several type parameters are now serialized in the right order; it fixes some issues with proofs and proof replay.
    • Manually applied inference and rewrite rules are now replayed correctly (in some cases, their replay was displayed as uncertain).
Version 4.0.1

22th December 2020

Release target: Rodin 3.5

  • Bug fixes:
    • The theory plugin now takes into account updates in theories, as well as creating a theory after using it (there was a cache issue).
    • The error messages at launch about rule-based provers failing to find the context of the proof have been removed.
    • The dropdown list in theory imports is now usable (there was an off-by-one issue when selecting an element in the list).
    • Manually applying an inference rule no longer throws a NullPointerException.
    • It is now possible to rename theories.
    • The TheoryPath creation dialog box has been simplified.
  • Optimizations:
    • The proving interface is now much more responsive, even when a theory contains a lot of rewrite rules (we have implemented a cache of the places where a rewrite rule can apply).
    • The theory plugin now generates much simpler WD conditions, especially for the pred, succ, prj1, prj2, and id operators.
Version 4.0.0-RC1

10th April 2017

Release target: Rodin 3.2

  • AST Extensions (4.0.0) Major API change.
    • Compatibility upgrade to Rodin 3.2
    • Support for get operator position for INFIX extended predicate operators.
    • Improve pattern matching for associative operators.
  • Theory plug-in Branding (0.0.1) Initial version
  • Theory Core (4.0.0) Internal implementation changes.
    • Compatibility upgrade to Rodin 3.2
    • Support for INFIX extended predicate operators.
    • Various bugs fixed.
  • Theory help (2.0.0) User documentations.
  • Theory Keyboard (0.0.1) Initial version (A special plug-in for typesetting Theory).
    • Support for typesetting Real arithmetics (plus, unary minus, multiply, divide, less than, less than or equal, greater than, greater than or equal).
  • Theory Rule-based Prover (4.0.0)
    • Reasoners' input does not contain the proof-obligation context.
    • Use the current sequent's origin to get the proof-obligation context.
    • Bug fixed: translate formula to ensure they have the same formula factory.
    • Added version numbers for reasoners.
    • Automatic rewrite and inference tactics are re-implemented so that each rule application is visible in proof trees.
  • Theory UI (3.0.0)
Version 3.0.0

17th December 2014

Release target : Rodin 3.1

  • migration changes to Rodin 3.1
Version 2.0.2

10th July 2014

Release target : Rodin 2.8

  • bug fixes.
Version 2.0.1

24th June 2014

Release target : Rodin 2.8

  • bug fixes.
Version 2.0.0

30th April 2014

Release target : Rodin 2.8

  • Major changes in the usability.
  • Important bug fixes.
Version 1.3.2

20th April 2012

Release target : Rodin 2.4

  • Important bug fixes.
  • Improvement of deployment and un-deployment wizards
Version 1.2

15th August 2011

Release target : Rodin 2.2.2

  • Bug fixes.
  • Added capability to instantiate multiple theorems at once.
  • Added automatic tactic for expanding operator definitions RbPxd·
Version 1.1

6th August 2011

Release target : Rodin 2.2.2

  • Theory library first version.
  • Bug fixes.
  • Improved UI.
Version 1.0

8th July 2011

Release target : Rodin 2.2

  • Bug fixes.
  • Added import relationships between theories.
  • Added experimental support for recursive definitions.
  • Improved project as well as workspace scope for mathematical and prover extensions.
  • Added tactic (xd) to expand all definitions.
  • Fixed support for polymorphic theorems.
Version 0.8

22nd May 2011

Release target : Rodin 2.1.1

  • Bug fixes.
  • Added import relationships between theories.
  • Added experimental support for recursive definitions.
  • Added project as well as workspace scope for mathematical and prover extensions.
Version 0.7

11th April 2011

Bug fixes. Fixed for Rodin 2.1.1.

Version 0.6

6th January 2011

Minor bug fixes and improvements to theories pretty printer.

Version 0.5

28th October 2010

This is the first release of the Theory plug-in with support for mathematical as well as prover extensions.

Features Requests and Bugs

Please do not hesitate to raise any issues with regards to usability as well as efficiency. Finally, please remember to report any bugs through the SourceForge portal.