# CI workflow for SGC Lean 4 formalization
# Triggers on push to main and pull requests
# Uses leanprover/lean-action for reproducible Lean builds

name: Build

on:
  push:
    branches: [ main, master, dev, wip-* ]
  pull_request:
    branches: [ main, master ]

# Cancel in-progress runs for the same branch
concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  build:
    runs-on: ubuntu-latest
    
    steps:
    - name: Checkout repository
      uses: actions/checkout@v4
      with:
        # Disable submodule handling to avoid issues with .lake/packages
        submodules: false
    
    - 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: Get Mathlib cache
      run: |
        # Install lake if needed and get mathlib cache
        lake exe cache get || true
    
    - name: Build SGC
      run: lake build
    
    - name: Verify no sorries
      run: |
        set -e
        echo "Checking for 'sorry' in source files..."
        
        # Search for sorry as a standalone word (the tactic), excluding:
        # - Comment lines (starting with --)
        # - Docstrings (/-- ... -/)
        # - Backticked references (`sorry`) in documentation
        # - Meta-references about verification status
        SORRY_COUNT=$(grep -rn --include="*.lean" -E '\bsorry\b' src/ \
          | grep -v '^\s*--' \
          | grep -v '/--' \
          | grep -v '`sorry`' \
          | grep -v 'sorry-free' \
          | grep -v 'zero.*sorry' \
          | grep -v 'unproven' \
          | wc -l || true)
        
        if [ "$SORRY_COUNT" -gt 0 ]; then
          echo "Found $SORRY_COUNT potential 'sorry' occurrences:"
          grep -rn --include="*.lean" -E '\bsorry\b' src/ \
            | grep -v '^\s*--' \
            | grep -v '/--' \
            | grep -v '`sorry`' \
            | grep -v 'sorry-free' \
            | grep -v 'zero.*sorry' \
            | grep -v 'unproven' || true
          
          # Only fail on main/master branches, warn on dev branches
          BRANCH_NAME="${GITHUB_REF#refs/heads/}"
          if [[ "$BRANCH_NAME" == "main" || "$BRANCH_NAME" == "master" ]]; then
            echo "::error::Sorries not allowed on $BRANCH_NAME branch"
            exit 1
          else
            echo "::warning::$SORRY_COUNT sorries found - allowed on $BRANCH_NAME branch (WIP)"
          fi
        else
          echo "✓ No active sorries found (verified)"
        fi
    
    - name: Post-job Cleanup
      if: always()
      run: |
        echo "Cleaning up build artifacts..."
        
        # 1. Force delete .lake (handle read-only git objects)
        if [ -d ".lake" ]; then
           chmod -R 777 .lake
           rm -rf .lake
           echo "✓ .lake directory deleted."
        fi

        # 2. Remove the .git directory
        # This prevents the 'actions/checkout' post-run step from trying
        # to scan for submodules in a directory we just confused.
        if [ -d ".git" ]; then
           rm -rf .git
           echo "✓ .git directory deleted (preventing post-job git hooks)."
        fi