ci(proofs): weekly cron gating the Isabelle + Mizar self-proof corpora

.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

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

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 \<open>ECHIDNA Isabelle/HOL self-proof corpus (base HOL).\<close>
+  theories
+    Basic
+    List
+    Nat
+    Propositional

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 *)