Scenarios for Merging Proofs - Revision history

imported>Ladenberger: /* Proof structure */

2011-10-27T10:34:36Z

Proof structure

← Older revision		Revision as of 10:34, 27 October 2011
Line 3:		Line 3:
	With respect to the merging objective, a proof is made of:		With respect to the merging objective, a proof is made of:
	# a component name,		# a component name,
	# a unique identifier inside that component, which is same as the [[PO]] identifier,		# a unique identifier inside that component, which is same as the [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/generated_proof_obligations.html PO] identifier,
	# a proof tree, either manual or automatic,		# a proof tree, either manual or automatic,
	# a proof status (PO discharged or not by the proof tree, in fact implemented with a ''confidence'' value: 1000 => proved, 500 => review, <500 => unproved)		# a proof status (PO discharged or not by the proof tree, in fact implemented with a ''confidence'' value: 1000 => proved, 500 => review, <500 => unproved)

imported>Ladenberger: /* Proof structure */

2011-10-27T10:33:51Z

Proof structure

← Older revision		Revision as of 10:33, 27 October 2011
Line 6:		Line 6:
	# a proof tree, either manual or automatic,		# a proof tree, either manual or automatic,
	# a proof status (PO discharged or not by the proof tree, in fact implemented with a ''confidence'' value: 1000 => proved, 500 => review, <500 => unproved)		# a proof status (PO discharged or not by the proof tree, in fact implemented with a ''confidence'' value: 1000 => proved, 500 => review, <500 => unproved)
	# a PO [[sequent]]		# a PO [http://handbook.cobra.cs.uni-duesseldorf.de/current/html/sequents.html sequent]

	== Rodin database implementation ==		== Rodin database implementation ==

imported>Mathieu: /* Complicated scenarios */

2009-08-12T14:35:29Z

Complicated scenarios

← Older revision		Revision as of 14:35, 12 August 2009
Line 87:		Line 87:
	:'''PR X''': proof change for X, compared to others user/branch		:'''PR X''': proof change for X, compared to others user/branch

	A prototype that implement a simpler policy (get ''other'' except if local has a successful manual proof) is being developed at http://~~freehg~~.org/~~u/clabaut~~/proofmerge/.		A prototype that implement a simpler policy (get ''other'' except if local has a successful manual proof) is being developed at http://bitbucket.org/matclab/proofmerge/.
	{{Hidden end}}		{{Hidden end}}

imported>Mathieu: /* Complicated scenarios */

2008-10-03T13:26:56Z

Complicated scenarios

← Older revision		Revision as of 13:26, 3 October 2008
Line 86:		Line 86:
	:'''PO X''': po changes for X compare to others user/branch		:'''PO X''': po changes for X compare to others user/branch
	:'''PR X''': proof change for X, compared to others user/branch		:'''PR X''': proof change for X, compared to others user/branch

			A prototype that implement a simpler policy (get ''other'' except if local has a successful manual proof) is being developed at http://freehg.org/u/clabaut/proofmerge/.
	{{Hidden end}}		{{Hidden end}}

imported>Mathieu: Scenario for Merging Proofs moved to Scenarios for Merging Proofs: Uniformity

2008-10-03T13:08:31Z

Scenario for Merging Proofs moved to Scenarios for Merging Proofs: Uniformity

← Older revision	Revision as of 13:08, 3 October 2008
(No difference)

imported>Mathieu: /* Complicated scenarios */

2008-10-03T12:54:48Z

Complicated scenarios

← Older revision		Revision as of 12:54, 3 October 2008
Line 36:		Line 36:

	=== Complicated scenarios ===		=== Complicated scenarios ===
	{{Hidden\|Complicated scenarios\|		{{Hidden begin\|title=Complicated scenarios}}
	''Those scenarios are kept for reference only''		''Those scenarios are kept for reference only''

Line 86:		Line 86:
	:'''PO X''': po changes for X compare to others user/branch		:'''PO X''': po changes for X compare to others user/branch
	:'''PR X''': proof change for X, compared to others user/branch		:'''PR X''': proof change for X, compared to others user/branch
	}}		{{Hidden end}}

	== User interactions ==		== User interactions ==

imported>Mathieu: /* Complicated scenarios */

2008-10-03T12:54:05Z

Complicated scenarios

← Older revision		Revision as of 12:54, 3 October 2008
Line 38:		Line 38:
	{{Hidden\|Complicated scenarios\|		{{Hidden\|Complicated scenarios\|
	''Those scenarios are kept for reference only''		''Those scenarios are kept for reference only''



	The table hereafter described the envisioned use cases.		The table hereafter described the envisioned use cases.

imported>Mathieu: /* Complicated scenarios */ Hidden

2008-10-03T12:32:35Z

Complicated scenarios: Hidden

← Older revision		Revision as of 12:32, 3 October 2008
Line 36:		Line 36:

	=== Complicated scenarios ===		=== Complicated scenarios ===
	''Those scenarios are kept for reference''		{{Hidden\|Complicated scenarios\|
			''Those scenarios are kept for reference only''


Line 87:		Line 88:
	:'''PO X''': po changes for X compare to others user/branch		:'''PO X''': po changes for X compare to others user/branch
	:'''PR X''': proof change for X, compared to others user/branch		:'''PR X''': proof change for X, compared to others user/branch
			}}

	== User interactions ==		== User interactions ==

imported>Mathieu: user and vcs interactions

2008-10-03T12:27:40Z

user and vcs interactions

← Older revision		Revision as of 12:27, 3 October 2008
Line 89:		Line 89:

	== User interactions ==		== User interactions ==
	~~When asked~~, the ~~user should be able~~ to ~~compare...~~		In the context of [[#Simple scenarios (need database evolution)\|simple scenarios]], no user interactions is requested from user.

			The only interaction envisioned is done after the merge, and is related to digging into [[proof history]]

	== VCS interactions ==		== VCS interactions ==
			With respect to the action of merging the proof, the only interaction with VCS, is the ability to retrieve ''local'', ''other'' and ''ancestors'' {{file\|.bpr}} files.
			It is a very common requirement, which is certainly fulfilled by every descent VCS.


	~~== External Links ==~~
	* [http://help.eclipse.org/stable/topic/org.eclipse.platform.doc.isv/samples/org.eclipse.compare.examples.xml/doc-html/ui_xmlcompare_ex.html org.eclipse.compare.example.xml]
	* [http://www.oxygenxml.com/xml_diff_and_merge.html xml diff GUI example]
	[[Category:Design proposal]]		[[Category:Design proposal]]

imported>Mathieu: /* Simple scenarios (need database evolution) */

2008-10-03T12:23:05Z

Simple scenarios (need database evolution)

← Older revision		Revision as of 12:23, 3 October 2008
Line 25:		Line 25:

	=== Simple scenarios (need database evolution) ===		=== Simple scenarios (need database evolution) ===
	While discussing about the merge topic, it appears that another wanted and related feature is [[multi-proof database]], where the {{file\|compname.bpr}} file contains not only the current proof (called ''main proof''), but also all the proof trees that were once used to ~~proof~~ the PO (the set of those proof ~~tree~~ is called ''proof history'').		While discussing about the merge topic, it appears that another wanted and related feature is [[multi-proof database]], where the {{file\|compname.bpr}} file contains not only the current proof (called ''main proof''), but also all the proof trees that were once used to prove the PO (the set of those proof trees is called ''proof history'').

	Once both ''multi-proof database'' and ''proof reuse'' are implemented, the merge process for the proofs may be the following one:		Once both ''multi-proof database'' and ''proof reuse'' are implemented, the merge process for the proofs may be the following one:
	# [[Requirements for merging models\|merge the model]] (machines and context)		# [[Requirements for merging models\|merge the model]] (machines and context)
	# ~~the~~ new ''proof history'' ~~is made of~~ the union of ''proof histories'' from ''O'' and ''L' plus ~~one of ''O'' or~~ ''L'' ''main proof''		# build new ''proof history'' as the union of ''proof histories'' from ''O'' and ''L' plus, say ''L'' ''main proof''
	# the ~~other~~ ''main proof'' ~~becomes~~ the ~~new~~ ''main proof''		# build the ''main proof'' with the ''O main proof''
	Those steps ~~are totally automatic~~.		Those steps do not need user interacions.

	~~Then the~~ person doing the merge may review the ~~proof~~ that do not replay, and see if one of the history proof tree may help (steps which may also be automated with the help of ''proof reuse'' feature.		The person doing the merge may then review the proofs that do not replay, and see if one of the history proof tree may help (steps which may also be automated with the help of ''proof reuse'' feature).

	=== Complicated scenarios ===		=== Complicated scenarios ===