Skip to content

Commit 757762d

Browse files
claudeclaude
committed
ci(proofs): gate the dogfood proof corpus (Coq, Lean, Agda, Idris validator)
The proof corpus had zero CI coverage: agda-meta-checker.yml only triggers on meta-checker/**, idris2-abi-ci.yml only on src/abi/**, and there was no Coq or Lean workflow at all. So proofs/{coq,lean,agda} and src/idris were never type-checked in CI — a green PR proved nothing about the proofs and regressions would land silently. New dogfood-proofs-ci.yml with three jobs (Coq via apt, Lean 4 via elan, Agda 2.7.0.1 + stdlib v2.1), each calling a just recipe so local and CI run identical commands (RSR-H14). idris2-abi-ci.yml extended to also type-check the src/idris validator (reuses its Idris2 install; adds src/idris/** to the path trigger). Closing the gap surfaced two latent bugs the absent CI had hidden: - proofs/lean/lakefile.lean rooted only `ECHIDNA`, whose umbrella imported 4 of 6 files; `lake build` silently skipped algebra/GroupTheory.lean and mvp_basic.lean, and in fact failed outright ("unknown module prefix 'Basic'") because the top-level modules were not in the lib's module space. Now every proof file is a root and ECHIDNA.lean imports the whole corpus. - src/idris/echidna-validator.ipkg declares an executable (main = Validator) but Validator.idr had no `main`, so `idris2 --build` failed with "Undefined name Validator.main". Added `main = testValidation`. New Justfile recipes: proofs, proofs-coq, proofs-lean, proofs-agda, proofs-idris (proofs-agda exports LC_ALL=C.UTF-8 — Agda aborts under a non-UTF-8 locale). Verified locally against real toolchains: coqc 8.18.0 (5/5), Lean v4.13.0 lake build (6 modules + umbrella), agda (13/13), idris2 0.8.0 --typecheck. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 0a190ba commit 757762d

6 files changed

Lines changed: 201 additions & 4 deletions

File tree

‎.github/workflows/dogfood-proofs-ci.yml‎

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Gates the ECHIDNA dogfood proof corpus: every theorem under proofs/{coq,lean,agda}
3+
# must type-check. These proofs had no CI coverage before this workflow — the
4+
# language-specific path filters on the other proof workflows (agda-meta-checker
5+
# → meta-checker/**, idris2-abi-ci → src/abi/**) never touched proofs/**, so
6+
# regressions here were invisible. Each job calls a `just` recipe so local and
7+
# CI run the identical command (RSR-H14).
8+
name: Dogfood Proof Corpus
9+
10+
on:
11+
push:
12+
branches: [main]
13+
paths:
14+
- 'proofs/**'
15+
- 'Justfile'
16+
- '.github/workflows/dogfood-proofs-ci.yml'
17+
pull_request:
18+
branches: [main]
19+
paths:
20+
- 'proofs/**'
21+
- 'Justfile'
22+
- '.github/workflows/dogfood-proofs-ci.yml'
23+
workflow_dispatch:
24+
25+
# Cause-B mitigation (#77): cancel superseded runs so stacked pushes
26+
# to the same ref don't pile up identical jobs in the queue.
27+
concurrency:
28+
group: ${{ github.workflow }}-${{ github.ref }}
29+
cancel-in-progress: true
30+
31+
permissions:
32+
contents: read
33+
34+
jobs:
35+
coq:
36+
name: Coq
37+
runs-on: ubuntu-latest
38+
steps:
39+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
40+
41+
- name: Install Coq
42+
run: |
43+
set -euo pipefail
44+
sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
45+
sudo apt-get install -y --fix-missing coq
46+
coqc --version
47+
48+
- name: Install just
49+
uses: taiki-e/install-action@e49978b799e49ff429d162b7a30601a569ab6538 # v2.81.1
50+
with:
51+
tool: just@1.51.0
52+
53+
- name: Type-check Coq corpus
54+
run: just proofs-coq
55+
56+
lean:
57+
name: Lean 4
58+
runs-on: ubuntu-latest
59+
steps:
60+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
61+
62+
- name: Cache elan + Lean toolchain
63+
uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
64+
with:
65+
path: ~/.elan
66+
key: elan-${{ runner.os }}-${{ hashFiles('proofs/lean/lean-toolchain') }}
67+
68+
- name: Install elan (Lean toolchain manager)
69+
run: |
70+
set -euo pipefail
71+
# The toolchain version itself is pinned by proofs/lean/lean-toolchain
72+
# (lake reads it and fetches that exact Lean on first invocation).
73+
if [ ! -x "$HOME/.elan/bin/lake" ]; then
74+
curl -fsSL --retry 3 \
75+
https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
76+
-o /tmp/elan-init.sh
77+
sh /tmp/elan-init.sh -y --default-toolchain none
78+
fi
79+
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
80+
81+
- name: Install just
82+
uses: taiki-e/install-action@e49978b799e49ff429d162b7a30601a569ab6538 # v2.81.1
83+
with:
84+
tool: just@1.51.0
85+
86+
- name: Build Lean corpus
87+
run: just proofs-lean
88+
89+
agda:
90+
name: Agda
91+
runs-on: ubuntu-latest
92+
steps:
93+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
94+
95+
- name: Setup Haskell
96+
uses: haskell-actions/setup@cd0d9bdd65b20557f41bea4dbe43d0b5fbbfe553 # v2
97+
with:
98+
ghc-version: '9.6'
99+
cabal-version: '3.10'
100+
101+
- name: Cache cabal (Agda build)
102+
uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
103+
with:
104+
# Keyed on the Agda version, not the proofs, so the expensive
105+
# from-source Agda build is reused across proof-only changes.
106+
path: ~/.cabal
107+
key: agda-cabal-${{ runner.os }}-Agda-2.7.0.1
108+
109+
- name: Install Agda
110+
run: |
111+
set -euo pipefail
112+
cabal update
113+
# --overwrite-policy=always: a warm ~/.cabal cache already carries
114+
# the agda symlink, so a plain install aborts with "path exists".
115+
cabal install Agda-2.7.0.1 --overwrite-policy=always
116+
echo "$HOME/.cabal/bin" >> "$GITHUB_PATH"
117+
118+
- name: Install Agda standard library (v2.1)
119+
run: |
120+
set -euo pipefail
121+
mkdir -p ~/.agda
122+
cd /tmp
123+
wget -q https://github.com/agda/agda-stdlib/archive/refs/tags/v2.1.tar.gz
124+
tar xzf v2.1.tar.gz
125+
# Fresh registration each run (`>`), then append the corpus library.
126+
echo "/tmp/agda-stdlib-2.1/standard-library.agda-lib" > ~/.agda/libraries
127+
echo "standard-library" > ~/.agda/defaults
128+
echo "${GITHUB_WORKSPACE}/proofs/agda/echidna-proofs.agda-lib" >> ~/.agda/libraries
129+
130+
- name: Install just
131+
uses: taiki-e/install-action@e49978b799e49ff429d162b7a30601a569ab6538 # v2.81.1
132+
with:
133+
tool: just@1.51.0
134+
135+
- name: Type-check Agda corpus
136+
run: just proofs-agda

‎.github/workflows/idris2-abi-ci.yml‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,12 @@ on:
55
push:
66
paths:
77
- 'src/abi/**'
8+
- 'src/idris/**'
89
- '.github/workflows/idris2-abi-ci.yml'
910
pull_request:
1011
paths:
1112
- 'src/abi/**'
13+
- 'src/idris/**'
1214
- '.github/workflows/idris2-abi-ci.yml'
1315

1416
# Cause-B mitigation (#77): cancel superseded runs so stacked pushes
@@ -57,6 +59,16 @@ jobs:
5759
idris2 --build echidnaabi.ipkg
5860
echo "✓ All ABI modules type-check successfully"
5961
62+
- name: Type-check Idris2 proof validator (src/idris)
63+
run: |
64+
# Mirrors `just proofs-idris`. --typecheck (not --build) so no codegen
65+
# backend is required; the declared executable's `main` is exercised
66+
# by `idris2 --build` locally where a backend is present.
67+
cd src/idris
68+
echo "=== Type-checking ECHIDNA proof validator ==="
69+
idris2 --typecheck echidna-validator.ipkg
70+
echo "✓ Validator modules type-check successfully"
71+
6072
- name: Verify no dangerous patterns
6173
run: |
6274
echo "=== Scanning for dangerous patterns in ABI code ==="

‎Justfile‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -244,6 +244,46 @@ test-s4-loop:
244244
@echo "Test will skip cleanly if the endpoint is unreachable."
245245
cargo test --features verisim --test s4_loop_closure -- --nocapture
246246

247+
# ── Dogfood proof corpus (proofs/{coq,lean,agda} + src/idris validator) ──
248+
# Each recipe assumes its toolchain is already installed (see `just doctor`);
249+
# CI installs the toolchains first, then calls these so local and CI run the
250+
# exact same commands.
251+
252+
# Type-check the whole dogfood proof corpus across every assistant.
253+
proofs: proofs-coq proofs-lean proofs-agda proofs-idris
254+
255+
# Compile the Coq proof corpus (proofs/coq/**/*.v).
256+
proofs-coq:
257+
#!/usr/bin/env bash
258+
set -euo pipefail
259+
cd proofs/coq
260+
for f in $(find . -name '*.v' | sort); do
261+
echo "coqc $f"
262+
coqc -q "$f"
263+
done
264+
echo "Coq corpus: all files type-check"
265+
266+
# Build the Lean 4 proof corpus via Lake (proofs/lean).
267+
proofs-lean:
268+
cd proofs/lean && lake build
269+
270+
# Type-check the Agda proof corpus (proofs/agda/*.agda).
271+
proofs-agda:
272+
#!/usr/bin/env bash
273+
set -euo pipefail
274+
# Agda writes UTF-8 to stdout and aborts under a non-UTF-8 locale (C/POSIX).
275+
export LC_ALL="${LC_ALL:-C.UTF-8}"
276+
cd proofs/agda
277+
for f in $(find . -name '*.agda' -not -path './_build/*' -not -path './dist-newstyle/*' | sort); do
278+
echo "agda $f"
279+
agda "$f"
280+
done
281+
echo "Agda corpus: all files type-check"
282+
283+
# Type-check the Idris2 validator (src/idris) — --typecheck needs no codegen backend.
284+
proofs-idris:
285+
cd src/idris && idris2 --typecheck echidna-validator.ipkg
286+
247287
# Format code
248288
fmt:
249289
cargo fmt

‎proofs/lean/ECHIDNA.lean‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
-- SPDX-License-Identifier: MPL-2.0
22
-- Copyright (c) 2025 ECHIDNA Project Team
3-
-- ECHIDNA proof library root module — imports all sub-modules.
3+
-- ECHIDNA proof library root module — umbrella import of the whole corpus.
44
import Basic
55
import Nat
66
import List
77
import Propositional
8+
import mvp_basic
9+
import algebra.GroupTheory

‎proofs/lean/lakefile.lean‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,12 @@ import Lake
22
open Lake DSL
33

44
package echidna_proofs where
5-
-- add package configuration options here
5+
-- ECHIDNA dogfood proof corpus — pure Lean 4 core, no Mathlib / external deps.
66

77
@[default_target]
88
lean_lib ECHIDNA where
9-
-- add library configuration options here
10-
roots := #[`ECHIDNA]
9+
-- Each proof file is its own top-level module, so every file must be listed
10+
-- as a root: a single umbrella root only builds the modules reachable through
11+
-- its import graph, silently skipping the rest. Listing them all makes
12+
-- `lake build` type-check the entire corpus.
13+
roots := #[`ECHIDNA, `Basic, `Nat, `List, `Propositional, `mvp_basic, `algebra.GroupTheory]

‎src/idris/Validator.idr‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -191,3 +191,7 @@ testValidation = do
191191
putStrLn $ show (validateProof proof3 goal3)
192192

193193
putStrLn "Validation tests complete."
194+
195+
-- Executable entry point (declared in echidna-validator.ipkg: `main = Validator`).
196+
main : IO ()
197+
main = testValidation

0 commit comments

Comments
 (0)