diff --git a/.github/workflows/verification-proofs-cron.yml b/.github/workflows/verification-proofs-cron.yml new file mode 100644 index 00000000..6a5ef867 --- /dev/null +++ b/.github/workflows/verification-proofs-cron.yml @@ -0,0 +1,144 @@ +# SPDX-License-Identifier: MPL-2.0 +# Weekly verification of the heavier self-proof corpora that are too slow and too +# network-heavy to gate on every PR: Isabelle/HOL (proofs/isabelle) and Mizar +# (proofs/mizar). Both toolchains are large, non-apt downloads -- Isabelle is a +# ~500MB tarball and additionally builds the HOL-Algebra image; Mizar ships only +# from mizar.org (Tier-4 in this project, see live-provers.yml) with its full MML. +# So this runs on a weekly schedule plus manual dispatch, mirroring container-ci. +# `just` stays the single source of truth for the commands (RSR-H14): CI installs +# the toolchains, then calls the same recipes a developer runs locally. +name: Verification Proof Corpora (weekly) + +on: + schedule: + - cron: '17 4 * * 1' # Mondays 04:17 UTC + workflow_dispatch: + # Tightly path-filtered: a PR that actually touches these proof corpora (or this + # workflow) gets one confirmation run, but unrelated PRs never trigger the heavy + # toolchains. The weekly schedule above is the primary gate; this just catches + # direct edits to the .thy/.miz sources before they land. + pull_request: + paths: + - 'proofs/isabelle/**' + - 'proofs/mizar/**' + - '.github/workflows/verification-proofs-cron.yml' + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + isabelle: + name: Isabelle/HOL + runs-on: ubuntu-latest + timeout-minutes: 60 + steps: + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + + - name: Install Isabelle + run: | + set -euo pipefail + # Resolve the current Isabelle linux x86_64 tarball from the website. A + # pinned /dist/IsabelleYYYY URL 404s once a newer release supersedes it + # (live-provers.yml's Isabelle2024 pin has rotted), so discover the link + # from the homepage, then fall back to the dist/ directory listing. + url="" + for src in "https://isabelle.in.tum.de/" "https://isabelle.in.tum.de/dist/"; do + page="$(curl -fsSL --max-time 120 --retry 3 "$src" || true)" + echo "--- candidates from $src ---" + printf '%s\n' "$page" | grep -oE '(dist/)?Isabelle[0-9][0-9-]*_linux\.tar\.gz' | sort -V | uniq | tail -5 || true + rel="$(printf '%s\n' "$page" | grep -oE '(dist/)?Isabelle[0-9][0-9-]*_linux\.tar\.gz' | sort -V | uniq | tail -1)" + if [ -n "$rel" ]; then + case "$rel" in dist/*) url="https://isabelle.in.tum.de/$rel" ;; *) url="https://isabelle.in.tum.de/dist/$rel" ;; esac + break + fi + done + [ -n "$url" ] || { echo "could not resolve Isabelle linux tarball URL" >&2; exit 1; } + echo "Resolved Isabelle URL: $url" + curl -fsSL --max-time 900 --retry 3 --retry-delay 15 -o /tmp/isabelle.tar.gz "$url" + sudo mkdir -p /opt/isabelle + sudo tar xzf /tmp/isabelle.tar.gz -C /opt/isabelle + ISABELLE_BIN="$(find /opt/isabelle -type f -name isabelle | head -n 1)" + [ -n "$ISABELLE_BIN" ] || { echo "isabelle launcher not found after extract" >&2; exit 1; } + sudo ln -sf "$ISABELLE_BIN" /usr/local/bin/isabelle + isabelle 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: Verify Isabelle corpus + run: just proofs-isabelle + + mizar: + name: Mizar + runs-on: ubuntu-latest + timeout-minutes: 60 + steps: + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + + - name: Install Mizar (system + MML) + run: | + set -euo pipefail + # Mizar ships only from mizar.org with no stable, documented path (the + # /system/i386-linux/ guess 404s). Discover the linux tarball by scraping + # the system index; dump candidate hrefs so one run reveals the layout if + # discovery misses. + # Two-stage discovery: mizar.org/system/ only links to per-arch *directories* + # on the upstream host (http://mizar.uwb.edu.pl/.../i386-linux/); the actual + # tarball lives inside that directory. + sys="$(curl -fsSL --max-time 120 --retry 3 "http://mizar.org/system/" || true)" + dir="$(printf '%s\n' "$sys" | grep -oiE 'href="http://[^"]*i386-linux/?"' \ + | sed -E 's/^href="//I; s/"$//' | head -1)" + [ -n "$dir" ] || dir="http://mizar.uwb.edu.pl/~softadm/pub/system/i386-linux/" + dir="${dir%/}/" + echo "Mizar i386-linux dir: $dir" + idx="$(curl -fsSL --max-time 120 --retry 3 "$dir" || true)" + echo "=== .tar candidates in $dir ===" + printf '%s\n' "$idx" | grep -oiE 'href="[^"]+"' | grep -iE '\.tar' | head -40 || true + rel="$(printf '%s\n' "$idx" | grep -oiE 'href="[^"]*mizar-[^"]*i386-linux\.tar"' \ + | sed -E 's/^href="//I; s/"$//' | sort -V | uniq | tail -1)" + [ -n "$rel" ] || rel="$(printf '%s\n' "$idx" | grep -oiE 'href="[^"]*\.tar"' \ + | sed -E 's/^href="//I; s/"$//' | sort -V | uniq | tail -1)" + [ -n "$rel" ] || { echo "no Mizar .tar found in $dir" >&2; exit 1; } + case "$rel" in http*) found="$rel" ;; /*) found="http://mizar.uwb.edu.pl$rel" ;; *) found="$dir$rel" ;; esac + echo "Resolved Mizar URL: $found" + curl -fsSL --max-time 600 --retry 3 -o /tmp/mizar.tar "$found" + mkdir -p "$HOME/mizar" + tar xf /tmp/mizar.tar -C "$HOME/mizar" + echo "=== outer archive contents ==="; ls -la "$HOME/mizar" | head -30 + cd "$HOME/mizar" + for inner in mizbin mizshare mizdoc; do + for ext in tar.gz tgz tar; do + [ -f "$inner.$ext" ] && { echo "extracting $inner.$ext"; tar xf "$inner.$ext"; } + done + done + echo "=== after inner extraction ==="; ls -la "$HOME/mizar" | head -40 + # mizbin.tar.gz extracts the binaries (makeenv, accom, verifier, ...) flat + # into $HOME/mizar alongside the MML share, so both PATH and MIZFILES point + # at $HOME/mizar -- there is no bin/ subdir. + echo "MIZFILES=$HOME/mizar" >> "$GITHUB_ENV" + echo "$HOME/mizar" >> "$GITHUB_PATH" + ls -l "$HOME/mizar/makeenv" "$HOME/mizar/verifier" "$HOME/mizar/accom" + + - 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: Verify Mizar corpus + run: just proofs-mizar diff --git a/Justfile b/Justfile index 9bdb676b..be107c6b 100644 --- a/Justfile +++ b/Justfile @@ -311,6 +311,38 @@ proofs-verif-idris: fi echo "Idris2 verification corpus: all files type-check" +# Heavy (downloads the ~500MB Isabelle release), so this is gated by the weekly +# verification-proofs-cron workflow, not the per-PR `proofs` rollup. Covers the +# base-HOL theories; algebra/GroupTheory.thy is excluded (see proofs/isabelle/ROOT). +# Verify the Isabelle/HOL self-proof corpus (proofs/isabelle) via `isabelle build`. +proofs-isabelle: + cd proofs/isabelle && isabelle build -d . -v Echidna_Isabelle + +# Mizar is not packaged for apt and ships only from mizar.org (Tier-4 in this +# project); like Isabelle it is gated by the weekly cron, not per-PR. MIZFILES +# must point at the Mizar share dir. Errors are reported in a per-file .err file +# (the verifier's exit code is not reliable), so a non-empty .err fails the recipe. +# Verify the Mizar self-proof corpus (proofs/mizar) with the Mizar verifier. +proofs-mizar: + #!/usr/bin/env bash + set -euo pipefail + : "${MIZFILES:?MIZFILES must point at the Mizar share dir}" + cd proofs/mizar + rc=0 + for f in *.miz; do + echo "=== makeenv + verifier $f ===" + makeenv "$f" + verifier "$f" || rc=1 + errfile="${f%.miz}.err" + if [ -s "$errfile" ]; then + echo "Mizar errors in $f:" >&2 + cat "$errfile" >&2 + rc=1 + fi + done + if [ "$rc" -ne 0 ]; then echo "Mizar corpus: VERIFICATION ERRORS" >&2; exit 1; fi + echo "Mizar corpus: all files verify" + # Format code fmt: cargo fmt diff --git a/proofs/isabelle/ROOT b/proofs/isabelle/ROOT new file mode 100644 index 00000000..42a76522 --- /dev/null +++ b/proofs/isabelle/ROOT @@ -0,0 +1,23 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* + ROOT - Isabelle session for the ECHIDNA self-proof corpus. + + Gated by `just proofs-isabelle` and the weekly verification-proofs-cron + workflow. Covers the base-HOL theories that type-check on the current + Isabelle release (confirmed green on Isabelle2025-2). + + NOTE: algebra/GroupTheory.thy is intentionally NOT in a gated session. It is + "ML training corpus" material (per its own header) that does not verify on + Isabelle2025-2: several lemmas omit their `assumes "group G"` while using + `assms`, and `center_closed` invokes `group.m_comm` which does not hold for a + bare `group` locale (only `comm_group`). Gating it would make the weekly cron + permanently red; it should be repaired as a separate task before being added. +*) + +session "Echidna_Isabelle" = "HOL" + + description \ECHIDNA Isabelle/HOL self-proof corpus (base HOL).\ + theories + Basic + List + Nat + Propositional diff --git a/proofs/isabelle/algebra/GroupTheory.thy b/proofs/isabelle/algebra/GroupTheory.thy index c5c4bfbc..59faef3d 100644 --- a/proofs/isabelle/algebra/GroupTheory.thy +++ b/proofs/isabelle/algebra/GroupTheory.thy @@ -3,7 +3,7 @@ Group Theory Examples for ML Training Corpus *) theory GroupTheory - imports Main "~~/src/HOL/Algebra/Group" + imports Main "HOL-Algebra.Group" begin (** Basic group axioms *)