11# 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).
2+ # Gates the ECHIDNA dogfood proof corpus (proofs/{coq,lean,agda}) in CI.
3+ # (Bisecting a startup_failure: minimal skeleton first, then restore jobs.)
84name : Dogfood Proof Corpus
95
106on :
2218 - ' .github/workflows/dogfood-proofs-ci.yml'
2319 workflow_dispatch :
2420
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.
2721concurrency :
2822 group : ${{ github.workflow }}-${{ github.ref }}
2923 cancel-in-progress : true
@@ -37,100 +31,5 @@ jobs:
3731 runs-on : ubuntu-latest
3832 steps :
3933 - 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
34+ - name : Smoke
35+ run : echo "skeleton OK"
0 commit comments