Difference between revisions of "D32 General Platform Maintenance"

From Event-B
Jump to navigationJump to search
imported>Tommy
imported>Tommy
m
Line 10: Line 10:
 
:
 
:
 
* Documentation
 
* Documentation
:  
+
: Plug-in developers expressed their need to get a detailed documentation about Rodin extension ability. A dedicated [http://wiki.event-b.org/index.php/Plug-in_Tutorial tutorial] has been written accordingly, and was the support of a training session given at the [http://www.event-b.org/rodin10.html Rodin User and Developer Workshop] in Düsseldorf this year.
  
 
See the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Release Notes] and the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation SourceForge] databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
 
See the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Release Notes] and the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation SourceForge] databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
  
 
= Motivations =
 
= Motivations =
The main evolutions of the Rodin platform are driven by the description of work for the DEPLOY project and the requirements expressed by industrial WP1 to WP4 partners or by advanced users during the lifecycle of the project.
+
The evolutive maintenance (resp. corrective maintenance) has its origin in the Deploy project's description of work, and the various requests (resp. bug reports) listed by WP1-4 partners, developers and users. Since the Deploy project's birth, various streams can be used to express feature requests or track an encountered bug :
 +
: - [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation dedicated trackers],
 +
: - mail to the deploy user list, etc.
 +
During the WP9 meetings, maintenance tasks to perform are being given a priority and are assigned to an according WP9 partner (as mentionned in the D23). The higher priority is given to WP partners requests.
 +
The following table describes the task that motivated the maintenance being done during the last Deploy project's year :
 +
 
 +
{{SimpleHeader}}
 +
|-
 +
! scope=col | Type || Maintenance Task || Done || Scheduled
 +
|-
 +
|Documentation || Rodin Extension documentation (Plug-in developers) || x ||
 +
|-
 +
| || Meaning of Retry auto-provers / Recalculate auto-status (end users) || x ||
 +
|-
 +
|Corrective Maintenance || || ||
 +
|-
 +
|Evolutive Maintenance || || ||
 +
|- || || ||
 +
|- || || ||
 +
|}
  
The priorities are discussed during the WP9 meetings (bi-weekly management conference call, WP9 face-to-face meetings during DEPLOY workshops).
 
  
 
= Choices / Decisions =
 
= Choices / Decisions =
The WP9 partners have agreed on a release policy (see the [http://wiki.event-b.org/index.php/D23_General_Platform_Maintenance#Available_Documentation Rodin Platform Releases] wiki page). In particular:
 
* A new version of the Rodin platform is released every 3 months.
 
* The code is frozen during the 2 weeks preceding each release.
 
* The Eclipse versioning policy is enforced (See [http://wiki.eclipse.org/index.php/Version_Numbering Version Numbering]).
 
* A wiki page is dedicated to each release.
 
  
The main advantages, for both developers and end-users, are summarized below:
+
---MAC plat 3.6
* Information. The wiki page dedicated to each release provides instant information on the new features and improvements, which may be discussed if necessary.
 
* Validation. The period of code freeze is more especially devoted to bug fixes, and the frequency of the stable releases is ensured.
 
* Integration. A synchronization between the optional plug-ins and other plug-ins is now possible.
 
  
 
= Available Documentation =
 
= Available Documentation =
The following pages give useful information about the Rodin platform releases:
+
As in the previous D23 delivrable, the following pages give useful information about the Rodin platform releases:
 
* Release notes.
 
* Release notes.
 
: See [http://wiki.event-b.org/index.php/Rodin_Platform_Releases Rodin Platform Releases].  
 
: See [http://wiki.event-b.org/index.php/Rodin_Platform_Releases Rodin Platform Releases].  

Revision as of 17:35, 4 November 2010

Overview

The main goal of the platform corrective and evolutive maintenance is to fix the listed known bugs, and implement some new requested features. As in the previous years of Deploy, these bugs and features are reported either by mail or through dedicated SourceForge trackers.

The terse list below gives an overwiew of the noteworthy features added in the main platform during the past year:

  • Proof replay of undischarged POs (releases 1.3 and upper)
It often happens, while modifying a model, that a set of previously manually discharged POs are slightly changed and need to be discharged again. However, replaying the proof for those POs could most of the time be enough to discharge it. Hence, a command was added to manually try replaying the proofs for a set of undischarged POs. This request was expressed by end users. See [1].
  • Rule Details View (releases 2.0 and upper)
When doing an interactive proof, one is guided by the proof tree appearing on the proof tree view. However, it is sometimes needed to get more informations about the rules being involved in a proof, such as instantiation details, hidden hypotheses, etc. The Rule Details View displaying such details has been added.
  • Refactoring plug-in (releases 1.2 and upper)
  • Documentation
Plug-in developers expressed their need to get a detailed documentation about Rodin extension ability. A dedicated tutorial has been written accordingly, and was the support of a training session given at the Rodin User and Developer Workshop in Düsseldorf this year.

See the Release Notes and the SourceForge databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.

Motivations

The evolutive maintenance (resp. corrective maintenance) has its origin in the Deploy project's description of work, and the various requests (resp. bug reports) listed by WP1-4 partners, developers and users. Since the Deploy project's birth, various streams can be used to express feature requests or track an encountered bug :

- dedicated trackers,
- mail to the deploy user list, etc.

During the WP9 meetings, maintenance tasks to perform are being given a priority and are assigned to an according WP9 partner (as mentionned in the D23). The higher priority is given to WP partners requests. The following table describes the task that motivated the maintenance being done during the last Deploy project's year :


Type Maintenance Task Done Scheduled
Documentation Rodin Extension documentation (Plug-in developers) x
Meaning of Retry auto-provers / Recalculate auto-status (end users) x
Corrective Maintenance
Evolutive Maintenance


Choices / Decisions

---MAC plat 3.6

Available Documentation

As in the previous D23 delivrable, the following pages give useful information about the Rodin platform releases:

  • Release notes.
See Rodin Platform Releases.
More details are provided in the notes distributed with each release (eg. [2]).
  • Bugs.
See [3].
  • Feature requests.
See [4].

Planning

The Rodin Platform Releases wiki page lists in particular the upcoming releases and give the scheduled release dates.