Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 9 additions & 8 deletions dag/gunbc/scm/ancestry.dag
Original file line number Diff line number Diff line change
Expand Up @@ -33,19 +33,20 @@ import std.minted_identity { MintedId, minted_id_eq }
// row list, and it is refused here for the same reason and one layer deeper.
//
// EXACTLY ONE PARENT, AND THIS IS THE DECISION THAT WOULD BE UNWRITABLE LATER, so it is derived from
// what the model's own merge does rather than from what git does.
// what this model's own commit-producing operation does rather than from what git does.
//
// gunbc.scm.merge `merge` takes ONE target Commit and a LIST OF PROPOSALS, and answers `Merged`
// carrying ONE commit. A Proposal is a set of authored requirements -- it is not a commit, it has no
// root, no message and no identity in history. So a merge in THIS model combines one commit with N
// things that were never commits, and the result has exactly one commit antecedent. Git's second
// parent exists because git merges two BRANCHES, which are two commits; that shape has no referent
// here, because nothing in this model can merge two commits at all.
// gunbc.scm.role_requirement_integration `integrate_role_requirements` takes ONE target Commit and
// a LIST OF PROPOSALS, and answers `RoleRequirementsIntegrated` carrying ONE commit. A Proposal is a
// set of authored requirements -- it is not a commit, it has no root, no message and no identity in
// history. So that operation combines one commit with N things that were never commits, and the
// result has exactly one commit antecedent. Git's second parent exists because git merges two
// BRANCHES, which are two commits; that shape has no referent here, because nothing in this model
// performs a two-commit merge at all.
//
// So a parent LIST would not be more general, it would be a state with no producer -- an arm nothing
// can construct, which DESIGN section 4b rules worse than absent because it gets cited as capability
// the model does not have. WIDENING TRIGGER, stated so the reason is checkable rather than trusted:
// if `merge` ever takes two Commits rather than one commit and N proposals, this coproduct gains a
// if an operation ever takes TWO Commits rather than one commit and N proposals, this coproduct gains a
// several-parents arm, and the change is a compile error at every consumer rather than a silent
// reinterpretation -- which is what makes single-parent a safe decision now rather than an
// irreversible one.
Expand Down
22 changes: 12 additions & 10 deletions dag/gunbc/scm/authoring.dag
Original file line number Diff line number Diff line change
Expand Up @@ -14,37 +14,38 @@ module gunbc.scm.authoring

import std.types { Bool, List, String }
import v2.std.node { Symbol }
import gunbc.scm.merge {
import gunbc.scm.proposal {
Requirement,
RequireBinding,
RequireBindingAbsent,
Proposal,
requirement_role,
}

// THE ROLE-CONFLICT RULE IS DERIVED, AND IT LANDS OPPOSITE TO merge's -- WHICH IS THE POINT.
// THE ROLE-CONFLICT RULE IS DERIVED, AND IT LANDS OPPOSITE TO THE INTEGRATION'S -- WHICH IS THE POINT.
//
// gunbc.scm.merge `apply_requirement` states its rule in the strongest terms available: "ONLY THE
// gunbc.scm.role_requirement_integration `apply_requirement` states its rule in the strongest terms available: "ONLY THE
// FIRST AUTHORING RESOLVES THE ROLE. A later competing authoring is recorded as an alternative and
// must NOT overwrite it: silently taking the last writer is the fabricated winner this outcome type
// exists to refuse." Read naively, that settles this module too, and `add` would have to refuse the
// second add of a role -- or record it as a contested alternative.
//
// It does not settle it, because the two operations are asked DIFFERENT QUESTIONS about different
// populations, and the merge rule's own justification is what shows this:
// populations, and the integration rule's own justification is what shows this:
//
// MERGE combines proposals from SEVERAL AUTHORS. Two requirements for one role are two PARTIES
// ROLE-REQUIREMENT INTEGRATION combines proposals from SEVERAL AUTHORS. Two requirements for one role are two PARTIES
// who each believe theirs is right, and neither authored in knowledge of the other. There is no
// fact of the matter about which is later in any sense that means anything -- "last" is an
// artifact of the order the merge happened to fold them. Picking one is fabricating a winner.
// artifact of the order the integration happened to fold them. Picking one is fabricating a winner.
//
// AUTHORING revises ONE author's OWN pending proposal, in the order THEY performed it. The second
// add is not a competing party; it is the same party saying "no, this". Here "later" is not a fold
// artifact -- it is the author's own sequence of intent, which is the only thing the operation has
// to go on.
//
// So the merge rule is not overridden, it does not reach: its premise is a contest between authors,
// and an author has no contest with themselves. The mechanical tell is that merge's rule is stated
// So the integration rule is not overridden, it does not reach: its premise is a contest between
// authors, and an author has no contest with themselves. The mechanical tell is that the
// integration's rule is stated
// over a LIST OF PROPOSALS whose order it explicitly refuses to privilege, while this is stated over
// ONE proposal being revised in place.
//
Expand All @@ -54,8 +55,9 @@ import gunbc.scm.merge {
// to correct a staged mistake would be to discard the proposal. A verb whose sole response to
// correction is "start over" has not modelled authoring; it has modelled a ledger.
//
// WHAT IS PRESERVED FROM merge's RULE: nothing is silently discarded ACROSS AUTHORS. This function
// produces one proposal per author, and when two authors' proposals meet, merge still sees exactly
// WHAT IS PRESERVED FROM THE INTEGRATION'S RULE: nothing is silently discarded ACROSS AUTHORS. This
// function produces one proposal per author, and when two authors' proposals meet, the integration
// still sees exactly
// two competing requirements and still refuses to pick between them. Replacing within a draft does
// not weaken that; it is upstream of it.
//
Expand Down
70 changes: 70 additions & 0 deletions dag/gunbc/scm/proposal.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
module gunbc.scm.proposal

import std.types { List }
import v2.std.node { Node, Symbol }
import v2.std.dependency { DependencyKind }

// THIS IS THE PROPOSAL AUTHORITY, AND IT IS DELIBERATELY NOT NAMED AFTER AN OPERATION.
//
// These nouns previously lived in `gunbc.scm.merge`, which made an OPERATION module the home of the
// vocabulary its callers needed. That was measurable rather than a matter of taste: of the eight
// modules importing that module, SIX consumed only these nouns and never the operation, and three of
// those six were production modules -- gunbc.scm.status, gunbc.scm.authoring and
// gunbc.scm.read_command. A vocabulary with three times the consumers of the operation it was filed
// under is not a detail of that operation.
//
// WHAT THIS MODULE MAY NOT BECOME. It is THE proposal authority, not one of two. A richer native
// proposal -- one carrying authored parent, target, occurrence, frame, authority, effects and
// evidence -- must WIDEN OR REPLACE these carriers in place. It must not arrive beside them as a
// second `NativeProposal` while this `Proposal` stays independently authoritative for the same
// transaction, because that is the section 3 fork this cut exists to remove, re-created one layer
// down.
//
// WHAT IT DELIBERATELY DOES NOT DEPEND ON: `ObjectStore` and `ObjectId`. A requirement is authored
// syntax; storage identity is not part of authoring it. Keeping that dependency out is what lets
// status, authoring and read-command consume this vocabulary without acquiring a storage fact none
// of them needs, and it fixes the direction of the graph -- proposal nouns, then integration, then
// the object store, never back the other way.

// A REQUIREMENT IS AUTHORED, AND ABSENCE IS ONE OF THE THINGS THAT CAN BE AUTHORED. A
// dependency-derived frontier can answer "is removing f compatible with everything that depends on
// f", but it cannot express "the author requested that f be absent" -- that is a stated requirement,
// not a consequence. Modelling delete as the absence of a positive requirement would make it
// indistinguishable from silence, and silence means PRESERVE THE TARGET, so a delete expressed by
// omission would be read as "leave f alone" -- the exact inversion of what was asked.
type Requirement
= RequireBinding { role: Symbol, value: Node }
| RequireBindingAbsent { role: Symbol }

fn requirement_role(r: Requirement) -> Symbol {
match r {
RequireBinding { role: role, value: _ } => role
RequireBindingAbsent { role: role } => role
}
}

type Proposal {
requirements: List<Requirement>
dependencies: List<RoleDependency>
}

// DEPENDENCIES ARE ROLE-GRAIN, NOT NODE-GRAIN, and that is a correctness choice rather than a
// convenience. `DependencyView` endpoints are Nodes, and a replacement mints a NEW immutable node --
// so a target-read edge `F1 -> K` says nothing about how `F2` relates to `K` once the binding is
// replaced. The binding ROLE is the bridge that survives the replacement, so the relation is carried
// at role grain and the question "does F2 still satisfy what K needed" stays answerable without
// giving nodes a temporal identity they must not have.
//
// AND IT IS NAMED FOR THE RELATION, NOT FOR EITHER OF ITS POPULATIONS. It was `MergeDependency`,
// which tied a neutral carrier to one operation. `ProposalDependency` was considered and REFUSED:
// the integration consumes this same type in TWO populations -- the target's own dependencies and
// the ones a proposal declares -- and combines them, so a proposal-flavoured name would make every
// target-side use a lie. What is genuinely operation-specific is which KINDS an integration
// supports, which kinds propagate a removal, and how an unsupported kind becomes a refusal. Those
// are classifier policy and they stay with the operation; none of them is a property of this row.
type RoleDependency {
dependent: Symbol
required: Symbol
kind: DependencyKind
usage_site: Symbol
}
2 changes: 1 addition & 1 deletion dag/gunbc/scm/read_command.dag
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ import gunbc.scm.repository_load {
}
import gunbc.scm.log { CommitLog, repository_log }
import gunbc.scm.status { RepositoryStatus, repository_status }
import gunbc.scm.merge { Proposal }
import gunbc.scm.proposal { Proposal }

// THE VERB IS A TYPE ARGUMENT, NOT AN ARM. Selecting a verb from argv is dispatch, and dispatch is
// realization (DESIGN section 3), so a `ScmReadCommand = Log | Status` coproduct here would pull
Expand Down
Loading
Loading