From 0173cb439e8e2cd47a69343177ab2c507b0f85bc Mon Sep 17 00:00:00 2001 From: fraware Date: Thu, 16 Jul 2026 04:36:05 -0700 Subject: [PATCH] fix(ci): ungate lean-offline from push/schedule GitHub-hosted runners hang during/after mathlib vendor (step timeouts stop firing). Push-gated Lean stays on lean-morph; lean-offline becomes workflow_dispatch-only with concurrency, no mid-job cache save, and verify folded into the vendor step. --- .github/workflows/lean-offline.yaml | 115 ++++++++-------------------- 1 file changed, 33 insertions(+), 82 deletions(-) diff --git a/.github/workflows/lean-offline.yaml b/.github/workflows/lean-offline.yaml index acbdbe51e..40ad17c5e 100644 --- a/.github/workflows/lean-offline.yaml +++ b/.github/workflows/lean-offline.yaml @@ -1,25 +1,20 @@ name: Lean Offline Build +# Full mathlib vendor + offline lake build is unreliable on GitHub-hosted +# runners (repeated mid-vendor cancels and post-vendor runner hangs). +# Push-gated Lean CI is covered by lean-morph.yml. This workflow stays +# workflow_dispatch-only so it can still be run manually without gating +# the main inventory on an unachievable cold-cache path. on: - push: - branches: [main, develop] - paths: - - "**/*.lean" - - "**/lakefile.lean" - - "**/lean-toolchain" - - "vendor/mathlib/**" - - ".github/workflows/lean-offline.yaml" - - "scripts/vendor-mathlib.sh" - schedule: - # Warm mathlib cache and verify offline builds nightly (not a merge gate). - - cron: "0 3 * * *" workflow_dispatch: +concurrency: + group: lean-offline-${{ github.ref }} + cancel-in-progress: true + jobs: lean-offline: runs-on: ubuntu-latest - # Cold cache must finish vendor+build once so actions/cache can persist; - # prior 44m job limit cancelled nightly runs mid-vendor (no cache ever saved). timeout-minutes: 90 name: "Lean Offline Build" @@ -29,12 +24,10 @@ jobs: with: fetch-depth: 0 - - name: Restore Lean toolchain and mathlib cache - id: cache - uses: actions/cache/restore@v4 + - name: Cache Lean toolchain and mathlib artifacts + uses: actions/cache@v4 with: - # Do not cache vendor/mathlib/.git — it balloons past practical - # actions/cache upload sizes and hung tip runs for 30+ minutes. + # Do not cache vendor/mathlib/.git — upload size hung tip runs. path: | ~/.elan ~/.cache/lake @@ -43,9 +36,9 @@ jobs: spec-templates/v1/proofs/.lake bundles/my-agent/proofs/.lake bundles/test-new-user-agent/proofs/.lake - key: lean-offline-${{ hashFiles('lean-toolchain') }}-mathlib-a45ae637-v3 + key: lean-offline-${{ hashFiles('lean-toolchain') }}-mathlib-a45ae637-v4 restore-keys: | - lean-offline-${{ hashFiles('lean-toolchain') }}-mathlib-a45ae637-v3 + lean-offline-${{ hashFiles('lean-toolchain') }}-mathlib-a45ae637-v4 - name: Set up Lean (elan) run: | @@ -59,11 +52,13 @@ jobs: fi "$HOME/.elan/bin/elan" override set "$TOOLCHAIN" lean --version + df -h . - - name: Vendor mathlib + - name: Vendor mathlib and verify checkout id: vendor - timeout-minutes: 40 + timeout-minutes: 35 run: | + set -euo pipefail MATHLIB_COMMIT="a45ae63747140c1b2cbad9d46f518015c047047a" if [ -f vendor/mathlib/lakefile.lean ] && [ -d vendor/mathlib/.git ] \ && [ -d vendor/mathlib/.lake/build/lib ] \ @@ -71,57 +66,28 @@ jobs: ACTUAL=$(git -C vendor/mathlib rev-parse HEAD) if [ "$ACTUAL" = "$MATHLIB_COMMIT" ]; then echo "Cached vendored mathlib ready, skipping vendor script" - echo "vendor_ready=true" >> "$GITHUB_OUTPUT" - exit 0 + else + echo "Cached mathlib commit mismatch (expected $MATHLIB_COMMIT, got $ACTUAL)" + chmod +x scripts/vendor-mathlib.sh + bash scripts/vendor-mathlib.sh fi - echo "Cached mathlib commit mismatch (expected $MATHLIB_COMMIT, got $ACTUAL)" + else + chmod +x scripts/vendor-mathlib.sh + bash scripts/vendor-mathlib.sh fi - chmod +x scripts/vendor-mathlib.sh - bash scripts/vendor-mathlib.sh - echo "vendor_ready=true" >> "$GITHUB_OUTPUT" - - - name: Save Lean toolchain and mathlib cache - if: steps.vendor.outputs.vendor_ready == 'true' && steps.cache.outputs.cache-hit != 'true' - continue-on-error: true - timeout-minutes: 12 - uses: actions/cache/save@v4 - with: - path: | - ~/.elan - ~/.cache/lake - vendor/mathlib/.lake - core/lean-libs/.lake - spec-templates/v1/proofs/.lake - bundles/my-agent/proofs/.lake - bundles/test-new-user-agent/proofs/.lake - key: lean-offline-${{ hashFiles('lean-toolchain') }}-mathlib-a45ae637-v3 - - name: Verify vendor/mathlib exists - run: | - if [ ! -d "vendor/mathlib" ]; then - echo "vendor/mathlib directory not found!" - echo "Please run: ./scripts/vendor-mathlib.sh" - exit 1 - fi - echo "vendor/mathlib found" - - - name: Verify mathlib commit - run: | - cd vendor/mathlib - EXPECTED_COMMIT="a45ae63747140c1b2cbad9d46f518015c047047a" - ACTUAL_COMMIT=$(git rev-parse HEAD) - if [ "$ACTUAL_COMMIT" != "$EXPECTED_COMMIT" ]; then - echo "Mathlib commit mismatch!" - echo "Expected: $EXPECTED_COMMIT" - echo "Actual: $ACTUAL_COMMIT" - echo "Please run: ./scripts/vendor-mathlib.sh" + test -d vendor/mathlib + test -f vendor/mathlib/lakefile.lean + ACTUAL_COMMIT=$(git -C vendor/mathlib rev-parse HEAD) + if [ "$ACTUAL_COMMIT" != "$MATHLIB_COMMIT" ]; then + echo "Mathlib commit mismatch: expected $MATHLIB_COMMIT got $ACTUAL_COMMIT" exit 1 fi echo "Mathlib commit verified: $ACTUAL_COMMIT" + df -h . - name: Block network access run: | - # Block all outbound network traffic sudo iptables -P OUTPUT DROP sudo iptables -A OUTPUT -d 127.0.0.1 -j ACCEPT sudo iptables -A OUTPUT -d ::1 -j ACCEPT @@ -132,31 +98,24 @@ jobs: run: | echo "Building Lean proofs in offline mode..." - # Build core lean-libs cd core/lean-libs lake build echo "core/lean-libs built successfully" - # Build spec templates cd ../../spec-templates/v1/proofs lake build echo "spec-templates built successfully" - # Build my-agent cd ../../../bundles/my-agent/proofs lake build echo "my-agent built successfully" - # Build test-new-user-agent cd ../../test-new-user-agent/proofs lake build echo "test-new-user-agent built successfully" - name: Test offline build failure run: | - echo "Testing that network access is properly blocked..." - - # Try to fetch from git (should fail) if git fetch origin 2>/dev/null; then echo "Network access not properly blocked!" exit 1 @@ -164,15 +123,13 @@ jobs: echo "Network access properly blocked" - name: Restore network access + if: always() run: | - sudo iptables -P OUTPUT ACCEPT + sudo iptables -P OUTPUT ACCEPT || true echo "Network access restored" - name: Verify all proofs compile run: | - echo "Verifying Lean proofs compile..." - - # Check for 'sorry' or 'by admit' in CI-enforced targets only ENFORCED="core/lean-libs spec-templates/v1/proofs bundles/my-agent/proofs bundles/test-new-user-agent/proofs" FOUND="" for d in $ENFORCED; do @@ -200,12 +157,6 @@ jobs: echo "- Mathlib vendored at commit: a45ae63747140c1b2cbad9d46f518015c047047a" >> lean-build-report.md echo "- No placeholder proofs ('sorry' or 'by admit') found" >> lean-build-report.md echo "- Network access properly blocked during build" >> lean-build-report.md - echo "" >> lean-build-report.md - echo "Built projects:" >> lean-build-report.md - echo "- core/lean-libs" >> lean-build-report.md - echo "- spec-templates/v1/proofs" >> lean-build-report.md - echo "- bundles/my-agent/proofs" >> lean-build-report.md - echo "- bundles/test-new-user-agent/proofs" >> lean-build-report.md - name: Upload build report uses: actions/upload-artifact@v4