Skip to content

contributing.adoc

Latest commit

 

History

History
60 lines (48 loc) · 2.41 KB

contributing.adoc

File metadata and controls

60 lines (48 loc) · 2.41 KB
Raw

Contributing to Mathesis

This guide is for a person or an agent who changes Mathesis. To read the atlas, see usage. Read CLAUDE.md and the deed mathesis_chora.deed first: they state the identity, the boundaries and the golden path.

Tools

  • just 1.56.0 and the other tools that mise.lock pins, each with its checksum.

  • Bun, for the atlas and the registry.

  • Nickel 1.18.0, for just validate-claude-md and just validate-coapt.

  • Agda, Rocq and Lean for the proof checks. CI takes them from the Guix revision that build/channels.scm pins (build/manifest.scm).

The golden path

export MATHESIS_STANDARDS=/path/to/standards
just check-views
guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- just check-proofs

just check runs both halves; CI runs it in the pinned Guix shell. A stale view or a failing proof fails it.

Rules of this repository

  • One writer for census data. Only just census and just update-rows write rows and the not-reached list; record open census work in docs/status/ROADMAP.adoc first (see docs/atlas/README.adoc).

  • A public frame. docs/atlas/census/repos.jsonl holds public repositories only. Never write the name of a private repository anywhere.

  • No grade by hand. Claim pins carry no grade; the registry derives each grade from a receipt.

  • The deed has one writer. Change mathesis_chora.deed only with scripts/deed-clause.sh, then run just claude-md and just coapt.

  • Contractiles are sensitive. The owner reviews each clause before it lands.

  • Signed commits. Every commit is signed.

  • Generated files. Regenerate CLAUDE.md, the coaptation receipt, the views and docs/architecture/REPOSITORY-MAP.adoc with their tools; never edit them by hand.

Decisions

Record a non-obvious design decision as an ADR in docs/decisions/, from 0001-template.adoc. Decisions that are the owner’s go to the owner first.

Reporting issues