From 68764f53824138db7589b50a9dfd2b3dbeb29e3a Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Sat, 9 May 2026 21:34:50 +1000 Subject: [PATCH] doc: add CLAUDE.md guidance on rebasing vs changing PR base (#13652) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a short guidance note to `.claude/CLAUDE.md` clarifying that "rebase onto X" requests should only change the local branch base, never the PR's `--base` target on GitHub. The Lean4 workflow specifically uses `nightly-with-mathlib` as a rebase target to get a mathlib-tested snapshot for CI, while the PR continues to target `master`. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.7 (1M context) --- .claude/CLAUDE.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index eb1e03de83..cb2b23f45a 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -155,3 +155,9 @@ Test files (in `tests/`) do not need copyright headers. ## Test Module Docstrings Every test `.lean` file must include a module docstring (`/-! ... -/`) briefly explaining what the file tests. For regression tests, reference the issue (e.g. `#13599`). Place the docstring after the `import` block, if any. + +## Rebasing vs PR base + +When asked to "rebase a PR onto X", **only change the local branch base** — never change the PR's `--base` target on GitHub unless explicitly told to. + +Common Lean4 case: rebasing onto `nightly-with-mathlib` is done to get a mathlib-tested snapshot for CI; the PR still targets `master`.