From 4a7f38626880db2d6bc557f1f49a3b3773f796f1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:25:49 +0000 Subject: [PATCH 1/5] Fill the PROOF-STATUS title placeholder and say what verification/proofs/ contains MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/status/PROOF-STATUS.adoc opened with '= Proof Status — {{PROJECT}}', an unfilled mint placeholder, where haec and hermeneia read HAEC and HERMENEIA. The repository does gate placeholders, but openssf-compliance.yml checks a fixed list of required files (SECURITY, LICENSE, CONTRIBUTING, README, CHANGELOG and three .machine_readable/6a2 files) that does not include the status surfaces, which is why this passed CI. Title now reads VOCARIUM. Added a note saying what verification/proofs/ actually contains, since the summary reads 0% proven beside nine prover files. Every one is an unmodified mint template: the Coq is a toy expression language, the Agda proves length (xs ++ ys) ≡ length xs + length ys, the Lean the functor laws for a template ApiResult, the TLA+ a placeholder request pipeline. None states anything about vocarium, so 0% is the accurate count rather than a backlog. Two consequences recorded rather than left implicit: - build/just/proofs.just's proof-check-* recipes print "SKIP: not installed" and continue, against this repository's own no-silent-skip constraint; and if a toolchain were present they would report green on template boilerplate. They are not reachable from the golden path (just test && just quality), so no gate is affected today. trope-checker's build/just/proofs.just carries the estate's reference treatment: it refuses to report a skip as a pass. - no escape hatch is present in any body, verified with mathesis scripts/census/proof-holes.sh over this tree on 2026-11-09. That scan does return one real policy finding: verification/proofs/agda/Properties.agda carries no OPTIONS pragma at all, so it does not set --safe, let alone the PROOF-POLICY §2.1 invocation. Under PROOF-POLICY §8.1 none of this supports a Proof Witness Grade. Removing the templates as trope-checker did under ADR 0005 D5 is an owner decision, so nothing is deleted here. Documentation only. Verified here: asciidoctor 2.0.26 --failure-level=WARN clean on both changed files; no {{PLACEHOLDER}} token remains in the file. NOT RUN here: Agda, Coq, Lean, Idris2, TLA+ (no toolchain). Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- CHANGELOG.adoc | 17 +++++++++++++++ docs/status/PROOF-STATUS.adoc | 40 ++++++++++++++++++++++++++++++++++- 2 files changed, 56 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index ca1c652..ed8e001 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -7,3 +7,20 @@ Changelog], and this project adheres to https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] + +==== Fixed + +* *`+docs/status/PROOF-STATUS.adoc+` title was an unfilled mint placeholder +(2026-11-09).* It read `+= Proof Status — {{PROJECT}}+`; it now reads +`+VOCARIUM+`, matching haec and hermeneia. The repository's placeholder gate +(`+.github/workflows/openssf-compliance.yml+`) checks a fixed list of required +files that does not include the status surfaces, which is why this passed CI. + +==== Added + +* *A note saying what `+verification/proofs/+` actually contains (2026-11-09).* +Every file there is an unmodified mint template that states nothing about +vocarium, so the 0%-proven summary is accurate rather than a backlog. The note +also records that `+build/just/proofs.just+`'s `+proof-check-*+` recipes report +`+SKIP+` and continue, against this repository's `+no-silent-skip+` constraint, +and that they are not reachable from the golden path. diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index aca702c..d63e127 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -2,7 +2,7 @@ // Copyright (c) Jonathan D.A. Jewell // Template: rsr-template-repo/docs/status/PROOF-STATUS.adoc // Tracks proof completion. Requirements defined in PROOF-NEEDS.adoc -= Proof Status — {{PROJECT}} += Proof Status — VOCARIUM == Summary @@ -68,6 +68,44 @@ | TP-2 | Public API type safety | TP | Lean4 | P2 | 4h |=== +== What `verification/proofs/` currently contains + +NOTE: as of 2026-11-09 every file under `verification/proofs/` is an *unmodified +mint template*. Each still carries its "Replace with your project's …" header, and +none of them states anything about vocarium: `coq/TypeSafety.v` is a toy expression +language, `agda/Properties.agda` proves `length (xs ++ ys) ≡ length xs + length ys`, +`lean4/ApiTypes.lean` proves the functor laws for a template `ApiResult`, and +`tlaplus/StateMachine.tla` models a placeholder request pipeline. They are +therefore *not* evidence for anything, which is why the summary above correctly +reads 0% proven — the figure is not a backlog against those files, it is the +accurate count. + +Two consequences worth stating rather than leaving implicit: + +* The `proof-check-*` recipes in `build/just/proofs.just` print + `SKIP: not installed` and continue. That contradicts this repository's + own `no-silent-skip` constraint, and if a toolchain *were* present they would + report green on template boilerplate. The recipes are not reachable from the + golden path (`just test && just quality`), so no gate is currently affected. + `hyperpolymath/trope-checker`'s `build/just/proofs.just` carries the estate's + reference treatment: it refuses to report a skip as a pass. +* `hyperpolymath/trope-checker` removed the identical never-instantiated templates + under ADR 0005 D5. Whether vocarium does the same is an owner decision (doctrine + 7: cold is not disposable), so nothing is deleted here. + +No escape hatch is present: no `believe_me`, `assert_total`, `postulate`, `sorry`, +`Axiom` or `Admitted` occurs in any body — verified by `hyperpolymath/mathesis`, +`scripts/census/proof-holes.sh`, run over this tree on 2026-11-09. That scan does +return one real policy finding: `verification/proofs/agda/Properties.agda` carries +no `OPTIONS` pragma at all, so it does not set `--safe`, let alone the +PROOF-POLICY §2.1 invocation `--safe --without-K --cubical-compatible`. As the file +is mint boilerplate rather than a theory entrypoint of this repository, the +defensible fix is removal rather than adding flags to a template. + +Under PROOF-POLICY §8.1 these files support no Proof Witness Grade: they are not +theory obligations of this repository at all. Vocarium's real proof obligations +are the store invariants named in `PROOF-NEEDS.adoc`. + == Verification Commands [source,bash] From f819ccfb0b599d5783d4a497e2d83bd734c61856 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:44:29 +0000 Subject: [PATCH 2/5] Replace the forbidden "0% proven" line with a census MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/status/PROOF-STATUS.adoc published: *Overall*: 0% proven PROOF-POLICY §8.4 rule 7 forbids exactly that form: "Never publish 'X% proved', an average grade, or a single confidence score." It asks for a census instead — a count per category with the denominator. The figure was accurate; the shape was the prohibited one, and a percentage invites being averaged or trended, which is what the rule exists to prevent. It now reads as a census (0 done, 0 in progress, 0 blocked, 7 remaining, of 7 recorded obligations), with a note recording what changed and why, and the fact that no obligation here carries a Proof Witness Grade because none is a theory obligation of this repository under §8.1. The same line ships in rsr-template-repo's PROOF-STATUS.adoc, so every repository minted from it carries the same breach. The note says so: fixing it there is the solution at source, and this change is the downstream symptom being treated only because the surface is published today. Documentation only. Verified here: asciidoctor 2.0.26 --failure-level=WARN clean on both changed files; no percentage-of-proved claim remains in the file. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- CHANGELOG.adoc | 7 +++++++ docs/status/PROOF-STATUS.adoc | 17 +++++++++++++---- 2 files changed, 20 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index ed8e001..ffbd949 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -10,6 +10,13 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. ==== Fixed +* *`+docs/status/PROOF-STATUS.adoc+` published a percentage, which PROOF-POLICY +forbids (2026-11-09).* The summary read `+*Overall*: 0% proven+`. §8.4 rule 7 is +explicit — "Never publish 'X% proved', an average grade, or a single confidence +score" — and asks for a count per category with the denominator instead. The +figure was accurate; the form was the forbidden one. It now reads as a census. +The same line ships in `+rsr-template-repo+`'s `+PROOF-STATUS.adoc+`, so fixing +it there is the solution at source. * *`+docs/status/PROOF-STATUS.adoc+` title was an unfilled mint placeholder (2026-11-09).* It read `+= Proof Status — {{PROJECT}}+`; it now reads `+VOCARIUM+`, matching haec and hermeneia. The repository's placeholder gate diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index d63e127..667b237 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -20,7 +20,16 @@ | *Total* | *7* | *0* | *0* | *0* | *7* |=== -*Overall*: 0% proven +*Census.* Of 7 recorded obligations: 0 done, 0 in progress, 0 blocked, 7 +remaining. No obligation here carries a Proof Witness Grade, because none is a +theory obligation of this repository under PROOF-POLICY §8.1. + +NOTE: this line used to read "*Overall*: 0% proven". PROOF-POLICY §8.4 rule 7 is +explicit — "Never publish 'X% proved', an average grade, or a single confidence +score" — and requires a count per category with the denominator instead. The +figure was accurate; the *form* was the one the policy forbids. The same line +ships in `rsr-template-repo`'s `PROOF-STATUS.adoc`, so every repository minted +from it carries it; fixing it there is the solution at source. == Proofs Done @@ -76,9 +85,9 @@ none of them states anything about vocarium: `coq/TypeSafety.v` is a toy express language, `agda/Properties.agda` proves `length (xs ++ ys) ≡ length xs + length ys`, `lean4/ApiTypes.lean` proves the functor laws for a template `ApiResult`, and `tlaplus/StateMachine.tla` models a placeholder request pipeline. They are -therefore *not* evidence for anything, which is why the summary above correctly -reads 0% proven — the figure is not a backlog against those files, it is the -accurate count. +therefore *not* evidence for anything, which is why the census above correctly +reads 0 done of 7 — that count is not a backlog against those files, it is +accurate. Two consequences worth stating rather than leaving implicit: From b8660dc3f27a491b838f2f181db629fe2e3df3bf Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:33:36 +0000 Subject: [PATCH 3/5] Fix the openssf failure I caused, and two claims the review found wrong MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit openssf-compliance went red on this branch, and it was mine: ##[error]CHANGELOG.adoc contains 1 unfilled {{PLACEHOLDER}} tokens 21:(2026-11-09).* It read `+= Proof Status — +`; it now reads The changelog entry describing the placeholder fix quoted the placeholder literally, and CHANGELOG.adoc is on that gate's required-files list — the very list this PR's own note says the status surfaces are missing from. So the entry reintroduced the defect it documents. It now describes the token without reproducing it. Reproduced the gate's loop locally over vocarium's required files: FAIL before, PASS after. Two claims the review was right to challenge, both checked here: - The note said vocarium's real obligations "are the store invariants named in PROOF-NEEDS.adoc". They are not named there: that file's project-specific table is empty, and the seven rows the summary counts are the mint's ABI/FFI and typing categories — which sit oddly beside ADR-0002's pure-Zig wire boundary, since it specifies no C-ABI structs and no bindings. The note now says the obligations this store owes (append-only JSONL replay, index reconstruction on open, use-model relativity, warrant checking) are described in README.adoc and the ADR and are not yet written down as proof obligations. - The note treated all proof-check-* recipes alike. The aggregate proof-check-all does fail, but for an unintended reason: it also runs proof-scan-dangerous, which greps raw source with no comment awareness, so its pattern matches the words postulate, Admitted, believe_me and assert_total in the templates' own header comments. Verified here by running that recipe's logic directly: it matches eight files, every hit a comment. So the one recipe that fails does so on comment text, not because it checked anything. The note now says that. Documentation only. Verified here: the openssf placeholder loop passes over the required files; asciidoctor 2.0.26 --failure-level=WARN clean on both changed files. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- CHANGELOG.adoc | 2 +- docs/status/PROOF-STATUS.adoc | 20 +++++++++++++++----- 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index ffbd949..e403634 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -18,7 +18,7 @@ figure was accurate; the form was the forbidden one. It now reads as a census. The same line ships in `+rsr-template-repo+`'s `+PROOF-STATUS.adoc+`, so fixing it there is the solution at source. * *`+docs/status/PROOF-STATUS.adoc+` title was an unfilled mint placeholder -(2026-11-09).* It read `+= Proof Status — {{PROJECT}}+`; it now reads +(2026-11-09).* Its title carried the mint's unfilled project-name token; it now reads `+VOCARIUM+`, matching haec and hermeneia. The repository's placeholder gate (`+.github/workflows/openssf-compliance.yml+`) checks a fixed list of required files that does not include the status surfaces, which is why this passed CI. diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 667b237..2f6fcba 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -91,10 +91,14 @@ accurate. Two consequences worth stating rather than leaving implicit: -* The `proof-check-*` recipes in `build/just/proofs.just` print +* The individual `proof-check-*` recipes in `build/just/proofs.just` print `SKIP: not installed` and continue. That contradicts this repository's - own `no-silent-skip` constraint, and if a toolchain *were* present they would - report green on template boilerplate. The recipes are not reachable from the + own `no-silent-skip` constraint, and with a toolchain present each would report + green on template boilerplate. The aggregate `proof-check-all` is the exception + and fails for an unintended reason: it also runs `proof-scan-dangerous`, whose + pattern matches the words `postulate` and `Admitted` *in the templates' own + comments*. So the one recipe that does fail does so because of comment text, + not because it checked anything. The recipes are not reachable from the golden path (`just test && just quality`), so no gate is currently affected. `hyperpolymath/trope-checker`'s `build/just/proofs.just` carries the estate's reference treatment: it refuses to report a skip as a pass. @@ -112,8 +116,14 @@ is mint boilerplate rather than a theory entrypoint of this repository, the defensible fix is removal rather than adding flags to a template. Under PROOF-POLICY §8.1 these files support no Proof Witness Grade: they are not -theory obligations of this repository at all. Vocarium's real proof obligations -are the store invariants named in `PROOF-NEEDS.adoc`. +theory obligations of this repository at all. Nor does `PROOF-NEEDS.adoc` yet +list vocarium's own obligations — its project-specific table is empty, and the +seven rows the summary counts are the mint's ABI/FFI and typing categories, which +sit oddly beside ADR-0002's pure-Zig wire boundary (no C-ABI structs, no +bindings). The obligations this store actually owes — append-only JSONL replay, +index reconstruction on open, use-model relativity, warrant checking — are +described in `README.adoc` and the ADR, and are not yet written down as proof +obligations anywhere. == Verification Commands From 89fbe19406cb0ef4e249ce39b41877e17b1c3fb6 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:07:44 +0000 Subject: [PATCH 4/5] Say what proof-check-idris2 would actually do MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review was right and the document was wrong. PROOF-STATUS.adoc claimed that with a toolchain present every individual proof-check-* recipe would report green on template boilerplate, and that only the aggregate fails — "because of comment text, not because it checked anything". True for Agda, Coq and Lean. False for Idris2. The recipe runs `idris2 --check` from the repository root with no `--source-dir`, and there is no `.ipkg` anywhere in this repository, so for every file under verification/proofs/idris2/ the declared module name — `Types`, `ABI.Compliance`, and the rest — cannot match the name Idris2 derives from the path. Idris2 rejects the module header before elaborating anything, so nothing is type-checked. And because `proof-check-all` runs its dependencies in order, with Idris2 installed it stops at `proof-check-idris2`, its first dependency, and never reaches `proof-scan-dangerous` at all. All six files are affected, not only Types.idr. So the aggregate fails for one of two reasons depending on the environment, and the document now names both: with Idris2 present it dies on the module header; with no prover present every recipe skips and the failure comes from the dangerous-pattern scan matching `postulate` and `Admitted` in the templates' own comments. Either way the failure says nothing about whether a proof was checked, which was the point the entry was making — it was just attributing it to the wrong mechanism. Marked NOT RUN in the document itself: Idris2 is not installed in this session, so the Idris2 path is read from the recipe and from Idris2's own header check in src/Idris/ProcessIdr.idr, not executed. Agda, which IS installed here, is not affected the same way, because it adds the file's own directory to the include path where Idris2 keys off the source dir. Unchanged and re-confirmed: proof-check-all is genuinely unreachable from the golden path — Justfile:206 is `quality: fmt-check lint test`, Justfile:202 is `test-all: test e2e aspect bench readiness`, and proof-check-all appears in neither; it is reachable only through the `import?` at Justfile:581. Placeholder gate re-checked, since a literal mint token in CHANGELOG.adoc is what broke this repository's openssf lane earlier in this session: zero `{{` occurrences in either changed file. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- CHANGELOG.adoc | 19 +++++++++++++++++++ docs/status/PROOF-STATUS.adoc | 27 +++++++++++++++++++++------ 2 files changed, 40 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index e403634..25382fd 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -10,6 +10,25 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. ==== Fixed +* *The `+proof-check-idris2+` account was wrong (2026-11-09).* Review found it, + and it was right. `+docs/status/PROOF-STATUS.adoc+` said that with a toolchain + present every individual `+proof-check-*+` recipe would report green on + template boilerplate, and that only the aggregate fails, "because of comment + text, not because it checked anything". That holds for Agda, Coq and Lean but + is false for Idris2: the recipe runs `+idris2 --check+` from the repository + root with no `+--source-dir+` and there is no `+.ipkg+` in the tree, so every + file under `+verification/proofs/idris2/+` declares a module name + (`+Types+`, `+ABI.Compliance+`, …) that cannot match the name Idris2 derives + from its path. Idris2 rejects the header before elaborating anything, and + because `+proof-check-all+` runs its dependencies in order it would stop there + and never reach `+proof-scan-dangerous+`. The entry now states both failure + paths and which one applies when. NOT RUN: Idris2 is unavailable in this + session, so the Idris2 path is read from the recipe and from Idris2's own + header check in `+src/Idris/ProcessIdr.idr+`, not executed — and that is said + in the document rather than left implied. + +==== Fixed + * *`+docs/status/PROOF-STATUS.adoc+` published a percentage, which PROOF-POLICY forbids (2026-11-09).* The summary read `+*Overall*: 0% proven+`. §8.4 rule 7 is explicit — "Never publish 'X% proved', an average grade, or a single confidence diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 2f6fcba..7e5f26e 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -93,12 +93,27 @@ Two consequences worth stating rather than leaving implicit: * The individual `proof-check-*` recipes in `build/just/proofs.just` print `SKIP: not installed` and continue. That contradicts this repository's - own `no-silent-skip` constraint, and with a toolchain present each would report - green on template boilerplate. The aggregate `proof-check-all` is the exception - and fails for an unintended reason: it also runs `proof-scan-dangerous`, whose - pattern matches the words `postulate` and `Admitted` *in the templates' own - comments*. So the one recipe that does fail does so because of comment text, - not because it checked anything. The recipes are not reachable from the + own `no-silent-skip` constraint, and with an Agda, Coq or Lean toolchain + present each would report green on template boilerplate. + `proof-check-idris2` is the exception among the individual recipes: it runs + `idris2 --check` from the repository root with no `--source-dir`, and there is + no `.ipkg` anywhere in this repository, so for every file under + `verification/proofs/idris2/` the declared module name (`Types`, + `ABI.Compliance`, …) cannot match the name Idris2 derives from the path. + Idris2 rejects the header before elaborating anything — `Module name Types + does not match file name "verification/proofs/idris2/Types.idr"`. + The aggregate `proof-check-all` therefore fails for one of two reasons + depending on the environment: with Idris2 installed it stops at + `proof-check-idris2`, its first dependency, and never reaches + `proof-scan-dangerous`; with no prover installed every `proof-check-*` recipe + skips and the failure comes from `proof-scan-dangerous`, whose pattern matches + the words `postulate` and `Admitted` *in the templates' own comments*. Either + way the failure says nothing about whether any proof was checked. (NOT RUN + here: Idris2 is unavailable in this session, so the first path is read from the + recipe and from Idris2's own header check in `src/Idris/ProcessIdr.idr`, not + executed. Agda is not affected the same way: it adds the file's own directory + to the include path, where Idris2 keys off the source dir.) + The recipes are not reachable from the golden path (`just test && just quality`), so no gate is currently affected. `hyperpolymath/trope-checker`'s `build/just/proofs.just` carries the estate's reference treatment: it refuses to report a skip as a pass. From 5dd4df8a854af43d715f98017e9feb1985f29915 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 9 Nov 2026 21:17:01 +0000 Subject: [PATCH 5/5] docs(proofs): Clarify Agda standard library requirements in proof status and changelog --- CHANGELOG.adoc | 9 +++++---- docs/status/PROOF-STATUS.adoc | 5 +++-- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 25382fd..92b1e3c 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -14,10 +14,11 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. and it was right. `+docs/status/PROOF-STATUS.adoc+` said that with a toolchain present every individual `+proof-check-*+` recipe would report green on template boilerplate, and that only the aggregate fails, "because of comment - text, not because it checked anything". That holds for Agda, Coq and Lean but - is false for Idris2: the recipe runs `+idris2 --check+` from the repository - root with no `+--source-dir+` and there is no `+.ipkg+` in the tree, so every - file under `+verification/proofs/idris2/+` declares a module name + text, not because it checked anything". That holds for Coq and Lean, and for + Agda only if its standard library is configured (`+proof-check-agda+` does not + configure it), but is false for Idris2: the recipe runs `+idris2 --check+` from + the repository root with no `+--source-dir+` and there is no `+.ipkg+` in the + tree, so every file under `+verification/proofs/idris2/+` declares a module name (`+Types+`, `+ABI.Compliance+`, …) that cannot match the name Idris2 derives from its path. Idris2 rejects the header before elaborating anything, and because `+proof-check-all+` runs its dependencies in order it would stop there diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 7e5f26e..4098806 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -93,8 +93,9 @@ Two consequences worth stating rather than leaving implicit: * The individual `proof-check-*` recipes in `build/just/proofs.just` print `SKIP: not installed` and continue. That contradicts this repository's - own `no-silent-skip` constraint, and with an Agda, Coq or Lean toolchain - present each would report green on template boilerplate. + own `no-silent-skip` constraint, and with a Coq or Lean toolchain present each + would report green on template boilerplate. Agda would do so only if its + standard library is configured; `proof-check-agda` does not configure it. `proof-check-idris2` is the exception among the individual recipes: it runs `idris2 --check` from the repository root with no `--source-dir`, and there is no `.ipkg` anywhere in this repository, so for every file under