Skip to content

fix: select PR CI changes from the merge base - #644

Merged
kim-em merged 2 commits into
mainfrom
fix/pr-ci-merge-base
Sep 24, 2026
Merged

kim-em merged 2 commits into
mainfrom
fix/pr-ci-merge-base

Conversation

@kim-em

@kim-em kim-em commented Sep 23, 2026

Copy link
Copy Markdown
Collaborator

Summary

Select pull-request CI work from the PR merge base, rather than diffing the current main tip directly against the contributor head. The direct tip-to-tip diff treated changes that landed only on main as PR changes.

PR #643 illustrates the failure: its visible diff adds only a Lean module and manifest, but its CI selector reported .github/workflows/ci.yml, lake-manifest.json, lakefile.toml, and lean-toolchain as full-catalog sentinels. It also classified main-only generated/ changes as part of the PR, ran the generated-index check, and failed with stale generated/index.json even though all eight catalog shards passed.

Push-to-main selection remains unchanged. A regression test creates diverged branches and verifies that PR selection excludes base-only changes.

Validation

  • PYTHONDONTWRITEBYTECODE=1 python -m unittest discover -s tests/python -p 'test_*.py' — 36 tests passed.
  • python -m py_compile scripts/select_ci_problems.py tests/python/test_select_ci_problems.py — passed.
  • git diff --check — passed.

@kim-em
kim-em merged commit 04ddd7c into main Sep 24, 2026
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant