name: CI

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

jobs:
  lint:
    name: Lint (ruff)
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: actions/setup-python@v5
        with:
          python-version: "3.12"
      - name: Install ruff
        # Pinned so CI and local runs use the same rule set (ruff's import
        # sorting changes between releases).
        run: pip install ruff==0.15.14
      - name: ruff check
        run: ruff check .

  test:
    name: Test (pytest)
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: actions/setup-python@v5
        with:
          python-version: "3.12"
          cache: pip
      - name: Install dependencies
        run: |
          python -m pip install --upgrade pip
          pip install -r requirements.txt
          pip install pytest
      - name: Run pytest
        # The 3 real-Lean tests in test_lean_verifier.py self-skip when no
        # `lean` toolchain is on PATH (CI runners have none); the other ~95
        # tests use mocks and run everywhere.
        run: pytest tests/ -v

  deploy:
    name: Deploy to Hugging Face Spaces
    needs: [lint, test]
    # Only deploy on a real push to main — never on pull requests.
    if: github.ref == 'refs/heads/main' && github.event_name == 'push'
    runs-on: ubuntu-latest
    steps:
      - name: Check HF_TOKEN is configured
        id: gate
        run: |
          if [ -n "${{ secrets.HF_TOKEN }}" ]; then
            echo "ok=true" >> "$GITHUB_OUTPUT"
          else
            echo "ok=false" >> "$GITHUB_OUTPUT"
            echo "::notice::HF_TOKEN secret not set — skipping Hugging Face Spaces deploy."
          fi
      - name: Checkout (with Git LFS)
        if: steps.gate.outputs.ok == 'true'
        uses: actions/checkout@v4
        with:
          lfs: true
          fetch-depth: 0
      - name: Push to Hugging Face Spaces
        if: steps.gate.outputs.ok == 'true'
        run: |
          git push --force \
            "https://Ray5th:${{ secrets.HF_TOKEN }}@huggingface.co/spaces/Ray5th/lean4-helper" \
            HEAD:main