Report on a change and merge two lines

Classify what a revision or reference move changes, then join two lines of revisions at their common base.

Change reports and merges are worked out by identity from the project records (binding maps, assets and authoring bundles), never from source text. Nothing here is a check by the pinned Lean 4.34.1 kernel: a report reads the receipts that kernel replay wrote and the witnesses that replace, refine and correct recorded.

Before you start

• A running server on a store with a project reference and revisions, as in Set up a project reference. In the commands, $SOCK is the server’s socket.
• For a merge, two revisions whose lines share an ancestor.

1. Report on a change

Choose what to compare:

lema --socket $SOCK report --revision $REV               # a revision, from its before-snapshot
lema --socket $SOCK report --ref main                    # the reference's latest move
lema --socket $SOCK report --ref main --generation 3     # one recorded move
lema --socket $SOCK report --after $S2 --before $S1      # two snapshots, nothing cited

Each prints id and report. A report (lema.change-report/v1) is computed each time, not stored, and the same store state gives the same report and ID.

2. Read the classification

Each change falls into one category, which says what evidence it needs:

Evidence the store already holds (kernel receipts, and replace, refine and correct witnesses) is found by identity, so a revision need not cite it. For rebinds, substitutions, evolutions and removals, old_still_used lists the exports and roots that still hold the old object.

A report is conservative when every change adds an export or root, or is material that needs only its digest. Any other change makes it non-conservative, and so does a configuration or asset file.

3. Carry the open obligations

Missing evidence appears as open obligations, in the same format a revision uses, and uncarried lists the ones the revision does not carry. The report does not block publication. To keep the obligations on record, create the revision with them in --obligations-file (a JSON list). Every later revision must then carry or discharge each one, and a policy with require.no_obligations refuses a revision that has any open.

Removing an export always leaves an obligation open, because the store has no deprecation record. Only a waiver closes it, and only an actor listed under the policy’s waive can bring a waiver into the reference.

4. Find the common base

A merge needs a nearest common ancestor of its parents: a common ancestor that no other common ancestor descends from. List both lines:

lema --socket $SOCK revision log $OURS
lema --socket $SOCK revision log $THEIRS

lema merge refuses a base that is not a nearest common ancestor, and names the nearer ones. In a criss-cross history any of the nearest ones will do.

5. Merge the two lines

lema --socket $SOCK merge --parents $OURS,$THEIRS --base $BASE

The merge compares each parent’s after-snapshot with the base’s, key by key: exports by name, assets and sources by path, and notes by object. Roots and authoring bundles are compared as sets. A key that one side changed takes that side’s value, and a key that both sides changed in the same way takes that value. Anything else is a conflict:

Source texts are never merged line by line. The command prints the merge record’s id, created, the record itself (merge) and, when any parent has open obligations, inherited. The record names the merged snapshot (after) only once every conflict is resolved.

6. Resolve the conflicts

Write a resolution for the conflicts, and only the conflicts. Replace the placeholder with the object you choose:

{"exports": {"app.main": {"id": "<chosen object ID>"}}, "assets": {"notes.md": null}}

exports and assets give each conflicting key its value, or null to remove it. renames says which names keep the object in a rename-rename conflict, and authoring lists the merged authoring bundles. A key that is not in conflict is refused (other changes belong in a later revision), and so is a resolution that would undo a clean change.

lema --socket $SOCK merge --parents $OURS,$THEIRS --base $BASE --resolve-file resolve.json

7. Record and publish the merge revision

lema --socket $SOCK revision create --after $MERGED --intent "Merge the parser line." \
  --parents $OURS,$THEIRS --base $BASE --obligations-file inherited.json

$MERGED is the merge record’s after, and inherited.json holds the command’s inherited list. Keep the parents in the same order: the first is the line the reference is on. Then publish the merge revision to that reference as in Set up a project reference. If a merged line waived an obligation that the reference’s history does not hold yet, the publishing actor must be listed under waive.

A report on the merge revision adds a merge section. It shows each conflict with what the after-snapshot chose, and which evidence cited on the merged lines still covers the merged selection. Where the after-snapshot departs from the merge outside the resolved conflicts, the key is listed under overridden. A base that is not nearest is listed under nearer. Each of these adds an open obligation.

These are store rules, tested without a runtime (crates/lema-store/tests/changes.rs).