Repository navigation
Conversation
Design rationale for DialCache changes has lived in GitHub issue bodies that are rewritten in place, in a design folder on one laptop, and in Claude memory. Codex agents, which open about half of recent pull requests, can see none of the last two, and the edit history of a rewritten issue is not searchable. Recent examples: #132 shipped the compression design that #60 had closed as not planned without linking it; #117's body was rewritten six times; #219 exported CacheUseCaseOptions against #218's design while #218's decision checklist stayed unticked. Add design/ with a README and a template. A record is required before a new or changed portable contract, a new conformance profile, a redesign of the conformance machinery, a cross-port or reshaping public API change, or a reversal of an earlier decision. Decisions stay Open until a maintainer confirms them, the implementing pull request stays in draft until then, a changed decision keeps its earlier choice under Rejected, and departures from the record go to its Deviations section in the same pull request. Records explain decisions; Quint and the formal guides remain the definition of behavior. AGENTS.md gains a structure entry and one convention bullet, since it is the only instruction every agent reads. design/README.md joins the relative-link check because it links into formal/guides/; records themselves are unchecked. No source-audit or go-parity pin changes: neither ledger covers AGENTS.md, design/ or scripts/.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #225 +/- ##
=======================================
Coverage 93.73% 93.73%
=======================================
Files 78 78
Lines 11357 11357
Branches 656 656
=======================================
Hits 10645 10645
Misses 642 642
Partials 70 70
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Process rules were scattered across AGENTS.md convention bullets, AUTHORING.md, VALIDATION.md, docs/authoring.md and docs/maintainers.md, and recent PRs show the cost: #190, #197, #198 and #213 merged without a full run on their head; Python was left out of guides and checks after #200; #219 exported a type its design kept private; an agent merged PRs and agent reviews read like approvals. Rewrite AGENTS.md around one section, "Make a change": classify the change by type (each type sets the record, the steps and the validation required before a PR leaves draft), stop at five maintainer gates, follow the type's path, refresh pinned ledgers, validate the head commit, open the PR as a draft from the template, and finish against a checklist. Agents never submit approving reviews, and agent-posted GitHub text begins with "Agent:". Critical behavior and the conventions stay; the directory tree goes, and the stale claims it carried are corrected. Supporting changes: - CLAUDE.md imports AGENTS.md for Claude Code builds that do not read AGENTS.md natively. - .github/pull_request_template.md is the description shape AGENTS.md tells agents to fill, with Open questions, a port table and per-run commits. - formal/catalogs/README.md gains "Refresh after an edit": what each ledger pins and the order to refresh them. - design/README.md and TEMPLATE.md align with the gates: implementation waits for an Accepted record, searches include pull requests, unmerged pre-record PRs get records, and confirmations link or quote the approval. - AGENTS.md joins the relative-link check. None of these files is pinned by a ledger; make audit passes unchanged.
lan17
changed the title
lan17
marked this pull request as draft
October 13, 2026 23:45
lan17
commented
Oct 14, 2026
AGENTS.md is written for agents: exact steps, gates and commands. Add DEVELOPMENT_PROCESS.md for people who want to understand the workflow itself: how behavior is defined once in contracts and Quint and replayed by every port, the life of a change, the three validation levels and why ledgers exist, the change types, the design-record lifecycle, what only the maintainer decides, a portable feature end to end, and releasing. Four Mermaid diagrams render on GitHub; each was checked under Mermaid 11. The guide links to AGENTS.md as the authoritative rule set instead of restating commands, and AGENTS.md now says a change to "Make a change" updates the guide in the same PR. The file is named for its purpose rather than CONTRIBUTING.md, which GitHub shows to outside contributors and would imply a policy for them. It joins the relative-link check.
The full formal run takes about two and a half hours, and 136 of those minutes are the model-fault campaign, which reads only the Quint models, the challenge catalog and the Quint toolchain. Port changes cannot alter its result, yet the process asked for the whole run on every behavior change, so it was skipped (#190, #198 merged with no run) or re-run on intermediate pushes (63 green runs on superseded commits since September). Give formal-full.yaml a mode input. replay generates the corpus and completes every port replay, about 15 minutes. mutations adds the three port mutation campaigns, about 50 minutes. full, the default and the weekly schedule, adds check-models with the campaign. Lanes a mode does not select are skipped, and the aggregate requires them to be skipped, so a dispatch cannot pass as a stronger mode than it ran. The run name carries the mode. The generate job restores .formal-traces from a cache keyed on every input generation reads: the models, formal/replay, formal/tools, formal/generated, the catalogs other than the three review ledgers, the committed witness fixtures, the Quint pin, the Makefile and the lockfile. Generation is deterministic in content, so an exact key stands for a regenerated corpus; no partial key may restore. A branch that adds Quint regressions misses the cache and regenerates, so its histories enter the corpus that every port must pass. AGENTS.md, DEVELOPMENT_PROCESS.md, VALIDATION.md and maintainers.md state the tiers and when each applies: Replay for port, driver and regression-only changes; Mutations when a catalogued mutant's file is edited; Full when a transition, invariant, the kernel library or the Quint toolchain changes. A green run on an earlier commit still covers a head whose difference is prose, design records or ledger pins. The workflow-shape test pins the mode options, the lane conditions, the cache key inputs and each mode's gate; a flipped gate expectation fails it. The two pinned guides' ledger entries are refreshed.
Review of the mode change found these gaps. The concurrency group was keyed on the ref alone, so a replay dispatched while a full run was in progress on the same branch waited for it, up to two and a half hours. The group now includes the mode; same-mode dispatches still queue. The weekly scheduled run regenerates even on a cache hit, so a freshly installed toolchain re-exports the committed fixtures and vectors once a week; the save stays skipped when the entry already exists. A new challenge is measured only by the model-fault campaign, so the Bug fix row sends a changed challenge to Full. A layout move keeps Full with exploration, because exploration snapshots the source tree. The mutant rule reads the same in every document: a file a catalogued mutant rewrites, or a mutant catalog. The carry-over rule names Markdown files and ledger pins instead of "prose". maintainers.md, VALIDATION.md and AUTHORING.md no longer require full validation for every behavior change. The workflow-shape test pins the cache key and the restore step id exactly, and the gate line for line, so an added exclusion, a non-hashFiles key component or a loosened arm fails it.
# Conflicts: # formal/catalogs/go-parity.json # formal/catalogs/source-audit.json
# Conflicts: # formal/catalogs/source-audit.json
#236 added formal/tools/where.mjs, which prints where one contract is stated, tested, challenged and mapped. That is the navigation the Bug fix path and the formal convention in AGENTS.md asked agents to assemble by hand, so both name the command, and DEVELOPMENT_PROCESS.md lists it under Where to look.
lan17
marked this pull request as ready for review
October 15, 2026 08:10
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
Agents open most DialCache pull requests, and the process they follow is spread across
AGENTS.mdconvention bullets,AUTHORING.md,VALIDATION.md,docs/authoring.mdanddocs/maintainers.md. Design reasoning lives in rewritten issue bodies, a folder on one laptop and Claude memory. Recent cost:CacheUseCaseOptionsagainst Add exact-key delete for one cached result (child of #217) #218's design, and Add exact-key delete for one cached result (child of #217) #218's decisions were never ticked.This grew out of an evaluation of OpenSpec. Its
specs/tree would restate what Quint andCONTRACTS.mdalready define, so this adopts only a change-record convention plus an explicit process, with no CLI.The review comment on the first draft asked whether every behavior change needs the 2.5 h full run. It does not: 136 of those minutes are the model-fault campaign, which reads only the Quint models, the challenge catalog and the Quint toolchain, so port changes cannot alter its result. The last month had 115 full runs, 63 of them green on commits later superseded, while #190 and #198 broke
mainwith no run at all.Change
Type: Docs, plus Tooling (the formal workflow and the docs link checker). No design record is needed.
AGENTS.mdis organized around "Make a change":Critical behavior and the conventions stay. The directory tree goes, and the stale claims it carried are corrected.
design/README.mdanddesign/TEMPLATE.mdset out when a change needs a design record, how to find earlier decisions (searches include PRs), and the lifecycle:Openuntil the maintainer confirms them.Accepted..github/pull_request_template.mdis the description shapeAGENTS.mdtells agents to fill with--body-file. GitHub never applies templates togh pr create --body.formal/catalogs/README.mdgains "Refresh after an edit": what each ledger pins and the order to refresh them, using the--refreshand--refresh-inputscommands feat(formal): add in-repo ledger refresh commands #228 added. The branch is merged withmainthrough feat(formal): add where.mjs, the contract lookup command #236; each merge's ledger conflict was resolved by takingmain's copy and re-keying the three edited guides, three hash lines each time.AGENTS.mdandDEVELOPMENT_PROCESS.mdpoint at feat(formal): add where.mjs, the contract lookup command #236'snode formal/tools/where.mjs <ID>, which prints where a contract is stated, tested, challenged and mapped: the step the Bug fix path had agents assembling by hand.DEVELOPMENT_PROCESS.mdexplains the workflow to human readers, with four Mermaid diagrams: how behavior is defined, the life of a change, the design-record lifecycle, and a portable feature from start to finish. It also covers the change types, validation levels, ledgers, what only the maintainer decides, and releasing. It links toAGENTS.mdfor exact steps, andAGENTS.mdrequires both to change together. It is not namedCONTRIBUTING.mdbecause GitHub shows that file to outside contributors, which would imply a policy for them.CLAUDE.mdimportsAGENTS.mdfor Claude Code builds older than v2.1.277, which read onlyCLAUDE.md.scripts/check-docs.mjslink-checksAGENTS.md,DEVELOPMENT_PROCESS.mdanddesign/README.md.formal-full.yamlgets amodeinput, and each mode adds to the one before:replay: generate the corpus and replay it in all four ports. About 8 minutes when the corpus is cached, 17 on a miss.mutations: plus the TypeScript, Go and Rust mutation campaigns. About 50 minutes.full: plus the model checks and the model-fault campaign. About 2.5 hours. The default, and the weekly schedule.Lanes a mode does not select are skipped, and the aggregate requires them to be skipped, so a dispatch cannot pass as a stronger mode than it ran. The concurrency group is keyed by ref and mode, so a replay never queues behind a full run.
The corpus is cached by an exact hash of every generation input: the models,
formal/replay/,formal/tools/,formal/generated/, the catalogs other than the three review ledgers, the committed witness fixtures, the Quint pin, theMakefileand the package manifests. Generation is deterministic in content, so a hit equals a regenerated corpus; no partial key may restore. A branch that adds Quint regressions misses the cache and regenerates, so its histories enter the corpus every port must pass. The weekly run regenerates even on a hit. Committing the corpus was rejected: it is 35 MiB and changes on every model edit, and the 17 smoke histories are already the committed subset.The tiers in the documents: Replay for port, driver and regression-only changes; Mutations when a file a catalogued mutant rewrites, or a mutant catalog, is edited; Full for Quint transitions, invariants or challenges, the kernel library or the Quint toolchain; Full with exploration for a layout move. Exploration is otherwise weekly only. A green run on an earlier commit covers a head whose difference is Markdown files or ledger pins, with PR CI green on the head.
VALIDATION.md,AUTHORING.mdandmaintainers.mdsay the same, with their ledger pins refreshed.Open questions
Agent:prefix. Agent-posted issues, comments and reviews begin withAgent:, so approval means "your words, without the prefix". Recommended: keep.Accepted; an agent whose design needs a decision stops after pushing the record. The alternative is implementing in draft at the risk of rework. Recommended: keep the strict gate.Opendecisions stop at the design gate. The alternative is to exempt them. Recommended: records.Every bug fix requires a full run.Resolved by the tiers: a bug fix needs Replay (about 8 minutes), Mutations if it edits a mutant's file, Full only if it changes a Quint transition, invariant or challenge.AGENTS.mdis 290 lines and 19 KB, about 5k tokens per session. That is under Codex's 32 KiB budget and Claude's large-file warning, but over the 200-line guideline. The alternative is moving the per-type paths to a separate file, which the design panel scored lower because agents may never open it. Recommended: keep it in one file.Validation
Head:
788142a(merges ofmainat 71d44d4 and 5030320, plus thewhere.mjspointers)node --test scripts/check-docs.test.mjsat6490055: 5/5 pass.node scripts/check-docs.mjsat6490055: 30 pages link-checked; every anchorAGENTS.md,DEVELOPMENT_PROCESS.mdanddesign/README.mdlink to resolves.corepack pnpm --dir typescript exec vitest run test/formal-validation.test.tsat6490055: 34/34 pass. The new test pins the mode options, the lane conditions, the exact cache key and restore step id, and the gate line for line; flipping one gate expectation fails it (checked).make auditat6490055: passes with the refreshedsource-audit.jsonandgo-parity.jsonpins forVALIDATION.md,AUTHORING.mdandmaintainers.md; after the merge the same three files are re-keyed withcheck-source-audit.mjs --refresh, andgo-parity.jsonis unchanged because it now binds dispositions.replay) at296eede: green in 17 min 14 s; cache miss, corpus generated and saved;check-modelsand every mutation lane skipped.replay) at296eede: green in 8 min 16 s from start; cache hit, generate 71 s.replay) at6490055: green in 6 min 11 s; cache hit, generate 36 s; the per-mode concurrency group and the schedule condition parse and run.replay) at8667553: green in 15 min from start; cache miss, becausemain's kernel header rewrite and tool changes are in the key; the new corpus was saved. It queued behind an earlier replay in the same per-mode group, as designed.replay) at788142a: green in 19 min; cache miss, becausemain's tool and catalog changes are in the key; the new corpus was saved.make audit(now including feat(formal): measure Quint style and enforce two caps #234's Quint style caps),node scripts/check-docs.mjs(35 pages) and theformal-validation,formal-source-audit,formal-go-parityandformal-styletest files at788142a: 79/79 pass.make audit,node scripts/check-docs.mjsand theformal-validation,formal-source-auditandformal-go-paritytest files at8667553: pass. Two prerequisite-probe tests timed out once at the 5-second default under a load average of 31 from another session and pass with a longer budget; they are unchanged by this PR.AGENTS.mdshapes judged against a rule inventory and a study of agent failures in test(formal): parse the witness corpus once in the completion gates #176–docs: define the agent change process and in-repo design records #225; six simulated agents walked the result through real tasks; a fact-checker verified every claim against the repo and the ruleset; three reviewers checkedDEVELOPMENT_PROCESS.md; four reviewers checked the mode and cache change (Actions semantics, cache-key completeness against everything generation reads, policy coherence, test adequacy). Their fixes are in this head.Not run:
mutationsandfullmodes on this branch. This PR changes no port source, model or mutant input, soreplayis its tier; thefullpath is unchanged apart from the per-mode concurrency group and the schedule condition, both exercised by the replay run's parse of the same file.Follow-ups
formal/README.mdcan point atdesign/in a PR that refreshes its ledger pin.check-models' 150-minute budget (feat: add exact-key deletion across all ports #219 hit it). Sharding it or persisting its per-closure cache across runs would let a regression-only change re-measure one profile's cells in minutes.BEHAVIOR.md,GO-PARITY.md,SEMANTIC-COVERAGE.mdandPORTING.mdstill say behavior changes need full validation. That is stricter than the new policy, so it is harmless until their next ledger refresh.