Repository navigation
proofs: add full-mode Agda checker and accurately record XP-1 recheck debt #129
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,84 @@ | ||
| # SPDX-License-Identifier: MPL-2.0 | ||
| # Cross-project Agda compatibility gate. Pin external source revisions. | ||
| name: Cross-project Agda Verification | ||
|
|
||
| on: | ||
| pull_request: | ||
| paths: | ||
| - 'verification/proofs/agda/**' | ||
| - 'scripts/check-agda-verification.sh' | ||
| - '.github/workflows/agda-cross-project.yml' | ||
| push: | ||
| branches: [main] | ||
| paths: | ||
| - 'verification/proofs/agda/**' | ||
| - 'scripts/check-agda-verification.sh' | ||
| - '.github/workflows/agda-cross-project.yml' | ||
| workflow_dispatch: | ||
|
|
||
| permissions: | ||
| contents: read | ||
|
|
||
| concurrency: | ||
| group: agda-cross-project-${{ github.ref }} | ||
| cancel-in-progress: true | ||
|
|
||
| jobs: | ||
| typecheck: | ||
| runs-on: ubuntu-24.04 | ||
| timeout-minutes: 45 | ||
| steps: | ||
| - name: Checkout | ||
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | ||
| with: | ||
| persist-credentials: false | ||
|
|
||
| # Use Ubuntu's GHC/Cabal packages rather than an additional | ||
| # marketplace setup action; the proof compiler itself is pinned. | ||
| - name: Install Haskell build toolchain | ||
| run: | | ||
| set -euo pipefail | ||
| sudo apt-get update -qq | ||
| sudo apt-get install -y --no-install-recommends ghc cabal-install | ||
| # Hosted runners also contain newer GHC versions whose 'base' | ||
| # package is incompatible with Agda 2.7.0.1. Choose the distro | ||
| # compiler explicitly, not the first ghc found on PATH. | ||
| /usr/bin/ghc --version | ||
| cabal --version | ||
|
|
||
| - name: Install Agda 2.7.0.1 and compatible stdlib 2.1.1 | ||
| run: | | ||
| set -euo pipefail | ||
| cabal update | ||
| cabal install Agda-2.7.0.1 --with-compiler=/usr/bin/ghc --overwrite-policy=always | ||
| echo "$HOME/.cabal/bin" >> "$GITHUB_PATH" | ||
| curl -fsSL --retry 3 -o "$RUNNER_TEMP/agda-stdlib.tar.gz" \ | ||
| https://github.com/agda/agda-stdlib/archive/refs/tags/v2.1.1.tar.gz | ||
|
Check warning on line 56 in .github/workflows/agda-cross-project.yml
|
||
| tar xzf "$RUNNER_TEMP/agda-stdlib.tar.gz" -C "$RUNNER_TEMP" | ||
| test -f "$RUNNER_TEMP/agda-stdlib-2.1.1/standard-library.agda-lib" | ||
|
|
||
| - name: Fetch pinned first-party Agda libraries | ||
| run: | | ||
| set -euo pipefail | ||
| mkdir -p "$RUNNER_TEMP/type-libs" | ||
| git clone --no-checkout https://github.com/hyperpolymath/absolute-zero.git "$RUNNER_TEMP/type-libs/absolute-zero" | ||
| git -C "$RUNNER_TEMP/type-libs/absolute-zero" checkout bb46232ea4dbc4b6ad2b97d2da6baebb3e026662 | ||
| git clone --no-checkout https://github.com/hyperpolymath/echo-types.git "$RUNNER_TEMP/type-libs/echo-types" | ||
| git -C "$RUNNER_TEMP/type-libs/echo-types" checkout b0982c44f36133acd2d0e1d4e03cf031fff7a470 | ||
|
|
||
| - name: Register exact proof library revisions | ||
| run: | | ||
| set -euo pipefail | ||
| agda --version | ||
| stdlib="$RUNNER_TEMP/agda-stdlib-2.1.1/standard-library.agda-lib" | ||
| test -f "$stdlib" | ||
| mkdir -p "$HOME/.agda" | ||
| printf '%s\n' \ | ||
| "$stdlib" \ | ||
| "$RUNNER_TEMP/type-libs/absolute-zero/absolute-zero.agda-lib" \ | ||
| "$RUNNER_TEMP/type-libs/echo-types/echo-types.agda-lib" \ | ||
| > "$HOME/.agda/libraries" | ||
| printf 'standard-library\n' > "$HOME/.agda/defaults" | ||
|
|
||
| - name: Check full Agda profile | ||
| run: bash scripts/check-agda-verification.sh | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,33 @@ | ||
| // SPDX-License-Identifier: CC-BY-SA-4.0 | ||
| = Agda cross-project proof recheck — coordination boundary | ||
| :revdate: 2026-11-01 | ||
|
|
||
| Status: *RECHECK PENDING*. Do not treat the historical | ||
| `agda Verification.agda` or `--safe --without-K` record as | ||
| evidence of the stricter Cubical-compatible mode. | ||
|
|
||
| The cross-project entrypoint is | ||
| `verification/proofs/agda/Verification.agda`, which imports | ||
| `EchoTyping.agda` and the external `echo-types` Agda library. | ||
| Its dependency chain also includes the standard library and | ||
| `absolute-zero`. Do not vendor or rewrite those libraries to force | ||
|
Comment on lines
+12
to
+13
There was a problem hiding this comment.
This dependency boundary incorrectly says that Useful? React with 👍 / 👎. |
||
| compatibility. Record the exact revisions and Agda/stdlib version | ||
| used for any successful recheck. | ||
|
|
||
| Use: | ||
|
|
||
| [source,shell] | ||
| ---- | ||
| bash scripts/check-agda-verification.sh | ||
| ---- | ||
|
|
||
| This invokes `agda --safe --without-K --cubical-compatible` | ||
| from the proper proof root. Failure or unavailable dependencies | ||
| remain visible open obligations, not successes. A successful Agda | ||
| check alone would prove the stated Agda fragment, *not* a | ||
| cross-prover correspondence or end-to-end Wasm runtime refinement. | ||
|
|
||
| Existing owning-family proof claims and CI remain with those | ||
| families; coordination does not turn them into nextgen-typing code. | ||
| The canonical policy is in `metadatastician/standards` and | ||
| the theorem-level receipt inventory is planned in Mathesis. | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,15 @@ | ||
| #!/usr/bin/env bash | ||
| # SPDX-License-Identifier: MPL-2.0 | ||
| # Cross-project Agda proof gate (no implicit dependency download or skips). | ||
| set -euo pipefail | ||
| root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" | ||
| if ! command -v agda >/dev/null 2>&1; then | ||
| echo "FATAL: Agda is missing; proof check is not optional." >&2 | ||
| exit 1 | ||
| fi | ||
| cd "$root/verification/proofs/agda" | ||
| agda --version | ||
| # The .agda-lib requires both standard-library and echo-types; echo-types | ||
| # in turn requires absolute-zero. If imports are unavailable/incompatible, | ||
| # this command fails visibly instead of fabricating a proof receipt. | ||
| agda --safe --without-K --cubical-compatible Verification.agda | ||
|
There was a problem hiding this comment.
Anyone running the repository's existing Useful? React with 👍 / 👎.
Contributor
There was a problem hiding this comment.
 |
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The repository's
.github/workflows/workflow-linter.ymlrunsgh actions-lock --verify-localwhenever a workflow changes, but.github/workflows/actions.lockhas no entry for this new workflow or its checkout dependency. Because--verify-localverifies that everyuses:reference has a workflow-specific lockfile entry (official gh-actions-lock documentation), this PR will fail the workflow-linter check; regenerate and commit the lockfile entry foragda-cross-project.yml.Useful? React with 👍 / 👎.