ci.yml

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=32
          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

      - 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') }}
          restore-keys: |
            lake-${{ runner.os }}-

      - name: Get Mathlib build cache
        run: lake exe cache get
        continue-on-error: true

      - name: Force fresh OpenGALib elaboration (preserves Mathlib cache)
        # Lean linters only fire during elaboration; cached `.olean` files
        # skip them. Removing OpenGALib's build outputs forces re-elaboration
        # so all linter warnings reach `/tmp/build.log` for the baseline check.
        # Mathlib outputs in `.lake/build/lib/lean/Mathlib/…` are untouched.
        run: rm -rf .lake/build/lib/lean/OpenGALib .lake/build/ir/OpenGALib

      - 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.
          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:"
          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=35
          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