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) <noreply@anthropic.com>
This PR removes the Makefile-based Lake test runner and replaces it with
`run_test.sh` and `run_clean.sh`. These are still not designed for use
with the `with_*.sh` runners, but this a step closer to that
eventuality.
It also adds a line to `CLAUDE.md` informing Claude how to build and run
a single Lake test.
Previously, `elabInitialize` only checked for explicit `private` when
deciding whether to mangle `fullId`, ignoring the `module` system's
default-private semantics. It also overrode the user's visibility for
the generated `initFn` via `visibility.ofBool`.
Now, `elabInitialize` uses `elabVisibility` + `isInferredPublic` to
correctly handle all visibility contexts. The generated `initFn`
inherits the user's visibility rather than being forced public.
Also factors out `elabVisibility` from `elabModifiers` for reuse.
This PR adds two safety notes to the Claude Code release command:
- Mathlib bump branches live on `mathlib4-nightly-testing`, not the main
`mathlib4` repo
- Never force-update remote refs without explicit user confirmation
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR speeds up some benchmarks when run as tests by lowering their
workload. It also stops testing some of the more expensive benchmarks
that can't be easily made smaller.
The tests need to run with certain environment variables set that only
cmake really knows and that differ between stages. Cmake could just set
the variables directly when running the tests and benchmarks, but that
would leave no good way to manually run a single benchmark. So cmake
generates some stage-specific scripts instead that set the required
environment variables.
Previously, those scripts were sourced directly by the individual
`run_*` scripts, so the env scripts of different stages would overwrite
each other. This PR changes the setup so they can instead be generated
next to each other. This also simplifies the `run_*` scripts themselves
a bit, and makes `tests/bench/build` less of a hack.
This PR fixes `release_checklist.py` to report failing CI checks
immediately, even when other checks are still in progress. Previously,
having any in-progress checks would return `"pending"` status, masking
failures that had already occurred. Now it returns `"failure"` with a
message like `"1 check(s) failing, 2 still in progress"`.
Also adds a section to `.claude/commands/release.md` instructing the AI
assistant to investigate any CI failure immediately rather than
reporting it as "in progress" and moving on.
🤖 Prepared with Claude Code
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR fixes a CMake scoping bug that made `-DLEAN_VERSION_*` overrides
ineffective.
The version variables (`LEAN_VERSION_MAJOR`, `MINOR`, `PATCH`,
`IS_RELEASE`) were declared with plain `set()`, which creates normal
variables that shadow cache variables set by `-D` on the command line.
The fix changes them to `CACHE STRING ""` to match the existing
`LEAN_SPECIAL_VERSION_DESC` pattern.
However, `CACHE STRING ""` alone isn't sufficient because `project(LEAN
CXX C)` implicitly creates empty `LEAN_VERSION_{MAJOR,MINOR,PATCH}`
normal variables (CMake sets `<PROJECT>_VERSION_*` for the project
name). These shadow the cache values, so we `unset()` them after the
cache declarations to let `${VAR}` fall through to the cache.
Closes https://github.com/leanprover/lean4/issues/12681🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a section to the /release command explaining how to use `gh
pr checks --watch` to wait for CI or merges without polling.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR changes the shebang in `lean_profile.sh` from `#!/bin/bash` to
`#!/usr/bin/env bash` so the script works on NixOS and other systems
where bash is not at `/bin/bash`, and adds a Claude Code skill pointing
to the profiler documentation.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR sets up the new integrated test/bench suite. It then migrates
all benchmarks and some related tests to the new suite. There's also
some documentation and some linting.
For now, a lot of the old tests are left alone so this PR doesn't become
even larger than it already is. Eventually, all tests should be migrated
to the new suite though so there isn't a confusing mix of two systems.
This PR updates the CLAUDE.md instructions to better conform with our PR
conventions. Specifically, it clarifies that PR bodies must start with
"This PR" (which gets incorporated into release notes), and that
markdown headings like `## Summary` or `## Test plan` should not be used
in PR descriptions.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR registers the
[leanprover/skills](https://github.com/leanprover/skills) plugin
marketplace in `.claude/settings.json` so that Claude Code users working
on lean4 are automatically prompted to install it.
Also un-ignores `.claude/settings.json` in `.gitignore` — the blanket
`settings.json` rule was blocking it from being tracked.
🤖 Prepared with Claude Code
This PR adds guidance to `.claude/CLAUDE.md` about the `module` +
`prelude` convention required for files in `src/Lean/`, `src/Std/`, and
`src/lake/Lake/`. CI enforces that these files contain `prelude`, but
with `prelude` nothing is auto-imported, so explicit `Init.*` imports
are needed for standard library features like `while`,
`String.startsWith`, etc.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a "Copyright Headers" section to `.claude/CLAUDE.md`
instructing Claude to:
- Always use `date +%Y` for the copyright year instead of relying on
memory
- Match the copyright holder to what the author uses in other recent
files in the repo
- Skip copyright headers for test files in `tests/`
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds guidance to the release slash command to check actual PR
merge state (using `gh pr view`) when reporting status, rather than
relying on cached CI results. This prevents incorrectly reporting
already-merged PRs as still needing review.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds comprehensive test running instructions to
`.claude/CLAUDE.md`,
replacing the single `test_single.sh` example with the full range of
test
commands documented in `doc/dev/testing.md`: full suite, filtered by
name,
rerun failures, and direct ctest usage.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR documents the available `changelog-*` labels and when to use
them in the project-specific CLAUDE.md instructions.
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR documents the release notes writing process in detail and adds a
guard check to `release_checklist.py` to ensure release notes are
created for `-rc1` releases before proceeding with downstream repository
updates.
- **doc/dev/release_checklist.md**: Expanded "Writing the release notes"
section with detailed steps for generating, reviewing, and formatting
release notes in Verso format
- **script/release_checklist.py**: Added
`check_release_notes_file_exists()` to verify the release notes file
exists in reference-manual repository
- **.claude/commands/release.md**: Added "Release Notes" section
explaining the process for creating release notes during `-rc1` releases
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds documentation about the nightly build infrastructure to the
`/release` command to help future release managers understand the
relationship between branches and tags:
- `nightly` and `nightly-with-mathlib` are **branches** in
`leanprover/lean4`
- Dated tags like `nightly-YYYY-MM-DD` are **tags** in
`leanprover/lean4-nightly`
- When a nightly succeeds with mathlib, all three should point to the
same commit
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds guidance for investigating CI failures promptly rather than
waiting for other jobs to complete.
---
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR expands the pull request creation section with detailed
formatting guidelines including title format (type prefixes, imperative
present tense) and body format requirements (starting with "This PR").
Adds a concrete example for reference.
All modifications were suggested by Claude.
This PR adds explicit guidance to the `/release` command that Claude
should never merge PRs autonomously during the release process - always
wait for the user to do it.
🤖 Prepared with Claude Code
This PR improves the release automation. We link to CI output for
building the release tag, don't give instructions for bumping downstream
repositories until the release it ready, and improve documentation and
prompts.
This PR improves the scripts assisting with cutting Lean releases (by
reporting CI status of open PRs, and adding documentation), and adds a
`.claude/commands/release.md` prompt file so Claude can assist.
