chore: commit open changes [lean-runtime-analysis] #53
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Lean CI | |
| on: | |
| push: | |
| branches: | |
| - master | |
| - peer-review-fixes | |
| - 'epic/**' | |
| pull_request: | |
| branches: [master] | |
| jobs: | |
| build-and-verify: | |
| runs-on: self-hosted | |
| name: Build & Verify Formalization | |
| timeout-minutes: 25 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Install Elan | |
| run: | | |
| curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Cache Mathlib | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .lake/packages/mathlib | |
| .lake/build | |
| key: lake-${{ runner.os }}-${{ hashFiles('lakefile.lean', 'lake-manifest.json', 'lean-toolchain') }} | |
| restore-keys: lake-${{ runner.os }}- | |
| - name: Build | |
| run: lake build | |
| - name: Check for sorry | |
| run: | | |
| echo "::group::Searching for sorry in Lean sources" | |
| # LBTCoupling.lean has documented deferred proofs (LBT, selection amplification, G2). | |
| # These are tracked as known gaps — see Mechanization Boundary section in that file. | |
| FOUND=$(grep -rn 'sorry' --include='*.lean' . \ | |
| | grep -v '\.lake/packages/' \ | |
| | grep -v '^Binary' \ | |
| | grep -v 'LBTCoupling.lean' \ | |
| || true) | |
| if [ -n "$FOUND" ]; then | |
| echo "::error::Found sorry in Lean sources (outside LBTCoupling.lean)" | |
| echo "$FOUND" | |
| exit 1 | |
| fi | |
| # Count deferred proofs in LBTCoupling.lean for the summary | |
| LBT_SORRY=$(grep -c 'sorry' LBTCoupling.lean 2>/dev/null || echo "0") | |
| echo "LBTCoupling.lean deferred proofs: ${LBT_SORRY} (known gaps, not enforced)" | |
| echo "No sorry found in other Lean sources." | |
| echo "::endgroup::" | |
| - name: Check for axiom declarations | |
| run: | | |
| echo "::group::Searching for axiom declarations" | |
| FOUND=$(grep -rnE '^\s*(private\s+|protected\s+|noncomputable\s+)*axiom\b' --include='*.lean' . \ | |
| | grep -v '\.lake/packages/' \ | |
| || true) | |
| if [ -n "$FOUND" ]; then | |
| echo "::error::Found axiom declarations in Lean sources" | |
| echo "$FOUND" | |
| exit 1 | |
| fi | |
| echo "No axiom declarations found." | |
| echo "::endgroup::" | |
| - name: Check for admit | |
| run: | | |
| echo "::group::Searching for admit" | |
| FOUND=$(grep -rn 'admit' --include='*.lean' . \ | |
| | grep -v '\.lake/packages/' \ | |
| | grep -v 'sorry_admit' \ | |
| || true) | |
| if [ -n "$FOUND" ]; then | |
| echo "::error::Found admit in Lean sources" | |
| echo "$FOUND" | |
| exit 1 | |
| fi | |
| echo "No admit found." | |
| echo "::endgroup::" | |
| - name: Check for native_decide | |
| run: | | |
| echo "::group::Searching for native_decide" | |
| FOUND=$(grep -rn 'native_decide' --include='*.lean' . \ | |
| | grep -v '\.lake/packages/' \ | |
| || true) | |
| if [ -n "$FOUND" ]; then | |
| echo "::error::Found native_decide in Lean sources (bypasses kernel — use decide instead)" | |
| echo "$FOUND" | |
| exit 1 | |
| fi | |
| echo "No native_decide found." | |
| echo "::endgroup::" | |
| - name: Mechanization completeness audit | |
| run: | | |
| echo "::group::Mechanization completeness audit" | |
| ERRORS=0 | |
| check_theorem() { | |
| local file="$1" name="$2" label="$3" | |
| if grep -qE "^[[:space:]]*(private[[:space:]]+|protected[[:space:]]+|noncomputable[[:space:]]+)*theorem[[:space:]]+${name}\\b" "$file"; then | |
| echo " ✓ $label: $name" | |
| else | |
| echo "::error::$label missing: theorem $name not found in $file" | |
| ERRORS=$((ERRORS + 1)) | |
| fi | |
| } | |
| check_no_stub() { | |
| local file="$1" pattern="$2" label="$3" | |
| if grep -qF "$pattern" "$file"; then | |
| echo "::error::$label still contains stub: $pattern" | |
| ERRORS=$((ERRORS + 1)) | |
| else | |
| echo " ✓ $label: no stub markers" | |
| fi | |
| } | |
| echo "" | |
| echo "=== Fully mechanized (verified present) ===" | |
| check_theorem LeCamLowerBound.lean tight_sample_lower_bound "Thm 4 (Le Cam)" | |
| check_theorem LeCamLowerBound.lean hellingerSq_uniform_shift "Thm 4 (H² shift)" | |
| check_theorem LeCamLowerBound.lean exists_grid_size "Thm 4 (grid size)" | |
| check_theorem WitnessGameDrift.lean C_k_nonneg "Lem 4 (Y-drift)" | |
| check_theorem WitnessGameDrift.lean batch_mean_formula "Lem 5 (batch-mean)" | |
| check_theorem WitnessGameDrift.lean progression_gap_sum "Lem 5 (progression)" | |
| check_theorem WitnessGameDrift.lean regression_gap_sum "Lem 5 (regression)" | |
| check_theorem WitnessGameDrift.lean batch_mean_misranking "Prop 3 (misranking)" | |
| check_theorem RLocalGames.lean r_local_offset_bound "Lem 3 (r-local offset)" | |
| check_theorem RLocalGames.lean r_local_alignment "Thm 7 (r-local alignment)" | |
| check_theorem DriftTheorems/NegativeDrift.lean negative_drift_theorem "NDT (abstract)" | |
| echo "" | |
| echo "=== Required (must be fully mechanized) ===" | |
| check_theorem RLocalGames.lean r_local_tightness_all_pairs_misranked "Prop 1 (cyclic adversarial)" | |
| check_no_stub RLocalGames.lean "Uses a trivial zero-game" "Prop 1 (stub check)" | |
| echo "" | |
| echo "=== Skipped (known gaps — not enforced) ===" | |
| echo " ⊘ Thm 9: ND coupling → E[T_X] = 2^Ω(n)" | |
| echo " ⊘ Thm 8: LBT coupling → E[T_X] = O(n log n)" | |
| echo "" | |
| if [ $ERRORS -gt 0 ]; then | |
| echo "::error::$ERRORS mechanization target(s) missing or incomplete" | |
| exit 1 | |
| fi | |
| echo "All required mechanization targets present." | |
| echo "::endgroup::" | |
| - name: Summary | |
| run: | | |
| echo "## Formalization Status" >> $GITHUB_STEP_SUMMARY | |
| echo "" >> $GITHUB_STEP_SUMMARY | |
| LEAN_FILES=$(find . -name '*.lean' -not -path './.lake/*' | wc -l) | |
| TOTAL_LINES=$(find . -name '*.lean' -not -path './.lake/*' -exec cat {} + | wc -l) | |
| SORRY_COUNT=$(grep -rn 'sorry' --include='*.lean' . | grep -v '\.lake/packages/' | grep -v '^Binary' | wc -l || true) | |
| AXIOM_COUNT=$(grep -rnE '^\s*(private\s+|protected\s+|noncomputable\s+)*axiom\b' --include='*.lean' . | grep -v '\.lake/packages/' | wc -l || true) | |
| ADMIT_COUNT=$(grep -rn 'admit' --include='*.lean' . | grep -v '\.lake/packages/' | grep -v 'sorry_admit' | wc -l || true) | |
| NATIVE_DECIDE_COUNT=$(grep -rn 'native_decide' --include='*.lean' . | grep -v '\.lake/packages/' | wc -l || true) | |
| echo "- **Lean source files:** ${LEAN_FILES}" >> $GITHUB_STEP_SUMMARY | |
| echo "- **Total lines:** ${TOTAL_LINES}" >> $GITHUB_STEP_SUMMARY | |
| echo "- **sorry count:** ${SORRY_COUNT} (3 documented deferred proofs in LBTCoupling.lean)" >> $GITHUB_STEP_SUMMARY | |
| echo "- **axiom count:** ${AXIOM_COUNT}" >> $GITHUB_STEP_SUMMARY | |
| echo "- **admit count:** ${ADMIT_COUNT}" >> $GITHUB_STEP_SUMMARY | |
| echo "- **native_decide count:** ${NATIVE_DECIDE_COUNT}" >> $GITHUB_STEP_SUMMARY | |
| echo "- **required theorem:** Proposition 1 (r_local_tightness_all_pairs_misranked)" >> $GITHUB_STEP_SUMMARY |