ci(a-sounder-constitution): gate the Idris2 proof with idris2 --check - #46
Merged
Merged
Conversation
Add .github/workflows/idris2-proof.yml: builds Idris2 0.7.0 (Chez Scheme backend) and runs `idris2 --check a-sounder-constitution/formal/Constitution.idr` on every change under `formal/`. The certificate shipped once without being machine-checked and did not actually compile (#45); this gate stops the proof from drifting out of sync with its claims again. - Path-filtered to `formal/**` + the workflow file, so it only runs when the proof changes (keeps Actions burn low — no caching, builds from source). - Passes the repo's workflow-linter rules: SPDX header, top-level `permissions: contents: read`, SHA-pinned actions, concurrency guardrail. - formal/README.adoc: note that CI now enforces the check. Verified locally: YAML parses, all linter rules pass, and `idris2 --check Constitution.idr` exits 0 under Idris2 0.7.0. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015w8C1xaGwiDcHHjfuxHBd6
|
hyperpolymath
added a commit
that referenced
this pull request
Jun 27, 2026
…oof gate is red on main) (#47) ## The gate from #46 is failing on `main` The `Idris2 Proof` workflow added in #46 went **red** on `main` (run #2). The build and install of Idris2 0.7.0 succeeded; the failure is the check invocation: ``` Idris 2, version 0.7.0 1/1: Building a-sounder-constitution.formal.Constitution (a-sounder-constitution/formal/Constitution.idr) Error: Module name Constitution does not match file name "a-sounder-constitution/formal/Constitution.idr" ``` ### Why Idris2 derives the **expected module name from the path you give it**. Checking `a-sounder-constitution/formal/Constitution.idr` from the repo root makes it expect `module a-sounder-constitution.formal.Constitution` — which can't even be a legal module name (hyphens). The file declares `module Constitution`, which is correct. I verified the proof locally by running *from inside* `formal/` (`idris2 --check Constitution.idr`); the workflow ran it from the repo root, so it only surfaced once CI actually executed — and #46 merged before its first run finished. ### Fix Run the check from the module's own directory: ```yaml - name: Type-check the constitutional proof working-directory: a-sounder-constitution/formal run: | idris2 --check Constitution.idr ``` ### Verified locally (Idris2 0.7.0) - repo root + full path → **exit 1**, the exact CI error (reproduced) - `working-directory: a-sounder-constitution/formal` + `idris2 --check Constitution.idr` → **exit 0**, clean - YAML valid; still passes the workflow-linter rules (SPDX / `permissions` / SHA-pins) This PR edits the workflow file, so it matches the path filter and the gate runs on this PR — CI here is the end-to-end proof of the fix. **Worth letting `idris2-check` go green before merging this time.** 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_015w8C1xaGwiDcHHjfuxHBd6 --- _Generated by [Claude Code](https://claude.ai/code/session_015w8C1xaGwiDcHHjfuxHBd6)_ Co-authored-by: Claude <noreply@anthropic.com>
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.
Wire
idris2 --checkinto CIFollow-up to #45. That PR fixed a proof that had been merged claiming to compile but didn't — because nothing ever ran Idris2 on it. This adds the missing gate so it can't happen again.
What it does
.github/workflows/idris2-proof.yml:idris2 --check a-sounder-constitution/formal/Constitution.idr.Conventions followed
a-sounder-constitution/formal/**+ the workflow file, so it only runs when the proof actually changes — keeps Actions burn low (the reason there's no caching: the repo pins noactions/cacheSHA, and I won't introduce an unverifiable pin; a source build only fires on rare proof edits).workflow-linter.yml: SPDX header on line 1, top-levelpermissions: contents: read, alluses:SHA-pinned (actions/checkout@de0fac2e…),concurrencyguardrail withcancel-in-progress.formal/README.adocupdated to note CI now enforces the check.Verified locally (in the cloud session, where Idris2 0.7.0 is installed)
python3 -c 'yaml.safe_load(...)'→ YAML valididris2 --check formal/Constitution.idr→ exit 0, cleanThe workflow's own build path (apt
chezscheme→ tarball →make bootstrap/install) is exactly the sequence used to verify #45, so it mirrors a known-good install. It will run for the first time on this PR (it touchesformal/README.adoc, matching the path filter), so CI here is itself the end-to-end test.Scope: one new workflow + one doc note. No code or simulator behaviour touched.
🤖 Generated with Claude Code
https://claude.ai/code/session_015w8C1xaGwiDcHHjfuxHBd6
Generated by Claude Code