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)

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.

TODO: Describe the different scenarios, and the proposed merging actions