|
|
| Line 1: |
Line 1: |
| − | 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===
| |
| − | * ''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.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]]
| |
