SMT Solvers Plug-in Developer Support - Revision history

imported>Laurent: Added link to perf application

2014-05-19T14:34:13Z

Added link to perf application

← Older revision		Revision as of 14:34, 19 May 2014
Line 97:		Line 97:
	=== SMT solvers settings ===		=== SMT solvers settings ===
	''See [[SMT_Solvers_Plug-in#SMT_solvers_settings]].''		''See [[SMT_Solvers_Plug-in#SMT_solvers_settings]].''

			== Measuring Performance ==

			There exists an Eclipse Application for measuring the performance of SMT solvers. Its usage is described at [[SMT Plug-in Performance]].

	[[Category:Plugin]]		[[Category:Plugin]]
	[[Category:Developer documentation]]		[[Category:Developer documentation]]

imported>Laurent: Change category to developer

2013-10-12T12:14:29Z

Change category to developer

← Older revision		Revision as of 12:14, 12 October 2013
Line 99:		Line 99:

	[[Category:Plugin]]		[[Category:Plugin]]
	[[Category:~~User~~ documentation]]		[[Category:Developer documentation]]

imported>Tommy: /* Adding the SMT plug-ins to the Run Configuration */

2013-05-27T16:01:36Z

Adding the SMT plug-ins to the Run Configuration

← Older revision		Revision as of 16:01, 27 May 2013
Line 87:		Line 87:
	* org.eventb.smt.cvc3.linux,		* org.eventb.smt.cvc3.linux,
	* org.eventb.smt.cvc3.win32,		* org.eventb.smt.cvc3.win32,
	* org.eventb.smt.cvc3.macosx		* org.eventb.smt.cvc3.macosx.
	and one project from :		and one project from :
	* org.eventb.smt.verit.linux,		* org.eventb.smt.verit.linux,
	* org.eventb.smt.verit.win32,		* org.eventb.smt.verit.win32,
	* org.eventb.smt.verit.macosx		* org.eventb.smt.verit.macosx.

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

imported>Tommy: /* Adding the SMT plug-ins to the Run Configuration */

2013-05-27T16:01:16Z

Adding the SMT plug-ins to the Run Configuration

← Older revision		Revision as of 16:01, 27 May 2013
Line 82:		Line 82:

	[[Image:SMT_Solvers_Dev_Plug-ins_to_select.png\|600px]]		[[Image:SMT_Solvers_Dev_Plug-ins_to_select.png\|600px]]

			NB: You actually just need only one project containing the binaries of CVC3 and VeriT.
			Hence, you just need to select one project which corresponds to your platform from :
			* org.eventb.smt.cvc3.linux,
			* org.eventb.smt.cvc3.win32,
			* org.eventb.smt.cvc3.macosx
			and one project from :
			* org.eventb.smt.verit.linux,
			* org.eventb.smt.verit.win32,
			* org.eventb.smt.verit.macosx

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

imported>Tommy: /* Adding the SMT plug-ins to the Run Configuration */

2013-05-21T11:10:13Z

Adding the SMT plug-ins to the Run Configuration

← Older revision		Revision as of 11:10, 21 May 2013
Line 81:		Line 81:
	* ''org.eventb.smt.ui.tests''.		* ''org.eventb.smt.ui.tests''.

	[[Image:SMT_Solvers_Dev_Plug-ins_to_select.png]]		[[Image:SMT_Solvers_Dev_Plug-ins_to_select.png\|600px]]

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

imported>Tommy: /* Adding the SMT plug-ins to the Run Configuration */

2013-05-21T10:16:48Z

Adding the SMT plug-ins to the Run Configuration

← Older revision		Revision as of 10:16, 21 May 2013
Line 76:		Line 76:
	Close the Rodin Platform. Back in the Eclipse Platform, go to the Run Configuration: ''Run > Run Configurations...''.		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''.		Select the ''Rodin.product'' configuration, and go to the ''Plug-ins'' tab. <br/>
			Check all the SMT Plug-ins except :
			* ''org.eventb.smt.core.tests'' and
			* ''org.eventb.smt.ui.tests''.

	[[Image:~~Plug~~-~~ins to select~~.png~~\|525px~~]]		[[Image:SMT_Solvers_Dev_Plug-ins_to_select.png]]

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

imported>Tommy at 10:08, 21 May 2013

2013-05-21T10:08:43Z

← Older revision		Revision as of 10:08, 21 May 2013
Line 9:		Line 9:
	* Optionnally, install custom SMT solvers if you want to use some.		* Optionnally, install custom SMT solvers if you want to use some.

	=== Installing the Eclipse Platform ===		== Installing the Eclipse Platform ==
	If you don't have an Eclipse development platform for Java and Eclipse plug-ins installed, then :		If you don't have an Eclipse development platform for Java and Eclipse plug-ins installed, then :
	* Download Eclipse Classic (SDK) or Eclipse for RCP and RAP Developers at http://www.eclipse.org/downloads/ <br/>		* Download Eclipse Classic (SDK) or Eclipse for RCP and RAP Developers at http://www.eclipse.org/downloads/ <br/>
	* 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].

	=== Get ~~the~~ Rodin ~~sources =~~==		== Get a Rodin host plaform ==
			There are two possibilities:
			* OPTION 1: Develop with the latest sources of the platform (developpment branch).
			* OPTION 2: Use a target platform.

			=== Use a Rodin platform running from the Rodin sources ===
	Rodin Core sources are available from a Git repository on Sourceforge.		Rodin Core sources are available from a Git repository on Sourceforge.

Line 22:		Line 26:

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

			=== Use a Rodin target platfom ===
			You can also use a predefined target platform to be used as an host for the SMT Solvers plug-in you will develop.
			To get more information about this, please read [http://wiki.event-b.org/index.php/Using_Rodin_as_Target_Platform].


	=== Downloading the SMT Plug-in Sources ===		=== Downloading the SMT Plug-in Sources ===

imported>Tommy at 09:57, 21 May 2013

2013-05-21T09:57:37Z

← Older revision		Revision as of 09:57, 21 May 2013
Line 2:		Line 2:
	{{TOCright}}		{{TOCright}}

	==Installation from the sources==		== Installation from the sources ==
	~~You~~ will need to:		To start developping the sources of the SMT Solvers plug-in, you will need to:
	* Install ~~the~~ Eclipse Platform.		* Install an Eclipse Platform (to be used as the IDE for the developpment of the SMT Solvers plug-in sources).
	* Install the ~~Subclipse~~ plug-in ~~to use SVN in Eclipse~~.		* Clone the Rodin sources and import them into Eclipse or set a Rodin Platform as a ''target platform''.
	* Clone the Rodin sources and import them into Eclipse.		* Clone the SMT plug-in sources and import them into Eclipse.
	* Clone the SMT plug-in sources and import into Eclipse.		* Optionnally, install custom SMT solvers if you want to use some.
	** 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 ===		=== Installing the Eclipse Platform ===
	Download Eclipse Classic (SDK) or Eclipse for RCP and RAP Developers at http://www.eclipse.org/downloads/ <br/>		If you don't have an Eclipse development platform for Java and Eclipse plug-ins installed, then :
	Install it [http://wiki.eclipse.org/FAQ_Where_do_I_get_and_install_Eclipse%3F].		* Download Eclipse Classic (SDK) or Eclipse for RCP and RAP Developers at http://www.eclipse.org/downloads/ <br/>
			* Install it [http://wiki.eclipse.org/FAQ_Where_do_I_get_and_install_Eclipse%3F].

	=== Get the Rodin sources ===		=== Get the Rodin sources ===
Line 32:		Line 31:

	Then, from Eclipse, check out all projects of this cloned repository (i.e. use ''File > Import... > Existing projects in workspace'').		Then, from Eclipse, check out all projects of this cloned repository (i.e. use ''File > Import... > Existing projects in workspace'').
			The folling plug-ins are necessary to run the SMT Solvers plug-in:
			''org.eventb.smt''
			''org.eventb.smt-feature''
			''org.eventb.smt.core''
			''org.eventb.smt.core.performance''
			''org.eventb.smt.core.tests''
			''org.eventb.smt.cvc3''
			''org.eventb.smt.cvc3.linux''
			''org.eventb.smt.cvc3.macosx''
			''org.eventb.smt.cvc3.win32''
			''org.eventb.smt.help''
			''org.eventb.smt.releng''
			''org.eventb.smt.ui''
			''org.eventb.smt.verit''
			''org.eventb.smt.verit.linux''
			''org.eventb.smt.verit.macosx''
			''org.eventb.smt.verit.win32''

	== Launch configuration ==		== Launch configuration ==

imported>Tommy: /* Installation from the sources */

2013-05-21T09:49:14Z

Installation from the sources

← Older revision		Revision as of 09:49, 21 May 2013
Line 6:		Line 6:
	* Install the Eclipse Platform.		* Install the Eclipse Platform.
	* Install the Subclipse plug-in to use SVN in Eclipse.		* Install the Subclipse plug-in to use SVN in Eclipse.
	* ~~Download~~ Rodin sources into Eclipse.		* Clone the Rodin sources and import them into Eclipse.
	* ~~Download~~ SMT plug-in sources into Eclipse.		* Clone the SMT plug-in sources and import into Eclipse.
	** Install veriT if you want to use it (instead of ppTrans) to translate Event-B to SMT-LIB.		** 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.		* Install the SMT solvers you want to use.

imported>Tommy at 09:44, 21 May 2013

2013-05-21T09:44:54Z

← Older revision		Revision as of 09:44, 21 May 2013
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.