ci.yml

name: CI

on:
  push:
    branches: [main]
  pull_request:
    branches: [main]

env:
  ELAN_NO_OVERRIDE_NOTICE: 1

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout
        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: Install and activate toolchain
        run: |
          elan toolchain install $(cat lean-toolchain)
          elan override set $(cat lean-toolchain)
          lake --version

      - name: Cache .lake
        uses: actions/cache@v4
        with:
          path: .lake
          key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('Linglib/**/*.lean', 'Linglib.lean') }}
          restore-keys: |
            lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-

      - name: Get Mathlib cache
        run: lake exe cache get

      - name: Build
        run: lake build

      - name: Check for sorries (informational)
        run: |
          echo "=== Files with sorry ==="
          grep -r "sorry" Linglib/ --include="*.lean" | grep -v "-- " | head -50 || echo "No sorries found"