Skip to content

Benchmark fork PRs: name the head repository at checkout #387

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sgerbino merged 1 commit into from
Oct 7, 2026
Merged

Benchmark fork PRs: name the head repository at checkout #387

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions .github/workflows/benchmarks.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ jobs:
pull-requests: write
outputs:
head_sha: ${{ steps.decide.outputs.head_sha }}
head_repo: ${{ steps.decide.outputs.head_repo }}
base_sha: ${{ steps.decide.outputs.base_sha }}
tools_sha: ${{ steps.decide.outputs.tools_sha }}
pr: ${{ steps.decide.outputs.pr }}
Expand All @@ -72,6 +73,15 @@ jobs:
BASE_REF: ${{ github.event.pull_request.base.ref }}
run: |
set -e
# The repo the head commit lives in: the base repo except for
# fork PRs, whose commits exist only in the fork. The bench
# jobs pass it to checkout explicitly — actions/checkout
# refuses to fetch fork code from a pull_request_target
# workflow unless the fork is named, and naming it is safe
# here: the gate pins head_sha at label time, the label is a
# maintainer's approval to run that code on these machines,
# and the checkout keeps no credentials.
head_repo="${{ github.repository }}"
# Resolve head/base entirely via the API (no checkout needed).
# PR events compare against the PR's base branch; dispatch
# compares against develop and can also validate A/A (base vs itself).
Expand Down Expand Up @@ -132,6 +142,7 @@ jobs:
fi
echo "run=$run" >> "$GITHUB_OUTPUT"
head_sha="${{ github.event.pull_request.head.sha }}"
head_repo="${{ github.event.pull_request.head.repo.full_name }}"
base_sha=$(gh api "repos/${{ github.repository }}/compare/${BASE_REF}...${head_sha}" \
--jq .merge_base_commit.sha)
# pull_request_target runs workflow + job steps from the base
Expand All @@ -156,6 +167,7 @@ jobs:
echo "mode=${{ inputs.mode }}" >> "$GITHUB_OUTPUT"
fi
echo "head_sha=$head_sha" >> "$GITHUB_OUTPUT"
echo "head_repo=$head_repo" >> "$GITHUB_OUTPUT"
echo "base_sha=$base_sha" >> "$GITHUB_OUTPUT"
echo "tools_sha=$tools_sha" >> "$GITHUB_OUTPUT"
Expand Down Expand Up @@ -192,6 +204,7 @@ jobs:
- name: Checkout head
uses: actions/checkout@v4
with:
repository: ${{ needs.gate.outputs.head_repo }}
ref: ${{ needs.gate.outputs.head_sha }}
path: ws/head
persist-credentials: false
Expand Down
Loading