regenerate-main.yml

# Auth and bypass for this workflow are documented in docs/ci-secrets.md
# (`lean-eval-regenerator` GitHub App + Repository Ruleset bypass list).
name: Regenerate generated/ on main

on:
  push:
    branches: [main]
    paths:
      - 'LeanEval/**'
      - 'EvalTools/**'
      - 'manifests/problems.toml'
      - 'scripts/generate_projects.py'
      - 'lakefile.toml'
      - 'lean-toolchain'
  workflow_dispatch:

permissions:
  contents: read

concurrency:
  group: regenerate-main
  cancel-in-progress: false

jobs:
  regenerate:
    runs-on: ubuntu-latest
    steps:
      - name: Mint lean-eval-regenerator installation token
        id: app_token
        # actions/create-github-app-token pinned to d72941d7 (= refs/tags/v1 as of 2026-05-04).
        uses: actions/create-github-app-token@d72941d797fd3113feb6b93fd0dec494b13a2547
        with:
          app-id: ${{ secrets.LEAN_EVAL_REGENERATOR_APP_ID }}
          private-key: ${{ secrets.LEAN_EVAL_REGENERATOR_PRIVATE_KEY }}

      # actions/checkout pinned to 11bd7190 (= refs/tags/v4.2.2 as of 2026-05-04).
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
        with:
          fetch-depth: 0
          token: ${{ steps.app_token.outputs.token }}

      # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          use-mathlib-cache: true

      - name: Re-sync to latest origin/main
        # Codex finding: regenerate against the freshest source, not whatever
        # the runner cloned. A merge can land on main between the trigger and
        # the checkout above; without this, we'd regenerate against stale
        # source and then push a result that doesn't match HEAD.
        run: |
          set -euo pipefail
          git fetch origin main
          git reset --hard origin/main

      - name: Regenerate
        run: python scripts/generate_projects.py

      - name: Commit and push if changed
        run: |
          set -euo pipefail
          if git diff --quiet generated/ \
             && [ -z "$(git ls-files --others --exclude-standard generated/)" ]; then
            echo "No changes to generated/."
            exit 0
          fi
          git config user.name  "lean-eval-regenerator[bot]"
          git config user.email "lean-eval-regenerator[bot]@users.noreply.github.com"
          git add generated/
          git commit -m "chore: regenerate generated/ workspaces"
          # Retry once if a human commit landed during this run.
          if ! git push origin HEAD:main; then
            echo "push rejected; rebasing onto latest main and retrying"
            git pull --rebase origin main
            git push origin HEAD:main
          fi