fix(ci): clear OSSF Scorecard startup_failure (#119) #77
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
| # SPDX-License-Identifier: MPL-2.0 | ||
| # lean-proofs.yml — machine-checks the Lean 4 formal-verification proofs. | ||
| # | ||
| # Guards the root cause documented in docs/proofs/verification/AUDIT.md: the | ||
| # proofs had bit-rotted because no CI ever ran the prover. This gate keeps the | ||
| # "sorry-free, compiles" invariant honest from now on. | ||
| name: lean-proofs | ||
| on: | ||
| push: | ||
| paths: | ||
| - 'docs/proofs/verification/**' | ||
| - '.github/workflows/lean-proofs.yml' | ||
| pull_request: | ||
| paths: | ||
| - 'docs/proofs/verification/**' | ||
| - '.github/workflows/lean-proofs.yml' | ||
| permissions: | ||
| contents: read | ||
| jobs: | ||
| lean-check: | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | ||
| - name: Install Lean (version pinned by lean-toolchain) | ||
| run: | | ||
| set -euo pipefail | ||
| ver="$(sed -E 's#.*:v##' docs/proofs/verification/lean-toolchain)" | ||
| echo "Installing Lean ${ver}" | ||
| sudo apt-get update | ||
| sudo apt-get install -y zstd | ||
| curl -sSL -o /tmp/lean.tar.zst \ | ||
| "https://github.com/leanprover/lean4/releases/download/v${ver}/lean-${ver}-linux.tar.zst" | ||
| sudo mkdir -p /opt/lean | ||
| sudo tar --use-compress-program=unzstd -xf /tmp/lean.tar.zst -C /opt/lean | ||
| echo "/opt/lean/lean-${ver}-linux/bin" >> "$GITHUB_PATH" | ||
| - name: Verify WokeLang.lean (sorry-free; must exit 0 with no errors) | ||
| run: | | ||
| set -euo pipefail | ||
| lean --version | ||
| lean docs/proofs/verification/WokeLang.lean | ||
| echo "✅ WokeLang.lean verified" | ||
| - name: Verify WokeGrammar.lean (grammar proofs; sorry-free; must exit 0) | ||
| run: | | ||
| set -euo pipefail | ||
| lean docs/proofs/verification/WokeGrammar.lean | ||
| echo "✅ WokeGrammar.lean verified" | ||
| - name: Verify WokeGrammarStructure.lean (no-left-recursion + lexer + classification) | ||
| run: | | ||
| set -euo pipefail | ||
| lean docs/proofs/verification/WokeGrammarStructure.lean | ||
| echo "✅ WokeGrammarStructure.lean verified" | ||
| - name: Verify WokeGrammarRegular.lean (§7.1 not-regular: DFA + pigeonhole) | ||
| run: | | ||
| set -euo pipefail | ||
| lean docs/proofs/verification/WokeGrammarRegular.lean | ||
| echo "✅ WokeGrammarRegular.lean verified" | ||
| - name: Verify WokeGrammarCFL.lean (§7.3 CFL closure: union/concat/star) | ||
| run: | | ||
| set -euo pipefail | ||
| lean docs/proofs/verification/WokeGrammarCFL.lean | ||
| echo "✅ WokeGrammarCFL.lean verified" | ||
| - name: Verify WokeGrammarPumping.lean (§7.3 non-closure: pumping foundation) | ||
| run: | | ||
| set -euo pipefail | ||
| lean docs/proofs/verification/WokeGrammarPumping.lean | ||
| echo "✅ WokeGrammarPumping.lean verified" | ||
