D32 General Platform Maintenance

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[2] 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.

Maintenance tasks to perform are collected from the aforementioned streams and scheduled during WP9 meetings. These tasks are processed in the same way as the task planned in the description of work.

The following table describes the main tasks performed or scheduled tasks motivating the evolutive maintenance :

Origin	Maintenance Task	Done in 2010	Scheduled in 2011
WP1-4 partners	Updating fields of records	x
WP1-4 partners	Allow team work	x
WP1-4 partners	Increase platform performances		x
WP1-4 partners	Search in goal window		x
WP1-4 partners	Preferences for the automatic tactics		x
Plug-in developers	API to extend the Pretty Print View	x
Plug-in developers	View the error log	x
End Users	Adding a replay proof command in the Event-B Explorer	x
End Users	Having auto-completion in proof control	x
End Users	Displaying instantiated hypotheses	x
End Users	Displaying the inherited elements		x
End Users	Exporting / Importing configuration of auto-tactics and post-tactics		x

NB. Note that end users requests mostly overlap WP1-4 partners requests.

Concerning the refactoring plug-in...

Choices / Decisions

Prioritisation of maintenance tasks

As seen in the previous section, the tasks to be performed are listed and ordered by priority. Listed tasks are now being given a priority during WP9 biweekly meetings and then assigned to partners in charge of their processing. It has been decided to give more priority to WP1-4 partner's requests than end-users requests according to the needed time to process them.

64-bit release of Rodin for Mac platforms

A major UI bug, due to some incompatibilities between Eclipse 3.5 and Java 1.6 on Mac platforms motivated the migration to the Eclipse 3.6 as basis for the Rodin 2.0 platform. In the meantime, as the 32-bit Java Virtual Machine is no longer supported on Mac platforms, Rodin migrated to Java 1.6, so that the release 2.0 of Rodin became a 64-bit Mac platform only. The Rodin platforms family is then composed of three executables : 32-bit platforms for Linux and Windows environments and a 64-bit platform for Mac computers.

Releasing Rodin sources

The sources of Rodin releases are now packed with the platform. It has been decided to ship the sources in every platform release. It is, for developers, a convenient alternative to the available sources on SourceForge (See [3]).

Wiki release notes

The release notes contain information about the released plug-ins and centralise the requirements or existing issues which could not be stated at the main platform release date. Thus, since Rodin 2.0 release, it has been chosen to link the contents of the release notes text file included in Rodin releases, with the contents of the dedicated wiki page.

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.

• Bugs.

See [4].

• Feature requests.

See [5].

The user manual, user tutorial and other developer documentation on the wiki are continuously, and collaboratively updated and enhanced. A major update (see [6]) to the developer documentation about Rodin extension ability has been made.

Planning

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