FAQ - Revision history

imported>Ladenberger: Replacing page with '[http://handbook.event-b.org/current/html/faq.html Rodin Handbook (FAQ)]'

2011-10-27T10:49:35Z

Replacing page with '[http://handbook.event-b.org/current/html/faq.html Rodin Handbook (FAQ)]'

imported>Nicolas: /* General Tool Usage */

2011-09-06T08:48:00Z

General Tool Usage

← Older revision		Revision as of 08:48, 6 September 2011
Line 17:		Line 17:

	== General Tool Usage ==		== General Tool Usage ==

			=== Rodin does not launch on my 64 bit OS ===

			You are probably running a 64 bit Windows or 64 bit Linux: for these OSes, Rodin is provided in a 32 bit version (Rodin for Mac is 64 bit).
			So you need to have a 32 bit JRE installed to run Rodin.

			Then, you have to tell Rodin where to find it; edit the file "rodin.ini" in your Rodin install directory, then add a "-vm" option, as explained at
			[http://wiki.eclipse.org/Eclipse.ini http://wiki.eclipse.org/Eclipse.ini].

			As Rodin is an Eclipse product, rodin.ini file is very much the same as eclipse.ini file.

	=== Do I lose my proofs when I clean a project ? ===		=== Do I lose my proofs when I clean a project ? ===

imported>Nicolas: /* Do I lose my proofs when I clean a project ? */

2011-06-16T16:23:06Z

Do I lose my proofs when I clean a project ?

← Older revision		Revision as of 16:23, 16 June 2011
Line 27:		Line 27:

	A status may change from ''discharged'' to ''not discharged'' when the proof is no more compatible with the corresponding proof obligation (because hypotheses changed for instance), but '''the proof itself is still there !''' You can try to [[Proof_Obligation_Commands#Proof_Replay_on_Undischarged_POs\|replay]] it.		A status may change from ''discharged'' to ''not discharged'' when the proof is no more compatible with the corresponding proof obligation (because hypotheses changed for instance), but '''the proof itself is still there !''' You can try to [[Proof_Obligation_Commands#Proof_Replay_on_Undischarged_POs\|replay]] it.

			A confusion might arise from the possibility to launch automatic provers upon build. The cleaner does not undo these automatic proofs (why would it ?!!). Once a proof is made, the platform does not modify or delete it by itself. Even [[Proof Purger Interface#Why proofs become obsolete \| obsolete proofs]] are preserved !

	=== How do I install external plug-ins without using Eclipse Update Manager? ===		=== How do I install external plug-ins without using Eclipse Update Manager? ===

imported>Nicolas: /* Do I lose my proofs when I clean a project ? */

2011-06-16T15:55:13Z

Do I lose my proofs when I clean a project ?

← Older revision		Revision as of 15:55, 16 June 2011
Line 26:		Line 26:
	The cleaner just undoes what the builder does, i.e. it removes proof obligations and statuses, but it never modifies any proof.		The cleaner just undoes what the builder does, i.e. it removes proof obligations and statuses, but it never modifies any proof.

	A status may change from ''discharged'' to ''not discharged'' when the proof is no more compatible with the corresponding proof obligation (because hypotheses changed for instance), but the proof itself is still there ! You can try to [[Proof_Obligation_Commands#Proof_Replay_on_Undischarged_POs\|replay]] it.		A status may change from ''discharged'' to ''not discharged'' when the proof is no more compatible with the corresponding proof obligation (because hypotheses changed for instance), but '''the proof itself is still there !''' You can try to [[Proof_Obligation_Commands#Proof_Replay_on_Undischarged_POs\|replay]] it.

	=== How do I install external plug-ins without using Eclipse Update Manager? ===		=== How do I install external plug-ins without using Eclipse Update Manager? ===

imported>Nicolas: /* General Tool Usage */ added do I lose my proofs upon a clean

2011-06-16T15:53:36Z

General Tool Usage: added do I lose my proofs upon a clean

← Older revision		Revision as of 15:53, 16 June 2011
Line 17:		Line 17:

	== General Tool Usage ==		== General Tool Usage ==

			=== Do I lose my proofs when I clean a project ? ===

			No ! This is a common misunderstanding of what a project clean does. A project contains two kinds of files:
			* those you can edit: contexts, machines, proofs
			* those generated by a project build: proof obligations, proof statuses (roughly speaking, for each proof obligation, ''discharged'' or ''not discharged'')

			The cleaner just undoes what the builder does, i.e. it removes proof obligations and statuses, but it never modifies any proof.

			A status may change from ''discharged'' to ''not discharged'' when the proof is no more compatible with the corresponding proof obligation (because hypotheses changed for instance), but the proof itself is still there ! You can try to [[Proof_Obligation_Commands#Proof_Replay_on_Undischarged_POs\|replay]] it.

	=== How do I install external plug-ins without using Eclipse Update Manager? ===		=== How do I install external plug-ins without using Eclipse Update Manager? ===

imported>Nicolas: /* General Tool Usage? */

2011-03-16T13:17:29Z

General Tool Usage?

@@ Line 16: / Line 16: @@
 The Rodin platform was initially developed within the European Commission funded Rodin project (IST-511599 ), where Rodin is an acronym for "Rigorous Open Development Environment for Complex Systems” .  Rodin is also the name of a famous French [http://en.wikipedia.org/wiki/Auguste_Rodin sculptor], one of his most famous work being the [http://en.wikipedia.org/wiki/The_Thinker Thinker].
-== General Tool Usage? ==
+== General Tool Usage ==
 === How do I install external plug-ins without using Eclipse Update Manager? ===
@@ Line 46: / Line 46: @@
 On Windows platforms, it may happen that Rodin crashes, complaining about "no more handles". This is an OS specific limitation, described [http://journals.jevon.org/users/jevon-phd/entry/19833 here] and [https://bugs.eclipse.org/bugs/show_bug.cgi?id=211124 there]. A workaround is provided in [http://blogs.msdn.com/b/ntdebugging/archive/2007/01/04/desktop-heap-overview.aspx this site].
 == Modeling ==

imported>Nicolas: /* General Tool Usage? */

2011-02-17T13:57:53Z

General Tool Usage?

← Older revision		Revision as of 13:57, 17 February 2011
Line 42:		Line 42:
	You have to add a properties by appending the following code to your {{file\|eclipse/eclipse.ini}} or {{file\|rodin/rodin.ini}} file:		You have to add a properties by appending the following code to your {{file\|eclipse/eclipse.ini}} or {{file\|rodin/rodin.ini}} file:
	-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner/xulrunner-xxx		-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner/xulrunner-xxx

			=== No More Handles ===

			On Windows platforms, it may happen that Rodin crashes, complaining about "no more handles". This is an OS specific limitation, described [http://journals.jevon.org/users/jevon-phd/entry/19833 here] and [https://bugs.eclipse.org/bugs/show_bug.cgi?id=211124 there]. A workaround is provided in [http://blogs.msdn.com/b/ntdebugging/archive/2007/01/04/desktop-heap-overview.aspx this site].

	== Modeling ==		== Modeling ==

imported>Laurent: /* What are the ASCII shortcuts for mathematical operators */

2010-07-21T13:01:14Z

What are the ASCII shortcuts for mathematical operators

← Older revision		Revision as of 13:01, 21 July 2010
Line 35:		Line 35:
	===What are the ASCII shortcuts for mathematical operators===		===What are the ASCII shortcuts for mathematical operators===

	The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the ~~event-B~~ keyboard plug-in. In the help system, this page has the following path {{menu\|~~Event-B~~ Keyboard User Guide > Getting Started > Special Combos}}.		The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the Rodin keyboard plug-in. In the help system, this page has the following path {{menu\|Rodin Keyboard User Guide > Getting Started > Special Combos}}.

	This page is also available in the dynamic help system. The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors. To start the dynamic help, click {{menu\|Help > Dynamic Help}}, then click {{menu\|All Topics}} and select the page in the tree.		This page is also available in the dynamic help system. The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors. To start the dynamic help, click {{menu\|Help > Dynamic Help}}, then click {{menu\|All Topics}} and select the page in the tree.


	===Rodin (and eclipse) doesn't take into account the MOZILLA_FIVE_HOME environment variable===		===Rodin (and eclipse) doesn't take into account the MOZILLA_FIVE_HOME environment variable===

imported>Jrloria: move to Developer FAQ

2010-03-26T10:12:08Z

move to Developer FAQ

@@ Line 82: / Line 82: @@
 * {{ident|ML}} means ''discharged by the mono lemma prover''
-== How to contribute? ==
+== How to contribute and develop ? ==
-See the [[How_To_Contribute|How to contribute]] page.
+See the [[Developer FAQ]] page.
 [[Category:User FAQ]]

imported>Son: /* How do I extend the Event-B structure editor (the Edit Tab of the Event-B editor) for editing an attribute (which I added to the Rodin DB as described here)? */

2010-03-24T18:07:02Z

How do I extend the Event-B structure editor (the Edit Tab of the Event-B editor) for editing an attribute (which I added to the Rodin DB as described here)?

← Older revision		Revision as of 18:07, 24 March 2010
Line 150:		Line 150:
	* How the attribute is going to be displayed/edited. This is done by declaring one of the following elements: <code>textAttribute</code>, <code>choiceAttribute</code> or <code>toggleAttribute</code>.		* How the attribute is going to be displayed/edited. This is done by declaring one of the following elements: <code>textAttribute</code>, <code>choiceAttribute</code> or <code>toggleAttribute</code>.

	* The relationship between the attribute and an internal ~~element~~. This is done by declaring an <code>attributeRelation</code> element. Note: In fact, this relationship declares which element '''allows''' to have this attribute, which is not something enforce when the attribute is added as described [[#How do I add a new attribute to existing elements (e.g. Event-B event)?\| here]].		* The relationship between the attribute and internal elements. This is done by declaring an <code>attributeRelation</code> element. Note: In fact, this relationship declares which element '''allows''' to have this attribute, which is not something enforce when the attribute is added as described [[#How do I add a new attribute to existing elements (e.g. Event-B event)?\| here]].

	The detail steps are described in the following page [[Extending the Structure Editor#Adding a New Attribute\|Extending the Structure Editor]].		The detail steps are described in the following page [[Extending the Structure Editor#Adding a New Attribute\|Extending the Structure Editor]].