Difference between revisions of "SMT Solvers Plug-in Developer Support"

From Event-B
Jump to navigationJump to search
imported>Tommy
m
imported>Tommy
m
Line 15: Line 15:
 
Install it [http://wiki.eclipse.org/FAQ_Where_do_I_get_and_install_Eclipse%3F].
 
Install it [http://wiki.eclipse.org/FAQ_Where_do_I_get_and_install_Eclipse%3F].
  
−
=== Installing the Subclipse plug-in ===
+
=== Get the Rodin sources ===
−
Launch Eclipse and go to ''Help > Install New Software...''.
 
  
−
Click the ''Add'' button and type:
+
Rodin Core sources are available from a Git repository on Sourceforge.
  
−
http://subclipse.tigris.org/update_1.6.x
+
To use these sources, invoke the following command locally :
 +
git clone http://git.code.sf.net/p/rodin-b-sharp/rodincore rodin-b-sharp-rodincore
  
−
Name it (ex: SUBCLIPSE 1.6).
+
Then, from Eclipse, check out all projects of this cloned repository (i.e. use ''File > Import... > Existing projects in workspace'').
  
−
Then select the same items as in the following image:
+
=== Downloading the SMT Plug-in Sources ===
−
 
 
−
[[Image:Subclipse_selection.png|600px]]
 
−
 
 
−
Under Linux, in order to use JNI, you'll need to install the following packages:
 
−
    * libsvn-java
 
−
    * subversion
 
−
    * libsvn1
 
−
and to link the installation directory in eclipse.ini, by adding:
 
−
 
 
−
-Djava.library.path=/usr/lib/jni
 
  
−
then restart Eclipse and select ''JavaHL'' in ''Window > Preferences > Team > SVN''.
+
SMT plug-in sources are availbable from a Git repository on Sourceforge.
  
−
=== Downloading the Rodin Sources ===
+
To start your developpement of the SMT plug-in, invoke the following command locally :
−
Open the ''SVN Repository Exploring'' perspective.
+
git clone http://git.code.sf.net/p/rodin-b-sharp/smt rodin-b-sharp-smt
−
 
 
−
Right-clic in the ''SVN Repositories'' view, then ''New > Repository Location''. Enter the following URL : https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp
 
−
 
 
−
Select all projects in ''trunk > RodinCore'' then right-clic and ''Checkout...''.
 
−
 
 
−
[[Image:Rodin selection checkout.png|400px]]
 
−
 
 
−
''Check out into the workspace as projects'' must be selected. Then click ''Finish''.
 
−
 
 
−
The download might be long (might take around 15min), do not interrupt.
 
−
{{warning|Once all the sources are downloaded, get back to the ''Java'' perspective. ''org.eventb.core.seqprover'' and ''org.eventb.core.seqprover.tests'' projects might need to be recompiled: select the former and press ''F5''.}}
 
−
 
 
−
=== Downloading the SMT Plug-in Sources ===
 
−
Do the same as to dowload Rodin sources, with projects in ''trunk > exploratory > fages'':
 
−
* org.eventb.smt.core
 
−
* org.eventb.smt.core.tests
 
−
* org.eventb.smt.help
 
−
* org.eventb.smt.ui
 
−
* org.eventb.smt.ui.tests
 
  
−
== Configuration ==
+
Then, from Eclipse, check out all projects of this cloned repository (i.e. use ''File > Import... > Existing projects in workspace'').
  
−
You'll need to:
+
== Launch configuration ==
 +
To run a Rodin platform, from the sources in the developpment workspace, you'll need to create an Eclipse launch configuration:
 
* Launch the Rodin platform as to set the default ''Run Configuration''.
 
* Launch the Rodin platform as to set the default ''Run Configuration''.
 
* Add the SMT plug-ins to this configuration.
 
* Add the SMT plug-ins to this configuration.

Revision as of 09:44, 21 May 2013

For user support, see SMT Solvers Plug-in

Installation from the sources

You will need to:

  • Install the Eclipse Platform.
  • Install the Subclipse plug-in to use SVN in Eclipse.
  • Download Rodin sources into Eclipse.
  • Download SMT plug-in sources into Eclipse.
    • Install veriT if you want to use it (instead of ppTrans) to translate Event-B to SMT-LIB.
  • Install the SMT solvers you want to use.

Installing the Eclipse Platform

Download Eclipse Classic (SDK) or Eclipse for RCP and RAP Developers at http://www.eclipse.org/downloads/
Install it [1].

Get the Rodin sources

Rodin Core sources are available from a Git repository on Sourceforge.

To use these sources, invoke the following command locally : git clone http://git.code.sf.net/p/rodin-b-sharp/rodincore rodin-b-sharp-rodincore

Then, from Eclipse, check out all projects of this cloned repository (i.e. use File > Import... > Existing projects in workspace).

Downloading the SMT Plug-in Sources

SMT plug-in sources are availbable from a Git repository on Sourceforge.

To start your developpement of the SMT plug-in, invoke the following command locally : git clone http://git.code.sf.net/p/rodin-b-sharp/smt rodin-b-sharp-smt

Then, from Eclipse, check out all projects of this cloned repository (i.e. use File > Import... > Existing projects in workspace).

Launch configuration

To run a Rodin platform, from the sources in the developpment workspace, you'll need to create an Eclipse launch configuration:

  • Launch the Rodin platform as to set the default Run Configuration.
  • Add the SMT plug-ins to this configuration.
  • Set the SMT solvers you want to use within Rodin.

Launching the Rodin Platform

Once we have downloaded the Rodin sources, and built it within Eclipse, we can launch the Rodin platform.

Enter the org.rodinp.platform project and right-clic Rodin.product file then choose Run As... > Eclipse Application.

Run As EclipseApp.png

The Rodin platform is launched and ready.

Adding the SMT plug-ins to the Run Configuration

Close the Rodin Platform. Back in the Eclipse Platform, go to the Run Configuration: Run > Run Configurations....

Select the Rodin.product configuration, and go to the Plug-ins tab. Check all the SMT Plug-ins except org.eventb.smt.core.tests and org.eventb.smt.ui.tests.

Plug-ins to select.png

Now, you can launch the Rodin platform extended with the SMT plug-in.

SMT solvers settings

See SMT_Solvers_Plug-in#SMT_solvers_settings.

Retrieved from ‘https://wiki.event-b.org/index.php?title=SMT_Solvers_Plug-in_Developer_Support&oldid=9247’