Rodin Developer Support: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Jrloria
imported>Tommy
mNo edit summary
 
(28 intermediate revisions by 8 users not shown)
Line 1: Line 1:
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
The Developer Support provides resources for developing plug-ins for the Rodin Platform.


== Setting up Eclipse Workspace ==


== Rodin Platform Overview ==
=== 1. Building against a version of Rodin ===
see [[How To Contribute]]
The recommended practice is to work with a target platform, as described in
[[Using Rodin as Target Platform]].
 
Alternatively, one can develop extensions to the Rodin platform against the
leading edge version of the core plug-ins.  This is mandatory when one targets
a future release of the Rodin platform. We make our best to ensure that the
HEAD revision is always working, but some glitches can appear
from time to time. In this case, you will need to check out the Rodin platform
source code from Git into your workspace.  See
[[Developer_FAQ#Installing_the_sources_from_Git_in_Eclipse|
Installing the sources from Git in Eclipse]] for further instructions.
 
=== 2. Launching Rodin from Eclipse ===
To launch Rodin from within Eclipse, a '''Run Configuration''' is required. This instructions are for those who set up to use Rodin as a Target Platform.
 
1. Menu "Run/Run Configurations", to open the "Run Configurations" dialog.
 
2. Double-click on Eclipse Application on the left-hand side, a "New Configuration" is created
 
3. In the "Main" tab on the right-hand side, change the name of the configuration, e.g., "Rodin 3.0.1"
 
4. In the "Main" tab on the right-hand side, choose the "Location" for the run-time workspace
 
5. In the "Main" tab on the right-hand side, for "Run a product" option, choose "org.rodin.platform.product"
 
6. In the "Plug-ins" tab on the right-hand side, for "Launch with" option, choose "plug-ins selected below only".
 
7. In the list of plug-in, unselect all the test plug-ins for Target platform (Use the "tests" for filter the plug-ins and deselect them.
 
8. Click "Apply"/"Run" to launch Rodin.
 
=== 3. Build your plug-in ===
To start to build your plugin, it is recommended to look at the [[Plug-in Tutorial | Tutorial]]. Remember to add your plug-in to the "Run Configuration" when Testing/Debugging your plug-in.
== Rodin Developer FAQ ==
 
see [[Developer FAQ]].


== Architecture of the Rodin Platform ==
== Architecture of the Rodin Platform ==
[[File:Rodin_feature_dependencies_refactor.svg|800px|thumb|right]]


=== Rodin Platform Core ===
=== Rodin Platform Core ===
Line 23: Line 61:
=== Event-B User Interface ===
=== Event-B User Interface ===


The Event-B User Interface of the Roding Platform has two major components that are concerned with either [[Modelling User Interface|modelling]] in Event-B or [[Proving User Interface|proving]] properties of models.
The Event-B User Interface of the Roding Platform has two major components that are concerned with either [http://handbook.event-b.org/current/html/event_b_perspective.html modelling] in Event-B or [http://handbook.event-b.org/current/html/proving_perspective.html proving] properties of models.


* [[Modelling User Interface]]
* [http://handbook.event-b.org/current/html/event_b_perspective.html Modelling User Interface]


* [[Proving User Interface]]
* [http://handbook.event-b.org/current/html/proving_perspective.html Proving User Interface]


Apart from these are more minor components.
Apart from these are more minor components.
Line 39: Line 77:
=== Event-B Component Library ===
=== Event-B Component Library ===


Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a [[Static Checker|static checker]]. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The [[Proof Obligation Generator|proof obligation generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[Proof Manager|proof manager]] attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the [[Proving User Interface|proving user interface]]).
Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a [[Static Checker|static checker]]. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The [[Proof Obligation Generator|proof obligation generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[Proof Manager|proof manager]] attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the [http://handbook.event-b.org/current/html/proving_perspective.html proving user interface]).


* [[Abstract Syntax Tree]]
* [[Abstract Syntax Tree]]
Line 53: Line 91:
== Extending Rodin ==
== Extending Rodin ==


* [[Getting Started]]
* [[Developer Documentation]]


* [[Plug-in Tutorial]]
* [[Plug-in Tutorial]]
Line 62: Line 100:


* [[Extending the Structure Editor]]
* [[Extending the Structure Editor]]
* [[Extending the Pretty Print Page]]


* [[Extending the Proof Manager]]
* [[Extending the Proof Manager]]


* [[Extending the Index Manager]]
* [[Extending the Index Manager]]
* [[Extending the Static Checker]]


* [[Index Query]]
* [[Index Query]]
== Migration to Rodin 3.0 ==
The new release 3.0 of the Rodin platform introduces incompatible changes in
the core platform API.  The [[Rodin 3.0 Plug-in Migration Guide]] describes
how to adapt plug-ins that work with Rodin 2.7 to the new 3.0 API.


== Useful Hints ==
== Useful Hints ==
Line 73: Line 121:
=== Version Control ===
=== Version Control ===


All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge.  The repository currently used is Subversion and can be accessed using URL [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp].
All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge.  The repository currently used is Git and can be accessed using URI
<nowiki>git://git.code.sf.net/p/rodin-b-sharp/rodincore</nowiki>


=== Building against a version of Rodin ===
=== Building against a version of Rodin ===


To develop extensions to the Rodin platform your code build needs access to a consistent (version-wise) set of Rodin platform plug-ins. (Don't just check out the latest versions from 'Head' because it may be under development and in an inconsistent state). An easy way to set up your workspace is to import the Rodin platform source code from SVN into your workspace using the 'Releng' plug-in. See [http://wiki.event-b.org/index.php/FAQ#Installing_the_sources_from_Subversion_in_Eclipse Installing the sources from Subversion in Eclipse] for further instructions.
The recommended practice is to work with a target platform, as described in
[[Using Rodin as Target Platform]].


Alternatively, you can set your plugin development target platform to any Rodin installation you have installed (Eclipse-Preferences-Plug-in Development-Target Platform). This is useful as a final test that everything will work once installed into Rodin but because it uses a 'built' platform, you don't get access to the Rodin source code (e.g. for de-bugging).
Alternatively, one can develop extensions to the Rodin platform against the
leading edge version of the core plug-ins. This is mandatory when one targets
a future release of the Rodin platform. We make our best to ensure that the
HEAD revision is always working, but some glitches can appear
from time to time. In this case, you will need to check out the Rodin platform
source code from Git into your workspace. See
[[Developer_FAQ#Installing_the_sources_from_Git_in_Eclipse|
Installing the sources from Git in Eclipse]] for further instructions.


=== Testing ===
=== Testing ===


=== Debugging ===
=== Debugging ===
There is nothing special to the Rodin platform as concerns debugging. This is just like debugging any Eclipse plug-in. See for instance [http://eclipse.org/resources/?sort=date&category=Debugging Eclipse Debugging Resources].


=== Publishing ===
=== Publishing ===
Line 91: Line 150:
Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).  
Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).  


First upload your jar files onto the Sourceforge uploads area and then create a new release in the FRS (Admin-file releases). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You must not repeat files that have not changed. Sourceforge does not allow you to upload multiple copies of the same jar file. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release.
Create a new release folder in the FRS (On Sourceforge Rodin project website - Admin-file releases) noting the naming conventions (e.g. Plugin_<mypluginName>) and sub-folder structure conventions (one per release). Now you can upload your jar files using the controls on the releases webpage). Note that you should include a zip of the complete source projects to comply with Sourceforge rules.  
See here for details:- http://alexandria.wiki.sourceforge.net/File+Release+System+-+Offering+Files+for+Download
You should not repeat files that have not changed. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release.


Finally, the update site must be updated to redirect the update requests to the files on the FRS.  
Finally, the update site must be updated to redirect the update requests to the files on the FRS. ([[Details for Uploading Main Rodin Update Site]]).
(Currently this is done by Colin Snook on request - see Rodin developers page for contact details).


[[Details for Maintaining Main Rodin Update Site]]
=== Upgrading and maintain ===
 
== Rodin Developer FAQ ==


see [[FAQ#Developer_FAQ]].
Please note that you should always keep an existing version of your plug-in for the antepenultimate version of Rodin when you want to perform some clean-up of your update site.
Indeed, not all the users switch to the latest version of Rodin by the time of its release, and certainly would like to use your plug-ins anyway.


[[Category:Developer documentation]]
[[Category:Developer documentation]]
[[Category:Rodin Platform]]
[[Category:Rodin Platform]]

Latest revision as of 12:45, 30 July 2015

The Developer Support provides resources for developing plug-ins for the Rodin Platform.

Setting up Eclipse Workspace

1. Building against a version of Rodin

The recommended practice is to work with a target platform, as described in Using Rodin as Target Platform.

Alternatively, one can develop extensions to the Rodin platform against the leading edge version of the core plug-ins. This is mandatory when one targets a future release of the Rodin platform. We make our best to ensure that the HEAD revision is always working, but some glitches can appear from time to time. In this case, you will need to check out the Rodin platform source code from Git into your workspace. See Installing the sources from Git in Eclipse for further instructions.

2. Launching Rodin from Eclipse

To launch Rodin from within Eclipse, a Run Configuration is required. This instructions are for those who set up to use Rodin as a Target Platform.

1. Menu "Run/Run Configurations", to open the "Run Configurations" dialog.

2. Double-click on Eclipse Application on the left-hand side, a "New Configuration" is created

3. In the "Main" tab on the right-hand side, change the name of the configuration, e.g., "Rodin 3.0.1"

4. In the "Main" tab on the right-hand side, choose the "Location" for the run-time workspace

5. In the "Main" tab on the right-hand side, for "Run a product" option, choose "org.rodin.platform.product"

6. In the "Plug-ins" tab on the right-hand side, for "Launch with" option, choose "plug-ins selected below only".

7. In the list of plug-in, unselect all the test plug-ins for Target platform (Use the "tests" for filter the plug-ins and deselect them.

8. Click "Apply"/"Run" to launch Rodin.

3. Build your plug-in

To start to build your plugin, it is recommended to look at the Tutorial. Remember to add your plug-in to the "Run Configuration" when Testing/Debugging your plug-in.

Rodin Developer FAQ

see Developer FAQ.

Architecture of the Rodin Platform

Rodin Platform Core

Event-B User Interface

The Event-B User Interface of the Roding Platform has two major components that are concerned with either modelling in Event-B or proving properties of models.

Apart from these are more minor components.

Event-B Component Library

Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an abstract syntax tree. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a static checker. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The proof obligation generator uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the proof manager attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the proving user interface).

Extending Rodin

Migration to Rodin 3.0

The new release 3.0 of the Rodin platform introduces incompatible changes in the core platform API. The Rodin 3.0 Plug-in Migration Guide describes how to adapt plug-ins that work with Rodin 2.7 to the new 3.0 API.

Useful Hints

Version Control

All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge. The repository currently used is Git and can be accessed using URI

git://git.code.sf.net/p/rodin-b-sharp/rodincore

Building against a version of Rodin

The recommended practice is to work with a target platform, as described in Using Rodin as Target Platform.

Alternatively, one can develop extensions to the Rodin platform against the leading edge version of the core plug-ins. This is mandatory when one targets a future release of the Rodin platform. We make our best to ensure that the HEAD revision is always working, but some glitches can appear from time to time. In this case, you will need to check out the Rodin platform source code from Git into your workspace. See Installing the sources from Git in Eclipse for further instructions.

Testing

Debugging

There is nothing special to the Rodin platform as concerns debugging. This is just like debugging any Eclipse plug-in. See for instance Eclipse Debugging Resources.

Publishing

A Plug-in developed for the Rodin Platform will normally consist of a collection of eclipse 'plugin' projects and a single eclipse 'feature' project. The feature project contains branding information such as logo's icons and licensing details. It is also used to identify your Plug-in so that users can install it. To build your Plug-in use an eclipse 'site' project. This will build the jar files for your plugin projects and a jar for your feature. See eclipse documentation for more details.

Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).

Create a new release folder in the FRS (On Sourceforge Rodin project website - Admin-file releases) noting the naming conventions (e.g. Plugin_<mypluginName>) and sub-folder structure conventions (one per release). Now you can upload your jar files using the controls on the releases webpage). Note that you should include a zip of the complete source projects to comply with Sourceforge rules. You should not repeat files that have not changed. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release.

Finally, the update site must be updated to redirect the update requests to the files on the FRS. (Details for Uploading Main Rodin Update Site).

Upgrading and maintain

Please note that you should always keep an existing version of your plug-in for the antepenultimate version of Rodin when you want to perform some clean-up of your update site. Indeed, not all the users switch to the latest version of Rodin by the time of its release, and certainly would like to use your plug-ins anyway.