ci(proofs): restore full dogfood corpus CI without marketplace setup actions

taiki-e/install-action reproducibly triggers a startup_failure in this
workflow's context (bisected: header + checkout + run steps start fine; adding
the action fails before any job runs, even though mvp-smoke.yml uses the same
pin on main). Switch all toolchain installs to plain run steps -- apt for Coq
and Agda, curl tarballs for elan and just -- matching the idris2/chapel
workflows, which use only actions/checkout plus run steps.

Agda now installs via apt (agda + agda-stdlib), which reproduces the local
verification environment exactly. just is installed from its release tarball.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: claude

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

@@ -1,6 +1,16 @@
 # SPDX-License-Identifier: MPL-2.0
-# Gates the ECHIDNA dogfood proof corpus (proofs/{coq,lean,agda}) in CI.
-# (Bisecting a startup_failure: testing curl-installed just, no marketplace action.)
+# Gates the ECHIDNA dogfood proof corpus: every theorem under proofs/{coq,lean,agda}
+# must type-check. These proofs had no CI coverage before this workflow -- the other
+# proof workflows are path-filtered to meta-checker/** (agda-meta-checker) and
+# src/abi/** (idris2-abi-ci), and there was no Coq or Lean workflow at all, so
+# regressions in proofs/ landed silently.
+#
+# Toolchains are installed with plain `run:` steps (apt / curl tarballs, matching the
+# idris2 + chapel workflows) rather than marketplace setup actions: a third-party
+# setup action (taiki-e/install-action) reproducibly tripped a startup_failure in this
+# workflow's context, so this workflow uses only actions/checkout plus run steps.
+# `just` stays the single source of truth for the commands (RSR-H14) -- CI installs it
+# and calls the same recipes a developer runs locally.
 name: Dogfood Proof Corpus
 
 on:
@@ -32,6 +42,76 @@ jobs:
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
+      - name: Install Coq
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
+          sudo apt-get install -y --fix-missing coq
+          coqc --version
+
+      - name: Install just
+        run: |
+          set -euo pipefail
+          curl -fsSL --retry 3 \
+            "https://github.com/casey/just/releases/download/1.51.0/just-1.51.0-x86_64-unknown-linux-musl.tar.gz" \
+            -o /tmp/just.tar.gz
+          mkdir -p "$HOME/.local/bin"
+          tar xzf /tmp/just.tar.gz -C "$HOME/.local/bin" just
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
+
+      - name: Type-check Coq corpus
+        run: just proofs-coq
+
+  lean:
+    name: Lean 4
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Install elan + Lean toolchain
+        run: |
+          set -euo pipefail
+          # The toolchain version is pinned by proofs/lean/lean-toolchain; lake reads
+          # it and fetches that exact Lean on first invocation.
+          curl -fsSL --retry 3 \
+            https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Install just
+        run: |
+          set -euo pipefail
+          curl -fsSL --retry 3 \
+            "https://github.com/casey/just/releases/download/1.51.0/just-1.51.0-x86_64-unknown-linux-musl.tar.gz" \
+            -o /tmp/just.tar.gz
+          mkdir -p "$HOME/.local/bin"
+          tar xzf /tmp/just.tar.gz -C "$HOME/.local/bin" just
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
+
+      - name: Build Lean corpus
+        run: just proofs-lean
+
+  agda:
+    name: Agda
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Install Agda + standard library
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
+          sudo apt-get install -y --fix-missing agda agda-stdlib
+          agda --version
+          # Register the Ubuntu-packaged standard library so the corpus's
+          # `depend: standard-library` resolves (the corpus .agda-lib is
+          # auto-detected from proofs/agda when agda runs there).
+          mkdir -p ~/.agda
+          STDLIB="$(find /usr/share -name standard-library.agda-lib 2>/dev/null | head -1)"
+          echo "$STDLIB" > ~/.agda/libraries
+          echo "standard-library" > ~/.agda/defaults
+
       - name: Install just
         run: |
           set -euo pipefail
@@ -42,5 +122,5 @@ jobs:
           tar xzf /tmp/just.tar.gz -C "$HOME/.local/bin" just
           echo "$HOME/.local/bin" >> "$GITHUB_PATH"
 
-      - name: Smoke
-        run: just --version
+      - name: Type-check Agda corpus
+        run: just proofs-agda