name: Auto Pipeline — Extract → DB → RRC

on:
  push:
    paths:
      - '0-Core-Formalism/lean/**/*.lean'
      - '2-Search-Space/PIST/**/*.lean'
  workflow_dispatch:

env:
  NEON_HOST: 100.92.88.64
  PG_USER: postgres
  PG_PASS: postgres

jobs:
  pipeline:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Set up Lean
        uses: leanprover/lean-action@v1
        with:
          working-directory: 0-Core-Formalism/lean/Semantics

      - name: Build Compiler target
        run: |
          cd 0-Core-Formalism/lean/Semantics
          lake build Compiler

      - name: Extract theorem metadata
        run: |
          python3 scripts/auto/auto_pipeline.py --ci

      - name: Populate ENE database
        run: |
          psql "${{ secrets.NEON_PG_URL }}" -f scripts/auto/ene_schema.sql
          python3 scripts/auto/populate_ene_tables.py
        env:
          PGPASSWORD: ${{ secrets.PG_PASS }}