Scenarios for Merging Proofs

This page is a first tentative to describe the scenario that a merge tool will have to face.

Proof structure

With respect to the merging objective, a proof is made of:

1. a component name,
2. a unique identifier inside that component, which is same as the PO identifier,
3. a proof tree, either manual or automatic,
4. a proof status (PO discharged or not by the proof tree)
5. a PO sequent

Rodin database implementation

Each component

compname

is associated with:

• a
  compname.bpr
  file, which contains the proof trees associated with each PO (1/, 2/ and 3/ before).
• a
  compname.bps
  file, which contains the proof status associated with each PO (2/, 5/ and 3/ - discharged or not, manual or automatic)
• a
  compname.bpo
  file, which contains the PO (1/ and 2/ + PO content).

Merging scenarios

PO being uniquely identified, it may be enough to consider a merge taking place PO by PO.

In the following we call L the local database/user/branch, O the other database/user/branch and A the database which reflects the common state from which L and O have departed (A, for ancestor). We also consider L and O as being symmetrical (and thus we won't describe symmetrical scenarios).

The table hereafter described the envisioned use case.

n°	A st	L st	O st	A ma	L ma	O ma	PO L	PO O	PR L	PR O	Actions
1	-	nok	nok	-	-	-	=A	/=A	-	-	get PR O (O model has changed)
2	nok	nok	nok	-	-	-	=A	=A	/=A	=A	get PR L (L has perhaps tried a demo)
3	nok	nok	nok	-	-	-	=A	=A	/=A	/=A	ask user (both PR changed)
4	nok	nok	nok	-	-	-	=A	=A	=A	=A	get PR L (or O, no difference)
5	nok	ok	nok	-	-	-	-	-	-	-	get PR L
6	nok	ok	ok	-	-	-	=A	/=A	-	-	get PR O, (O model has changed)
7	nok	ok	ok	-	-	-	=A	=A	-	-	ask user (both demo are ok)
8	nok	ok	ok	-	-	-	=A	=A	-	-	ask user (both model have changed)
9	ok	nok	nok	-	-	-	=A	=A	/=A	-	get PR A (model has not changed and was proved)
10	ok	nok	nok	-	-	-	=A	=A	=A	=A	get PR A (model has not changed and was proved)
11	ok	ok	nok	-	-	-	=A	=A	-	-	get PR L (no model has changed)
12	ok	ok	nok	-	ma	au	=A	/=A	-	-	get PR L (O model has changed but L had a manual proof)
13	ok	ok	nok	-	au	ma	=A	/=A	-	-	get PR O (O model has changed and has a manual proof)
14	ok	ok	nok	-	ma	ma	=A	/=A	-	/=A	get PR O (O model has changed and has a new manual proof)
15	ok	ok	nok	-	ma	ma	=A	/=A	-	=A	get PR O (O model has changed)
16	ok	ok	nok	-	au	au	=A	/=A	-	-	get PR O (O model has changed)
17	ok	ok	nok	-	ma	au	/=A	/=A	-	-	get PR L (both model changed but L had a manual proof)
18	ok	ok	nok	-	ma	ma	/=A	/=A	-	-	ask user (both model changed with manual proof)
19	ok	ok	nok	-	au	au	/=A	/=A	-	-	ask user (both model changed with manual proof)

X st: (ok,nok) proof status for X (A,O or L)

X ma: (manual, automatic) manual status for X (A,O or L)

PO X: po changes for X compare to others user/branch

PR X: proof change for X, compared to others user/branch