Difference between pages "Rodin Developer Support" and "Rodin Editor"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
(→‎Building against a version of Rodin: Change recommended practice)
 
imported>Tommy
m (New page: Return to Rodin Plug-ins The Rodin Editor is a new editor based on the same principles as the historical structured Event-B Editor. This latter editor shown its weakness while editing...)
 
Line 1: Line 1:
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
+
Return to [[Rodin Plug-ins]]
  
 +
The Rodin Editor is a new editor based on the same principles as the historical structured Event-B Editor. This latter editor shown its weakness while editing large models. Furthermore, it was impossible to show some information, which is needed when one edits an Event-B model, such as the inherited elements which were formerly displayed only in the pretty print view.
  
== Rodin Developer FAQ ==
+
=== Installation Details ===
  
see [[Developer FAQ]].
+
=== How do I use it ? ===
  
== Architecture of the Rodin Platform ==
 
  
=== Rodin Platform Core ===
+
=== Available keyboard shortcurts ===
  
* [[Database]]
+
==== Customize this list ====
  
* [[Builder]]
+
==== Tips ====
  
* [[Rodin Index Design]]
+
[[Category:Plugin]]
 
+
[[Category:User documentation]]
* [[Indexing System]]
 
 
 
* [[Undo Redo]]
 
 
 
* [[File Root Separation]]
 
 
 
=== Event-B User Interface ===
 
 
 
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.
 
 
 
* [http://handbook.event-b.org/current/html/event_b_perspective.html Modelling User Interface]
 
 
 
* [http://handbook.event-b.org/current/html/proving_perspective.html Proving User Interface]
 
 
 
Apart from these are more minor components.
 
 
 
* [[Proof Purger Design|Proof Purger]] allows to delete unused proofs.
 
 
 
* [[Proof Skeleton Design]] is a view that displays skeletons of existing proofs
 
 
 
* [[Auto-Completion Design]] proposes a list of names to the user editing a model
 
 
 
=== 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 [http://handbook.event-b.org/current/html/proving_perspective.html proving user interface]).
 
 
 
* [[Abstract Syntax Tree]]
 
 
 
* [[Static Checker]]
 
 
 
* [[Proof Obligation Generator]]
 
 
 
* [[Proof Manager]]
 
 
 
* [[Proof Simplification]]
 
 
 
== Extending Rodin ==
 
 
 
* [[Developer Documentation]]
 
 
 
* [[Plug-in Tutorial]]
 
 
 
* [[Extending the Rodin Database]]
 
 
 
* [[Extending the project explorer]]
 
 
 
* [[Extending the Structure Editor]]
 
 
 
* [[Extending the Pretty Print Page]]
 
 
 
* [[Extending the Proof Manager]]
 
 
 
* [[Extending the Index Manager]]
 
 
 
* [[Extending the Static Checker]]
 
 
 
* [[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 ==
 
 
 
=== 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].
 
 
 
=== 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 from Subversion 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 Subversion into your workspace using the 'Releng' plug-in.  See
 
[[Developer_FAQ#Installing_the_sources_from_Subversion_in_Eclipse|
 
Installing the sources from Subversion 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 [http://eclipse.org/resources/?sort=date&category=Debugging 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.
 
 
 
[[Category:Developer documentation]]
 
[[Category:Rodin Platform]]
 

Revision as of 16:13, 1 July 2011

Return to Rodin Plug-ins

The Rodin Editor is a new editor based on the same principles as the historical structured Event-B Editor. This latter editor shown its weakness while editing large models. Furthermore, it was impossible to show some information, which is needed when one edits an Event-B model, such as the inherited elements which were formerly displayed only in the pretty print view.

Installation Details

How do I use it ?

Available keyboard shortcurts

Customize this list

Tips