Difference between pages "Rodin Index Design" and "Rodin Platform 2.0 Release Notes"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Mathieu
 
imported>Tommy
 
Line 1: Line 1:
==Purpose==
+
{{TOCright}}
  
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences.  This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.
+
== What's New in Rodin 2.0? ==
 +
* General Interface
 +
:'''Improved Statistic View'''. The statistic view was simplified and unified, to make it clearer and easily resizable and be displayed at first click on every element.
  
==Specification==
+
* Modelling
 +
:'''Mathematical Extensions'''. Rodin was extended to allow definition of basic predicates, new operators or new algebraic types.
 +
::See [[Mathematical extensions]]
  
===The name table===
+
:'''Better platform's behaviour'''. Some cumbersome behaviours where improved:
 +
::- It is now possible to display statistics for a project without expanding it first.
 +
::- The view on selected hypotheses is now correctly scrolled to bottom, to display freshly added ones.
 +
::- Navigating through proof tree nodes is faster (useless refreshings of search hypotheses where removed to gain performance).
  
Firstly, the index manager needs to store declarations. We make the assumption that a declaration corresponds to one and only one element in the database.
+
:'''Independent quantified variables with the same name'''. It is now possible to use the same name for quantified variables which are independant.
  
<blockquote><em>For event-B, this assumption is true. For instance, a variable declaration is an <tt>IVariable</tt> element, an event declaration is an <tt>IEvent</tt>, etc.</em></blockquote>
+
* Proving
 +
:'''Project Explorer's Actions now able to run in background'''. The "Proof Replay on Undischarged POs", "Retry Auto Provers" and "Recalculate Auto Status" commands are now able to run in background. The user is allowed to modify his models, and do interactive proving while such commands are running. Note that the "Save" action on interactively proved PO, which is concerned by such a command, might be delayed as concurrency occurs. The "Save" action will then be scheduled as a further task to be performed, and the user will have to wait or cancel the command. Those commands are accessible by right-clicking in the Event-B Explorer.
 +
:See also: [[Proof Obligation Commands]]
  
However, the element handle doesn't carry directly the user-defined name for the element. This name is stored in an attribute of the element. Thus, one needs to access to the element in the database to retrieve this name. We therefore want to cache this name in the index to prevent frequent accesses to the database that would hinder performance.
+
* Changes for plugin-developers
 +
:'''Rodin 2.0 is Helios based'''. Rodin 2.0 is based on the Eclipse 3.6 Helios release. A wiki page has been added to document main improvements that could be of interest for plug-in developpers.
 +
:See: [[Migration to Eclipse 3.6]]
  
<blockquote>the user-defined name of a variable is stored in its <tt>identifier</tt> attribute, the name of an event in its <tt>label</tt> attribute.</blockquote>
+
:'''Simplified addition of tactic providers for the proving UI'''. A new attribute ("any") can now be used to describe the tactic providers that both apply on hypotheses and goal (i.e. that have the same behavior for both hypothesis predicates and goal predicate).
  
So, the first table that the index manager needs to maintain is specified as
+
:'''A new mechanism to collect informations while traversing formulae'''. The <tt>IFormulaInspector<F></tt> interface has been added and published in order to ease the aggregation of informations (of type F) computed while traversing the AST of a formula. This mechanism replace the old one, where one should retrieve positions where such informations could take place and iterate in a second time on each positions to calculate and accumulate informations.
  
<blockquote><math>\mathit{name}\in\mathit{ELEMENT}\pfun\mathit{STRING}</math>&nbsp;,</blockquote>
+
== Requirements ==
 +
{{TODO | Inform here of some specific system requirements (version of Java, etc).}}
 +
*  It is recommended to run the Rodin platform with a Java 1.6 Runtime Environment.
  
where <math>\mathit{ELEMENT}</math> is the set of all element handles and <math>\mathit{STRING}</math> is the set of all character strings.
+
* Only a 32-bit version of the Rodin platform is provided for PCs.
  
 +
* Only a 64-bit version of the Rodin platform is provided for MAC.
 +
: In other terms, Rodin 2.0 does not support MAC PowerPC / Intel 32-bit based platforms any longer.
  
===The occurrences table===
+
* Migration to Eclipse 3.6 (Helios)
 +
:Some incompatibilities may arise while moving from Eclipse 3.5 to Eclipse 3.6.
 +
:The following page aims to list exhaustively the items to be checked and modified in order to make a plug-in compatible with Rodin 2.0.
 +
:See [[Migration to Eclipse 3.6]].
  
Secondly, the index manager needs to maintain the relation between declarations and occurrences. This relation is specified as
+
== Incompatibilities between Rodin 1.x and Rodin 2.0 ==
  
<blockquote><math>\mathit{occurrences}\in\dom(\mathit{name})\rel\mathit{LOCATION}</math>&nbsp;,</blockquote>
+
=== For Rodin 1.x users ===
 +
:No incompatibility is introduced when migrating to Rodin 2.0. In other terms, models used within Rodin 1.3 are compatible with Rodin 2.0, and vice-versa.
  
where <math>\mathit{LOCATION}</math> is the set of all locations in the database, a location being either an element, or an attribute of an element, or a substring of an attribute of an element. We also have the following function which relates a location to the element that contains the location
+
=== For Rodin 1.x plugin developers ===
 +
:This part lists the incompatibilities encountered when migrating from Rodin 1.x to Rodin 2.0.
  
<blockquote><math>\mathit{element}\in\mathit{LOCATION}\tsur\mathit{ELEMENT}</math>&nbsp;.</blockquote>
+
====Migrating to JVM 1.6====
 +
Plugin developers should be aware of possibly occurring issues when migrating from the JVM 1.5 to the JVM 1.6.<br>
 +
A typical exemple that could produce errors or an unwanted behaviour happen when inlining the result of a HashMap and then compare it to hard-coded values (for example, a string).
  
However, note that this relation is <em>not</em> maintained by the index manager, it is inherent to the definition of locations.
+
''Action required'' : Set the JVM used by the plugin to the 1.6 version, and then check and modify if necessary, the code which produces or could produce errors.
  
==Populating the Index==
+
== External plug-ins ==
 +
{{TODO | Describe here the available plug-ins, and the supported versions for this release.}}
  
Following the general principles of the Rodin core, the Rodin index manager is notation agnostic.  Therefore, it cannot populate the index by itself, but delegates this to plug-ins through an extension point.  These contributions are called <em>indexers</em>.
+
== Downloading ==
 +
{{TODO | Add here a link to download the platform.}}
  
Then, the question arises to define the granularity at which these indexers will be declared and work.  Having an indexer declared and working on a whole project would be too coarse grain.  Conversely, having an indexer declared and working at the granularity of internal elements would be too fine grain.  So, it has been decided that indexers are declared for file elements, based on their type. In hindsight, we are taking here the same design decision we took for the event-B tools when defining the granularity of static checking and proof obligation generation.
+
== Fixed Bugs ==
 +
{{TODO | Add here a list of the fixed bugs.}}
  
Moreover, we want to keep the index at least as open as the Rodin database. So, we need to be prepared to accommodate several indexers working on the same file, as the elements contained in a file can be contributed by several plug-ins.  In this case, the side question is in which order should these indexers be run. The solution chosen is that any indexer can declare that it should be run after another indexer.  In other words, plug-ins can define a partial order among the indexers that will be enforced by the index manager.
+
== Known Issues ==
 +
{{TODO | Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.2).}}
  
Putting everything together, we obtain an extension point for contributing indexers with the following components
+
[[Category:Rodin Platform Release Notes]]
 
 
* id: unique identifier of the indexer
 
* name: human-readable name of the indexer
 
* class: implementation of the indexer
 
* type: list of the file element types handled by the indexer
 
* after: list of the ids of the indexers that must be run before the indexer
 
 
 
 
 
==Index Maintenance==
 
 
 
Of course, the database will change when users edit their models.  We therefore must define a policy for updating the index when the database is modified.  Detecting database changes is easy, thanks to the deltas that are generated by the database manager upon modification.
 
 
 
The difficulty here is that there is no restriction on the occurrences of an element: an element can occur in the file where it is declared, but it can also occur in a completely different file.
 
 
 
<blockquote>For instance, in event-B, a constant can occur in the context where it is declared, but also in any context that extends (directly or indirectly) its declaring context.</blockquote>
 
 
 
So, in principle, each time a file changes, we have to re-index all files.  This is clearly not acceptable from a performance point of view.  In order to keep index updating efficient, we need to better organize the way file changes are propagated in the index.  For this, we first need to gather additional information from indexers (like dependencies between files), then we have to enforce some restrictions on the indexes contributed by indexers, so that we can compute the consequences of a file change.
 
 
 
===Dependencies===
 
 
 
Firstly, we ask the indexers to provide the index manager with the list of files that a given file depends on.  This is stored in the table with the following specification
 
 
 
<blockquote><math>\mathit{dependsOn}\in\mathit{FILE}\rel\mathit{FILE}</math>&nbsp;,</blockquote>
 
 
 
where <math>\mathit{FILE}</math> is the set of all files.
 
 
 
{{TODO| What happens if <math>\mathit{dependsOn}</math> contains a cycle?}}
 
 
 
But having these dependencies is not precise enough, and can still lead to a lot of unnecessary indexing.
 
 
 
<blockquote>For instance, in event-B, if the user adds a theorem to a context on which all files of a project depend (e.g., the context seen by the top-level machine of this project), then we would have to re-index all the files of the project, although it will be useless, as the theorem is not visible to the other files.</blockquote>
 
 
 
Therefore, we also ask that the indexer reports the declarations that are exported (i.e., made visible)  by a file to the files that depend on it.  This information is stored in the table specified as
 
 
 
<blockquote><math>\mathit{exports}\in\mathit{FILE}\rel\mathit{ELEMENT}</math>&nbsp;.</blockquote>
 
<!--blockquote><math>\mathit{exports}\in\mathit{FILE}\rel(\mathit{ELEMENT}\cprod\mathit{STRING})</math>&nbsp;.</blockquote-->
 
 
 
 
 
===Restrictions===
 
 
 
Then, to minimize re-indexing, we ask that indexers behave as good citizens and enforce some restrictions on the elements and locations that an indexer can contribute to the index.
 
 
 
To express these constraints, we need a new constant relation that gives the file in which an element is declared
 
 
 
<blockquote><math>\mathit{file}\in\mathit{ELEMENT}\rel\mathit{FILE}</math>&nbsp;.</blockquote>
 
 
 
This relation is a constant and is inherent to the database structure, it is not maintained by the index manager, only used by it.
 
 
 
Firstly, we ask that an indexer running on file <math>f</math> contributes names only for elements belonging to this file, i.e., these elements must belong to set
 
 
 
<blockquote><math>
 
  \mathit{file}^{-1}[\{f\}]
 
</math>&nbsp;.</blockquote>
 
 
 
Secondly, the indexer must contribute only occurrences in file <math>f</math>, that is the occurrences provided by an indexer must belong to the set
 
 
 
<blockquote><math>
 
  (\mathit{element}\fcomp\mathit{file})^{-1}[\{f\}]
 
</math>&nbsp;.</blockquote>
 
 
 
Thirdly, an indexer only contributes occurrences for elements declared in the file on which it is run or exported by a file on which this file depends directly, i.e., the elements for which an indexer contributes an occurrence must belong to the set
 
 
 
<blockquote><math>
 
  \mathit{file}^{-1}[\{f\}]\bunion
 
  (\mathit{dependsOn}\fcomp\mathit{exports})[\{f\}]
 
</math>&nbsp;.</blockquote>
 
 
 
Finally, an indexer can only export elements for which it can contribute occurrences, as detailed in the previous point.
 
 
 
 
 
===Updating algorithm===
 
 
 
Given these restrictions, we need to update the index for a file only if
 
* either the file has changed,
 
* or the elements visible in the file have changed
 
since the last time it was indexed.
 
 
 
Formally, the last property means that the following set has changed
 
 
 
<blockquote><math>
 
  (\mathit{dependsOn}\fcomp\mathit{exports})[\{f\}]\domres\mathit{name}
 
</math>&nbsp;.</blockquote>
 
 
 
==Concurrency==
 
 
 
{{TODO|Describe concurrency issues: concurrent access and modifications}}
 
 
 
==Persistence==
 
 
 
{{TODO|How is the indexed made persistent across sessions?}}
 
 
 
[[Category:Design]]
 
[[Category:Work in progress]]
 

Revision as of 16:01, 16 July 2010

What's New in Rodin 2.0?

  • General Interface
Improved Statistic View. The statistic view was simplified and unified, to make it clearer and easily resizable and be displayed at first click on every element.
  • Modelling
Mathematical Extensions. Rodin was extended to allow definition of basic predicates, new operators or new algebraic types.
See Mathematical extensions
Better platform's behaviour. Some cumbersome behaviours where improved:
- It is now possible to display statistics for a project without expanding it first.
- The view on selected hypotheses is now correctly scrolled to bottom, to display freshly added ones.
- Navigating through proof tree nodes is faster (useless refreshings of search hypotheses where removed to gain performance).
Independent quantified variables with the same name. It is now possible to use the same name for quantified variables which are independant.
  • Proving
Project Explorer's Actions now able to run in background. The "Proof Replay on Undischarged POs", "Retry Auto Provers" and "Recalculate Auto Status" commands are now able to run in background. The user is allowed to modify his models, and do interactive proving while such commands are running. Note that the "Save" action on interactively proved PO, which is concerned by such a command, might be delayed as concurrency occurs. The "Save" action will then be scheduled as a further task to be performed, and the user will have to wait or cancel the command. Those commands are accessible by right-clicking in the Event-B Explorer.
See also: Proof Obligation Commands
  • Changes for plugin-developers
Rodin 2.0 is Helios based. Rodin 2.0 is based on the Eclipse 3.6 Helios release. A wiki page has been added to document main improvements that could be of interest for plug-in developpers.
See: Migration to Eclipse 3.6
Simplified addition of tactic providers for the proving UI. A new attribute ("any") can now be used to describe the tactic providers that both apply on hypotheses and goal (i.e. that have the same behavior for both hypothesis predicates and goal predicate).
A new mechanism to collect informations while traversing formulae. The IFormulaInspector<F> interface has been added and published in order to ease the aggregation of informations (of type F) computed while traversing the AST of a formula. This mechanism replace the old one, where one should retrieve positions where such informations could take place and iterate in a second time on each positions to calculate and accumulate informations.

Requirements

TODO: Inform here of some specific system requirements (version of Java, etc).

  • It is recommended to run the Rodin platform with a Java 1.6 Runtime Environment.
  • Only a 32-bit version of the Rodin platform is provided for PCs.
  • Only a 64-bit version of the Rodin platform is provided for MAC.
In other terms, Rodin 2.0 does not support MAC PowerPC / Intel 32-bit based platforms any longer.
  • Migration to Eclipse 3.6 (Helios)
Some incompatibilities may arise while moving from Eclipse 3.5 to Eclipse 3.6.
The following page aims to list exhaustively the items to be checked and modified in order to make a plug-in compatible with Rodin 2.0.
See Migration to Eclipse 3.6.

Incompatibilities between Rodin 1.x and Rodin 2.0

For Rodin 1.x users

No incompatibility is introduced when migrating to Rodin 2.0. In other terms, models used within Rodin 1.3 are compatible with Rodin 2.0, and vice-versa.

For Rodin 1.x plugin developers

This part lists the incompatibilities encountered when migrating from Rodin 1.x to Rodin 2.0.

Migrating to JVM 1.6

Plugin developers should be aware of possibly occurring issues when migrating from the JVM 1.5 to the JVM 1.6.
A typical exemple that could produce errors or an unwanted behaviour happen when inlining the result of a HashMap and then compare it to hard-coded values (for example, a string).

Action required : Set the JVM used by the plugin to the 1.6 version, and then check and modify if necessary, the code which produces or could produce errors.

External plug-ins

TODO: Describe here the available plug-ins, and the supported versions for this release.

Downloading

TODO: Add here a link to download the platform.

Fixed Bugs

TODO: Add here a list of the fixed bugs.

Known Issues

TODO: Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.2).