Projects, history and review

How Lema versions a project's selection of objects and its evidence by identity, and what LemaHub would add.

Suppose you rename an exported function and, the same afternoon, shorten the proof of a lemma it depends on. In a Git repository both are text diffs. The second also changes the file the lemma lives in, so a file-based build re-checks everything downstream of it. In a Lema store the rename changes one name and no object. The proof edit gives the lemma a new proof, and the statement, template and proof objects of everything that cites the lemma keep their IDs. Lema’s version control is built on that difference.

Objects, not files

Git versions files. In Lema the unit of meaning is a canonical object with an ID (Code stored by identity), and source files and names are views of objects. Three consequences shape the rest of this page:

• A rename is an alias move, or an export renamed in a binding map. No object’s ID depends on a name, so nothing is re-addressed and no proof is re-checked.
• Objects cite theorems by statement and definitions by template. A new proof of a theorem rebuilds the satisfaction and declaration objects that bind it, transitively up to the roots. This is a rebinding, and those objects still need kernel replay by the pinned Lean 4.34.1 kernel. Records and inductive families are cited concretely, so a change beneath one of them does re-address it.
• A different implementation has a different template. Putting it in place of the old one is a substitution, not a rebinding, and it needs a replacement claim.

A project’s history is a second graph beside the dependency graph. History records (binding maps, snapshots, revisions, policies) name objects, but no object cites a record, so history never changes an object’s ID. Git still holds the lema-lang repository’s own Rust and Lean sources. Its file-oriented workflow cannot express statements, realization bindings or replacement claims, though, so a store’s contents are versioned in the store.

Aliases move under an expectation

An alias is a store record outside identity: aliases.json maps a name to {id, role?, generation}. Every request that moves an alias names what it expects the alias to hold now. That is null for a new name, {id}, or {id, generation} as the find method returns it. A stale expectation is refused. An explicit overwrite: true skips the check, and the history records the change as an overwrite.

An alias starts at generation 1, and each move adds one. Aliases are never removed, so a generation is never reused, and an expectation with a generation detects A → B → A. An optional idempotency key binds the request’s digest, so a retry after a lost response returns the first response instead of applying the change again. Each request’s changes are written as one history line, which is the commit point. Aliases are not authenticated: any client of the server can move one, given a correct expectation. Move an alias safely gives the steps.

Bundles name a set of objects once

A bundle (lema.bundle/v1) is an export map over accepted objects: names, roles and IDs. An elaborate request can receive a bundle and have every export bound as a Received.* name, so you do not list each binding by hand. One lemma can appear in several bundles with one identity. Bundles only organize objects. They hide nothing from replay, give no confidentiality or abstraction, and receiving one cannot change the bindings stored in the objects it names. See Name a set of objects with a bundle.

Snapshots and revisions

A binding map selects a project’s roots and exported names, each pinned to an exact object ID. A snapshot is a binding map plus separately referenced material. That material is authoring bundles (original Lean source, source-to-object mappings and notes) and assets, which are referenced by SHA-256 and size; the store does not hold their bytes. Editing documentation changes the snapshot but not the binding map. Two histories that reach the same state share a snapshot ID and have different revision IDs.

A revision goes from its first parent’s snapshot, or from the empty state, to a new snapshot. It carries:

• an intent, free text of 1 to 4,096 bytes;
• evidence: the accepted objects or stored guarantee records it cites;
• obligations: every claim still open after it, inherited from its parents.

Obligations do not disappear by being left out. Each one open in a parent is either carried, exactly, or discharged. It can be discharged by an accepted theorem whose statement is the obligation’s statement, matched by identity, or by a recorded waiver. A merge revision lists all its parents and a separate common base.

Project references move only under a policy

A project reference (ref) is a name pointing to {policy, revision, generation}. ref.create starts it at the empty state. After that it moves only through two methods, and each names the revision, generation and policy version it expects:

• ref.publish moves it to a revision whose first parent is its current revision, or, as a reset, back to an ancestor;
• ref.adopt moves it to the next version of its policy.

The active policy (lema.policy/v1) decides which actors may publish, reset, adopt and waive. It also sets what a revision must meet: an axiom ceiling over its closure (require.axioms), IR profiles over named exports, or no open obligations. An incoming policy never authorizes its own adoption. The active one does, and the reference’s revision must also meet the incoming policy. A policy can protect exports with gates that pin, by identity, the claim a change must present (Implements, Replaces or Refines). It can also require reviews, and approvals count in addition to the evidence, never in place of it. Each move is one history line with its actor and the policy’s decision.

The operator registers actors, and local bearer tokens authenticate them. That keeps cooperating actors apart, such as an agent and a human steward. It does not stop a hostile local user, who can write the store’s files directly. Stronger authentication would come with a hosted service. Set up a project reference walks through one.

Change reports and merges by identity

A change report (lema.change-report/v1) is computed from these records, not from source text. It classifies what a revision changes and names the evidence each change needs:

Evidence the store already holds, such as receipts and witnesses, is found by identity. Missing evidence is listed as open obligations. The same store state gives the same report and the same report ID.

A merge compares each parent’s snapshot with a nearest common ancestor, key by key. If one side changed a key, the merge takes that side’s value. If two sides changed it differently, that is a conflict (collision, delete-update, update-update, rename-rename or bundle). Source texts are not merged as text, and immutable objects are never merged. A resolution only chooses between bindings. Evidence cited on a merged line is reused only where its premises still hold in the merged selection, and a property claimed of the combination still needs its own evidence. Report on a change and merge two lines shows the commands.

Inspection pages and approval views

lema site build writes static pages for the references, releases and pending reviews it is given. They are plain HTML with no script and a content security policy of default-src 'none', with Markdown and JSON beside each page and an optional llms.txt. Object and release pages have stable URLs. A declaration’s page leads with its statement in the contract view and keeps its three evidence panels apart (Checked, tested and assumed). The pages hold only the selection’s closure, so knowing an object’s ID gives no page for it.

An approval view (approval/<name>/<subject>) shows a pending move as a review of it would bind it. Its display digest covers the transition, the policy version, the closure, each declaration’s text and name map, the arguments the text leaves to Lean, and the renderer’s version. A review that carries the digest counts only while the subject still displays exactly that, so any change to the renderer stops such reviews from counting. See Build static inspection pages.

What LemaHub would add, and what exists

The research note docs/research/version-control-modules-and-lemahub.md proposes LemaHub: public discovery and collaboration over the same protocol as local development. Its public pages would work without JavaScript or login. They would have stable object and project version URLs, .lema contract views, original .lean proof scripts, portable exports, deterministic Git mirrors and an optional /llms.txt. A hosted service would not be needed for identity or proof authority. The note says of itself: “It is not an adopted specification or a claim that the proposed features are implemented.”

What is built is the static generator, lema site build, which decision 0031 set as this stage’s scope. Hosting, login and authentication, search, a desktop GUI, portable object bundles, Git mirrors and receipts from other machines are not built.

What this layer claims

Alias moves and bundles also run in native suites that passed. Project records, change reports, merges, protected references and the site generator are store rules tested without a runtime, over placeholder receipts. Their native suites are written but not yet run. Nothing in this layer is a kernel check. It reads receipts that kernel replay wrote, and it matches a theorem to an obligation by statement identity, relying on that theorem’s acceptance.