Skip to content

agda.yml installs an unpinned apt-get install -y agda at L51 and L176 — the prover under the proofs changes without a commit #322

Description

@hyperpolymath

Measured (2026-09-22, main = 9c4b72b)

  • .github/workflows/agda.yml:51 and :176 sudo apt-get install -y agda git (no version) on ubuntu-latest, with the stdlib cloned at v2.3.
  • Positive control: epistemic-types' Proof Safety runs in a digest-pinned debian:13-slim container with agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4, asserts agda --version, and passes --double-check; residual-evidence-types adopted the same recipe on 2026-09-22 (run 35773288367 green) with zero third-party actions.
  • Three stdlib versions are in play across the family (2.1 in residual, 2.3 here, 2.1-4 distro in epistemic-types).

Why it matters

An image bump changes the prover under the proofs without a commit: the next ubuntu-latest rollover changes the apt agda version and no receipt records which one checked the suite.

Acceptance criteria

  1. Both steps install an explicit version (agda-bin=<ver> in a digest-pinned container, or an apt pin with a checksum), and agda --version is asserted equal to the pinned string before any module is checked.
  2. Watched-failing → green: grep -c 'apt-get install -y agda git' .github/workflows/agda.yml is 2 today, 0 after.
  3. The chosen stdlib version is recorded in PROOF-STATUS with the measured warning count under it (measure the UnsupportedIndexedMatch warning count under each candidate stdlib before choosing; do not assume).
  4. Mutant: change the pinned version string to one that does not exist; the job fails at install, not silently later.

🤖 Generated with Claude Code

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions