Skip to content

mathema docsync

The sync pass over the layered store. Authoring surfaces are transitory input; the declared layer is the materialized intermediary; the verified layer is the append-only memory; the index is the generated map. docsync is the verb that keeps them coherent.

mathema docsync [mypkg ...] [--root .] [--yes] [--write-docstrings] [--report] [--write]

The layer model

  • Authoring surfaces: docstrings (Intent:/Claims:/Notes:/ Concepts: blocks and inline #tag spellings), decorators, claims files, module docstrings, READMEs. All input, all transitory.
  • Declared layer (.mathema/declared/<key>.yaml): a materialized view, the canonical rendering of every surface merged, regenerated by this verb. It is output, never input: people and agents read it (the index points here for the complete claim set per function), the engine never does, and an edit made in it is overwritten at the next sync without ever taking effect. To change a claim, edit an authoring surface.
  • Verified layer (.mathema/verified/<key>.yaml): machine-written records, append-only in membership: a claim, once verified, never vanishes. Deleting it from every authoring surface just means the next sweep repopulates it from the record and keeps adjudicating (its exits are the discovery flow, mathema accept --as historical, or --as superseded, never silent removal). A quantified derive row carries its region as a rendered condition (∀ x ∈ [0.0, 5.0] ⊂ ℝ ∪ {∅}), the proof's own quantifier; a probe row carries none, since there it would only restate the statement and domain. Grammar output round-trips, so the rendered region is the canonical form and repopulation parses it back. Records carry the git commit at adjudication and an integrity checksum over each claim's statement, verdict and acceptance, and over the retirement rows; a hand-edit is reported as "altered outside mathema" (an acceptance write is mathema's own hand and restamps). Concepts are the one deliberate exception to append-only: recomputed fresh each run, since tags are removable context, not evidence.
  • Curation (.mathema/meta/): the small human-decision files, concepts.yaml (dismissed suggestions, per key) and intent.yaml (module- and project-scope intent acceptances).
  • Index (.mathema/index.yaml): generated, system intent (top README), module intents (module docstrings/READMEs), function intents, keys, a sed-ready span per function, verified-record paths, concepts, and each scope intent's acceptance rung.

The whole .mathema/ directory is part of the source tree: commit it, so the verified layer travels with the code it is evidence about.

What one run does

  1. Materializes every function's declared entry, docstring intent winning over a declared-file intent (the declared intent is the skeleton only when no docstring exists).
  2. Surfaces conflicts in the three-tier model. A claim name has one owner per state:
  3. Name in the verified layer, authored differently anywhere: the record wins; the verified version keeps adjudicating and reverse-syncs into the declared layer; adopting the change is the explicit mathema accept <key> <claim> --as superseded (accept). docsync prints the command, never resolves this itself.
  4. Name not yet verified, docstring and declared file disagree: a per-conflict prompt shows both versions and lets you keep either ([d/f/s]); the docstring's version is written into the declared file structured (domain field), never as display text, and its route tag transfers only when the docstring stated one explicitly. --yes takes the docstring everywhere. The declared file is rewritten from its parsed form, so YAML # comments in it do not survive; docsync warns before writing such a file. Keep a claim's annotation in its note: field instead, which persists through every rewrite (see authoring).
  5. Name unknown everywhere: added to declared, no ceremony. An unresolved conflict of either kind is a verify gate failure.
  6. Reports docstring drift: Claims:-block names unknown to declared∪verified, and verified claims not listed in the block.
  7. Regenerates the index.

Editing source is always explicit

The default run never touches a .py file. --write-docstrings appends verified-but-unlisted claim names (with canonical statements) to an EXISTING Claims: block; it never creates a block and never rewrites a human's prose; the claim NAMES are the keys, the statement text in a docstring is free for humans to rephrase (the docstring is not the record). --write offers a generated docstring for functions that have none, prompted per function. --report prints the per-function sync checklist.

The score

The audit docsync column (in the grid by default, --exclude docsync to skip) measures the docstring against the OTHER layers, not just itself: Intent/Claims/symbol coverage, intent conciseness, intent-in-sync with the declared layer, Claims-block-in-sync (names known, zero conflicts), raises coverage (claim-first), domain declared/enforced, typing, callee documentation (direct callees only, a central undocumented callee already compounds through each caller's own row, so depth adds noise, not signal). The claim triplet {floor | actual | expected} reads declared∪verified and stays informational; a stale verified record (form changed since it was written) is flagged, never silently used.

Intent and acceptance

An intent's docstring SHAPE is labelled explicit (the paragraph following an Intent: marker) or implicit (the first paragraph stands in); the same rule reads module docstrings and README sections. Shape is not rung: both start at declared, and documented is a human act:

mathema accept mypkg.mod.fn --intent --by "lovelace"

The acceptance binds to the signature, the raised-exception surface, and the intent text; a body-only refactor keeps it; changing any of the three marks it stale and drops the rung until re-accepted. The same verb accepts scope intents (mathema accept mypkg.mod --intent, mathema accept __project__ --intent), bound to the text alone and stored in .mathema/meta/intent.yaml; the index annotates each scope with documented or stale. Concepts ride the same verb: --concepts a,b earns tags the documented rung, --dismiss-concepts c records a dismissal in .mathema/meta/concepts.yaml so the suggestion never returns.