name: PR benchmark

# Comment /benchmark on an open PR to compare its exact head commit with the
# snapshot committed by the latest weekly run. Only users with repository write access may
# start the expensive job. PR code executes solely in a read-only job.
on:
  issue_comment:
    types: [created]

permissions:
  contents: read
  pull-requests: read

concurrency:
  group: pr-benchmark-${{ github.event.issue.number }}
  cancel-in-progress: true

jobs:
  prepare:
    if: >-
      github.event.issue.pull_request &&
      github.event.comment.body == '/benchmark'
    runs-on: ubuntu-latest
    outputs:
      number: ${{ steps.pr.outputs.number }}
      sha: ${{ steps.pr.outputs.sha }}
      repo_url: ${{ steps.pr.outputs.repo_url }}
      base_ref: ${{ steps.pr.outputs.base_ref }}
    steps:
      - name: Resolve PR head
        id: pr
        env:
          GH_TOKEN: ${{ github.token }}
          PR_NUMBER: ${{ github.event.issue.number }}
          COMMENT_AUTHOR: ${{ github.event.comment.user.login }}
        run: |
          permission=$(gh api "repos/${GITHUB_REPOSITORY}/collaborators/${COMMENT_AUTHOR}/permission" --jq .permission)
          case "$permission" in
            admin|write) ;;
            *) echo "Only users with repository write access may run /benchmark." >&2; exit 1 ;;
          esac
          pr=$(gh api "repos/${GITHUB_REPOSITORY}/pulls/${PR_NUMBER}")
          test "$(jq -r .state <<< "$pr")" = open
          base_ref=$(jq -r .base.ref <<< "$pr")
          sha=$(jq -r .head.sha <<< "$pr")
          repo_url=$(jq -r .head.repo.clone_url <<< "$pr")
          [[ "$base_ref" =~ ^[A-Za-z0-9_./-]+$ ]]
          [[ "$sha" =~ ^[0-9a-f]{40}$ ]]
          [[ "$repo_url" =~ ^https://github\.com/[A-Za-z0-9_.-]+/[A-Za-z0-9_.-]+(\.git)?$ ]]
          echo "number=$PR_NUMBER" >> "$GITHUB_OUTPUT"
          echo "sha=$sha" >> "$GITHUB_OUTPUT"
          echo "repo_url=$repo_url" >> "$GITHUB_OUTPUT"
          echo "base_ref=$base_ref" >> "$GITHUB_OUTPUT"
          echo "Benchmarking PR #$PR_NUMBER at $sha from $repo_url"

  acknowledge:
    needs: prepare
    runs-on: ubuntu-latest
    permissions:
      issues: write
      pull-requests: write
    outputs:
      comment_id: ${{ steps.post.outputs.comment_id }}
    steps:
      - name: Post run link on PR
        id: post
        env:
          GH_TOKEN: ${{ github.token }}
          PR_NUMBER: ${{ needs.prepare.outputs.number }}
          PR_HEAD_SHA: ${{ needs.prepare.outputs.sha }}
          PR_BASE_REF: ${{ needs.prepare.outputs.base_ref }}
        run: |
          python3 - <<'PY' > comment.json
          import json
          import os
          body = (f"Benchmarking PR #{os.environ['PR_NUMBER']} at "
                  f"`{os.environ['PR_HEAD_SHA'][:12]}` against the latest committed "
                  f"weekly run. [Follow the run](https://github.com/"
                  f"{os.environ['GITHUB_REPOSITORY']}/actions/runs/"
                  f"{os.environ['GITHUB_RUN_ID']}). This comment will show the comparison when it finishes.")
          if os.environ['PR_BASE_REF'] != 'main':
              body += (f" This PR targets `{os.environ['PR_BASE_REF']}`; differences "
                       "from weekly `main` include changes on that base branch.")
          print(json.dumps({"body": body}))
          PY
          id=$(gh api --method POST "repos/${GITHUB_REPOSITORY}/issues/${PR_NUMBER}/comments" \
            --input comment.json --jq .id)
          echo "comment_id=$id" >> "$GITHUB_OUTPUT"

  status_start:
    needs: prepare
    runs-on: ubuntu-latest
    permissions:
      statuses: write
    steps:
      - name: Show benchmark in PR checks
        env:
          GH_TOKEN: ${{ github.token }}
          PR_HEAD_SHA: ${{ needs.prepare.outputs.sha }}
        run: |
          gh api --method POST "repos/${GITHUB_REPOSITORY}/statuses/${PR_HEAD_SHA}" \
            -f state=pending \
            -f context=benchmark/weekly-comparison \
            -f description='Benchmarking against the latest weekly snapshot' \
            -f target_url="https://github.com/${GITHUB_REPOSITORY}/actions/runs/${GITHUB_RUN_ID}" \
            --jq .url

  bench:
    needs: prepare
    runs-on: ubuntu-latest
    timeout-minutes: 340
    strategy:
      fail-fast: false
      matrix:
        include:
          - shard: uplc-width
            suites: UPLCWidth
          - shard: uplc-depth
            suites: UPLCDepth
          - shard: classic
            suites: NNG4,STG4,ITL4,MiniF2F,Verina
          - shard: home
            suites: BlasterHome,SmtHome,AutoHome,AesopHome,HammerHome
    permissions:
      contents: read
    env:
      Z3_VERSION: "4.15.2"
      GLIBC_Z3: "2.39"
    steps:
      - name: Free disk space
        run: |
          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \
                      /opt/hostedtoolcache/CodeQL /usr/local/share/boost || true
          df -h /

      - name: Checkout benchmarking harness
        uses: actions/checkout@v6
        with:
          repository: input-output-hk/Blaster-benchmarking
          ref: main
          path: benchmarking
          persist-credentials: false

      - name: Setup Lean (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 Z3
        run: |
          cd "$HOME"
          wget -q "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-glibc-${GLIBC_Z3}.zip"
          unzip -q "z3-${Z3_VERSION}-x64-glibc-${GLIBC_Z3}.zip"
          echo "$HOME/z3-${Z3_VERSION}-x64-glibc-${GLIBC_Z3}/bin" >> "$GITHUB_PATH"

      - name: Restore result cache
        uses: actions/cache@v4
        with:
          path: benchmarking/latest/results_cache
          key: pr-benchmark-v5-${{ needs.prepare.outputs.sha }}-${{ matrix.shard }}-${{ github.run_id }}
          restore-keys: |
            pr-benchmark-v5-${{ needs.prepare.outputs.sha }}-${{ matrix.shard }}-

      - name: Run Blaster from the PR head
        working-directory: benchmarking
        env:
          BLASTER_REPO_URL: ${{ needs.prepare.outputs.repo_url }}
          BLASTER_REF: ${{ needs.prepare.outputs.sha }}
          BENCHMARK_SUITES: ${{ matrix.suites }}
        run: bash latest/run_latest.sh blaster

      - name: Upload shard results
        if: always()
        uses: actions/upload-artifact@v6
        with:
          name: pr-benchmark-shard-${{ needs.prepare.outputs.number }}-${{ matrix.shard }}
          path: benchmarking/latest/results/
          if-no-files-found: warn

      - name: Upload shard logs
        if: always()
        uses: actions/upload-artifact@v6
        with:
          name: pr-benchmark-logs-${{ needs.prepare.outputs.number }}-${{ matrix.shard }}
          path: |
            benchmarking/latest/projects/blaster/update.log
            benchmarking/latest/projects/blaster/cache.log
            benchmarking/latest/projects/blaster/build.log
            benchmarking/latest/projects/blaster/bench.log
          if-no-files-found: warn

  compare:
    needs: [prepare, bench]
    runs-on: ubuntu-latest
    permissions:
      contents: read
    steps:
      - name: Checkout comparison script
        uses: actions/checkout@v6
        with:
          repository: input-output-hk/Blaster-benchmarking
          ref: main
          path: benchmarking
          persist-credentials: false

      - name: Checkout committed weekly snapshot
        uses: actions/checkout@v6
        with:
          ref: gh-pages
          path: weekly
          persist-credentials: false

      - name: Record baseline commit
        run: |
          test -f weekly/benchmark/snapshot.json
          echo "BASELINE_COMMIT=$(git -C weekly rev-parse HEAD)" >> "$GITHUB_ENV"

      - name: Download all shard results
        uses: actions/download-artifact@v6
        with:
          pattern: pr-benchmark-shard-${{ needs.prepare.outputs.number }}-*
          path: shards

      - name: Combine and validate shard results
        env:
          PR_NUMBER: ${{ needs.prepare.outputs.number }}
        run: python3 benchmarking/latest/merge_pr_shards.py shards combined "$PR_NUMBER"

      - name: Compare with the weekly run
        env:
          PR_NUMBER: ${{ needs.prepare.outputs.number }}
          PR_HEAD_SHA: ${{ needs.prepare.outputs.sha }}
        run: |
          python3 benchmarking/latest/compare_pr.py \
            combined weekly/benchmark/snapshot.json comparison.md
          cat comparison.md

      - name: Upload comparison and raw results
        if: always()
        uses: actions/upload-artifact@v6
        with:
          name: pr-benchmark-${{ needs.prepare.outputs.number }}
          path: |
            comparison.md
            combined/blaster/*_results.csv
            combined/manifest.tsv
          if-no-files-found: warn

  comment:
    needs: [prepare, acknowledge, compare]
    if: always() && needs.prepare.result == 'success'
    runs-on: ubuntu-latest
    permissions:
      issues: write
      pull-requests: write
    steps:
      - name: Download comparison
        if: needs.compare.result == 'success'
        uses: actions/download-artifact@v6
        with:
          name: pr-benchmark-${{ needs.prepare.outputs.number }}
          path: result

      - name: Post result on PR
        env:
          GH_TOKEN: ${{ github.token }}
          PR_NUMBER: ${{ needs.prepare.outputs.number }}
          PR_HEAD_SHA: ${{ needs.prepare.outputs.sha }}
          PR_BASE_REF: ${{ needs.prepare.outputs.base_ref }}
          BENCH_RESULT: ${{ needs.compare.result }}
          ACK_COMMENT_ID: ${{ needs.acknowledge.outputs.comment_id }}
        run: |
          if [ "$BENCH_RESULT" = success ] && [ -f result/comparison.md ]; then
            cp result/comparison.md comment.md
            if [ "$PR_BASE_REF" != main ]; then
              printf '\nThis PR targets `%s`; differences from weekly `main` include changes on that base branch.\n' \
                "$PR_BASE_REF" >> comment.md
            fi
          else
            printf 'Benchmark for PR #%s (`%.12s`) did not complete. [Inspect the run and logs](https://github.com/%s/actions/runs/%s).\n' \
              "$PR_NUMBER" "$PR_HEAD_SHA" "$GITHUB_REPOSITORY" "$GITHUB_RUN_ID" > comment.md
          fi
          python3 - <<'PY' > comment.json
          import json
          from pathlib import Path
          print(json.dumps({"body": Path("comment.md").read_text(encoding="utf-8")}))
          PY
          if [ -n "$ACK_COMMENT_ID" ]; then
            gh api --method PATCH "repos/${GITHUB_REPOSITORY}/issues/comments/${ACK_COMMENT_ID}" \
              --input comment.json --jq .html_url
          else
            gh api --method POST "repos/${GITHUB_REPOSITORY}/issues/${PR_NUMBER}/comments" \
              --input comment.json --jq .html_url
          fi

  status_finish:
    needs: [prepare, compare]
    if: always() && needs.prepare.result == 'success'
    runs-on: ubuntu-latest
    permissions:
      statuses: write
    steps:
      - name: Update PR benchmark check
        env:
          GH_TOKEN: ${{ github.token }}
          PR_HEAD_SHA: ${{ needs.prepare.outputs.sha }}
          BENCH_RESULT: ${{ needs.compare.result }}
        run: |
          if [ "$BENCH_RESULT" = success ]; then
            state=success
            description='Benchmark comparison completed; see run and artifact'
          else
            state=failure
            description='Benchmark did not complete; inspect the run logs'
          fi
          gh api --method POST "repos/${GITHUB_REPOSITORY}/statuses/${PR_HEAD_SHA}" \
            -f state="$state" \
            -f context=benchmark/weekly-comparison \
            -f description="$description" \
            -f target_url="https://github.com/${GITHUB_REPOSITORY}/actions/runs/${GITHUB_RUN_ID}" \
            --jq .url