Skip to content

Commit e4e4fc2

Browse files
ci(olean_report): fetch PR oleans from fork's cache (leanprover-community#38894)
Fixes an issue noticed in [this comment](leanprover-community#38653 (comment)) where the olean report said that 5066 modules were removed from a PR that only added `to_dual` tags. The issue is that the `olean_report` workflow only fetched oleans from the `leanprover-community/mathlib4` cache and not the fork cache. We fix this by also fetching the head repo name from `gh pr view --json headRepository` and re-running `cache get --repo=<head_repo>`, mirroring what `build_template.yml` already does for regular CI. Prepared with Claude code.
1 parent 24a0d31 commit e4e4fc2

1 file changed

Lines changed: 5 additions & 1 deletion

File tree

.github/workflows/olean_report.yaml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,11 +69,12 @@ jobs:
6969
run: |
7070
pr_json=$(gh pr view "${{ github.event.issue.number }}" \
7171
--repo "${{ github.repository }}" \
72-
--json headRefOid,baseRefOid,baseRefName)
72+
--json headRefOid,baseRefOid,baseRefName,headRepository)
7373
{
7474
echo "head_sha=$(echo "$pr_json" | jq -r '.headRefOid')"
7575
echo "base_sha=$(echo "$pr_json" | jq -r '.baseRefOid')"
7676
echo "base_ref=$(echo "$pr_json" | jq -r '.baseRefName')"
77+
echo "head_repo=$(echo "$pr_json" | jq -r '.headRepository.nameWithOwner')"
7778
} >> "$GITHUB_OUTPUT"
7879
7980
# Using refs/pull/N/head works for both same-repo and fork PRs, since
@@ -175,6 +176,9 @@ jobs:
175176
run: |
176177
cd pr-branch
177178
lake env "$CACHE_BIN" get
179+
# Run again with --repo in case this is a fork PR: fork PRs upload
180+
# their oleans to the fork's Azure container, not the upstream one.
181+
lake env "$CACHE_BIN" --repo="${{ steps.pr_info.outputs.head_repo }}" get
178182
179183
- name: Check PR head oleans
180184
id: pr_oleans_check

0 commit comments

Comments
 (0)