Reduce strict defeq compatibility options (#8) #139
Workflow file for this run
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: CI | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| branches: [main] | |
| jobs: | |
| count-checks: | |
| name: Sorry / axiom count | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Count sorries against docs/SORRY_CATALOG.md | |
| run: | | |
| # Tightened regex: match only standalone `sorry` (line is exactly | |
| # whitespace-then-sorry-then-whitespace), `by sorry`, `:= sorry`. | |
| # Excludes docstring text like "sorry'd" or "left as sorry". | |
| ACTUAL=$(grep -rnE "^[[:space:]]*sorry[[:space:]]*$|by sorry|:= sorry" \ | |
| --include="*.lean" \ | |
| OpenGALib \ | |
| 2>/dev/null | wc -l | tr -d ' ') | |
| EXPECTED=36 | |
| if [ "$ACTUAL" -ne "$EXPECTED" ]; then | |
| echo "::error::Sorry count drift: expected $EXPECTED, found $ACTUAL" | |
| echo "If the change is intentional, update docs/SORRY_CATALOG.md (and the EXPECTED constant in this workflow)." | |
| echo "If unintentional, close the new sorry or revert the regression." | |
| exit 1 | |
| fi | |
| echo "Sorry count: $ACTUAL (matches docs/SORRY_CATALOG.md)" | |
| - name: Count axioms (expect zero) | |
| run: | | |
| # Match only true axiom declarations: `axiom <ident>` at start of line, | |
| # nothing trailing. Excludes docstring text where 'axiom' may begin a | |
| # wrapped sentence (e.g., `axiom about CovariantDerivative wrapping`). | |
| ACTUAL=$(grep -rnE "^axiom[[:space:]]+[a-zA-Z_][a-zA-Z0-9_']*[[:space:]]*$" \ | |
| --include="*.lean" \ | |
| OpenGALib \ | |
| 2>/dev/null | wc -l | tr -d ' ') | |
| EXPECTED=0 | |
| if [ "$ACTUAL" -ne "$EXPECTED" ]; then | |
| echo "::error::Axiom count drift: expected $EXPECTED, found $ACTUAL" | |
| echo "If the change is intentional, document the axiom in module docstrings (and update the EXPECTED constant in this workflow)." | |
| echo "If unintentional, close the new axiom or revert the regression." | |
| exit 1 | |
| fi | |
| echo "Axiom count: $ACTUAL" | |
| build: | |
| name: Lake build | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 60 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install elan (Lean toolchain manager) | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| - name: Print Lean version | |
| run: lean --version | |
| # Cache the FULL Lake build: Mathlib oleans (via `lake exe cache get`), | |
| # OpenGALib oleans (incremental — Lake re-elaborates only changed | |
| # files + transitive deps), plus packages. Key on | |
| # lake-manifest + toolchain so a Mathlib/toolchain bump invalidates. | |
| # Branch prefix in restore-keys allows in-PR cache reuse across pushes. | |
| - name: Cache .lake build artifacts | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .lake/build | |
| .lake/packages | |
| key: lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json', 'lean-toolchain') }}-${{ github.sha }} | |
| restore-keys: | | |
| lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json', 'lean-toolchain') }}- | |
| lake-${{ runner.os }}- | |
| # `lake exe cache get` pulls Mathlib oleans from Mathlib's own artifact | |
| # cache. Safe no-op on cache hit; fast (~10 s) on cache miss. | |
| - name: Get Mathlib build cache | |
| run: lake exe cache get | |
| continue-on-error: true | |
| # Incremental build: Lake re-elaborates only the files that changed in | |
| # this PR plus their transitive downstream consumers. Linter warnings | |
| # only fire for files that re-elaborate, but since all linter baselines | |
| # are 0 (no untouched-file false-positive risk), this is the right | |
| # trade-off — fast PR feedback (~30 s on warm cache) while still | |
| # catching every new violation. | |
| - name: Build OpenGALib (capture linter output) | |
| run: | | |
| set -o pipefail | |
| lake build 2>&1 | tee /tmp/build.log | |
| - name: Enforce linter baselines | |
| run: | | |
| # Each Lean linter emits a distinct warning prefix; grep + count. | |
| # Only re-elaborated files emit warnings, but the EXPECTED | |
| # constants are all 0, so any new violation in changed files | |
| # (or their transitive consumers) fails CI. | |
| MATH_TAG=$(grep -c "docstring should start with" /tmp/build.log 2>/dev/null || echo 0) | |
| ANCHOR_PURITY=$(grep -c "in an anchor file" /tmp/build.log 2>/dev/null || echo 0) | |
| NAMING=$(grep -c "forbidden initialism" /tmp/build.log 2>/dev/null || echo 0) | |
| EXPECTED_MATH_TAG=0 | |
| EXPECTED_ANCHOR_PURITY=0 | |
| EXPECTED_NAMING=0 | |
| echo "Linter baselines (re-elaborated files only):" | |
| echo " MathTag: $MATH_TAG (expected $EXPECTED_MATH_TAG)" | |
| echo " AnchorPurity: $ANCHOR_PURITY (expected ≤ $EXPECTED_ANCHOR_PURITY; gradually reduce)" | |
| echo " Naming: $NAMING (expected $EXPECTED_NAMING)" | |
| FAIL=0 | |
| if [ "$MATH_TAG" -gt "$EXPECTED_MATH_TAG" ]; then | |
| echo "::error::MathTag linter regression: $MATH_TAG > $EXPECTED_MATH_TAG" | |
| echo "Every declaration with a docstring must begin with **Math.**, **Eng.**, or **Mixed.**" | |
| FAIL=1 | |
| fi | |
| if [ "$ANCHOR_PURITY" -gt "$EXPECTED_ANCHOR_PURITY" ]; then | |
| echo "::error::AnchorPurity linter regression: $ANCHOR_PURITY > $EXPECTED_ANCHOR_PURITY" | |
| echo "Move the new Eng/Mixed declaration into the layer's Util/ sub-module," | |
| echo "or update EXPECTED_ANCHOR_PURITY only when intentionally reducing the count." | |
| FAIL=1 | |
| fi | |
| if [ "$NAMING" -gt "$EXPECTED_NAMING" ]; then | |
| echo "::error::Naming linter regression: $NAMING > $EXPECTED_NAMING" | |
| echo "Expand the initialism in the declaration name (CLM → ContinuousLinearMap, etc.)." | |
| FAIL=1 | |
| fi | |
| exit $FAIL | |
| - name: Shake — unused-import baseline | |
| run: | | |
| # `lake exe shake` flags files with unused imports (and missing | |
| # transitive-relied-on imports). Baseline is current debt; CI | |
| # fails on growth, mirrors Mathlib's `noshake.json` discipline. | |
| ACTUAL=$(lake exe shake OpenGALib --no-downstream 2>&1 | grep -c "^/.*\.lean:$" || echo 0) | |
| EXPECTED_SHAKE=38 | |
| echo "Shake suggestions: $ACTUAL (expected ≤ $EXPECTED_SHAKE; gradually reduce)" | |
| if [ "$ACTUAL" -gt "$EXPECTED_SHAKE" ]; then | |
| echo "::error::Shake regression: $ACTUAL > $EXPECTED_SHAKE" | |
| echo "Add the missing import to the consumer file, or update EXPECTED_SHAKE only when reducing." | |
| echo "Run \`lake exe shake OpenGALib --no-downstream\` locally to see the suggestions." | |
| exit 1 | |
| fi | |
| # On main push, do a full-fresh elaboration to catch any linter regressions | |
| # that the incremental build missed (e.g., a regression hiding behind a | |
| # cached olean). This is the safety net; PRs use incremental for speed. | |
| full-lint-on-main: | |
| name: Full lint baseline (main push only) | |
| if: github.event_name == 'push' && github.ref == 'refs/heads/main' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 60 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install elan | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| - name: Print Lean version | |
| run: lean --version | |
| # Restore cache so Mathlib doesn't re-download | |
| - name: Cache .lake build artifacts (Mathlib only) | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| .lake/packages | |
| key: lake-mathlib-${{ runner.os }}-${{ hashFiles('lake-manifest.json', 'lean-toolchain') }} | |
| restore-keys: | | |
| lake-mathlib-${{ runner.os }}- | |
| - name: Get Mathlib build cache | |
| run: lake exe cache get | |
| continue-on-error: true | |
| # Force fresh OpenGALib elaboration to catch every linter warning | |
| - name: Build OpenGALib from scratch | |
| run: | | |
| set -o pipefail | |
| lake build 2>&1 | tee /tmp/build.log | |
| - name: Enforce linter baselines (fresh elaboration — authoritative) | |
| run: | | |
| MATH_TAG=$(grep -c "docstring should start with" /tmp/build.log 2>/dev/null || echo 0) | |
| ANCHOR_PURITY=$(grep -c "in an anchor file" /tmp/build.log 2>/dev/null || echo 0) | |
| NAMING=$(grep -c "forbidden initialism" /tmp/build.log 2>/dev/null || echo 0) | |
| echo "Linter baselines (fresh elaboration):" | |
| echo " MathTag: $MATH_TAG" | |
| echo " AnchorPurity: $ANCHOR_PURITY" | |
| echo " Naming: $NAMING" | |
| FAIL=0 | |
| if [ "$MATH_TAG" -gt 0 ]; then echo "::error::MathTag regression: $MATH_TAG"; FAIL=1; fi | |
| if [ "$ANCHOR_PURITY" -gt 0 ]; then echo "::error::AnchorPurity regression: $ANCHOR_PURITY"; FAIL=1; fi | |
| if [ "$NAMING" -gt 0 ]; then echo "::error::Naming regression: $NAMING"; FAIL=1; fi | |
| exit $FAIL |