From 061b5f4742438f9950e04c9204e321522311c3d6 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 13:22:41 -0400 Subject: [PATCH] ci: compare changed-file lints with the merge commit's first parent on PRs pull_request.base.sha is recorded when the event fires and can be an older tip of main than the base of the checked-out merge commit, so the step linted files that later main commits changed. Use the first parent, as the parallel-definition notice already does (#1057). Merge-group runs keep merge_group.base_sha. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- .github/workflows/lean_action_ci.yml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 23f4279609..b4ade72a5b 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -98,13 +98,21 @@ jobs: # Lints for the files a pull request adds or changes: names in module docstrings' "Main …" # lists exist, and a new test file does more than restate signatures. See # scripts/check_changed_files.py. The checkout is shallow, so the base commit is fetched - # and compared directly. + # and compared directly. On pull requests, as in the parallel-definition step below, the + # base is the first parent of the checked-out merge commit: `pull_request.base.sha` can be + # an older tip of `main`, and comparing with it would lint files that later commits on `main` + # changed. Merge-group runs keep `merge_group.base_sha`, which is always fetchable. - name: "Changed-file lints" if: github.event_name == 'pull_request' || github.event_name == 'merge_group' env: - BASE: ${{ github.event.pull_request.base.sha || github.event.merge_group.base_sha }} + RECORDED_BASE: ${{ github.event.pull_request.base.sha || github.event.merge_group.base_sha }} run: | set -e + BASE= + if [ "$GITHUB_EVENT_NAME" = pull_request ]; then + BASE=$(git cat-file -p HEAD | sed -n 's/^parent //p' | head -n 1) + fi + BASE=${BASE:-$RECORDED_BASE} git fetch --no-tags --depth=1 origin "$BASE" python3 -B scripts/check_changed_files.py --base "$BASE" # Advisory only: public definitions that a pull request adds or changes and that share a