This PR replaces `find -print0 | xargs -0 -I{} sh -c '...'` with
`find -print0 | while IFS= read -r -d '' f; do ... done` for the
subverso sub-manifest sync in release_steps.py. The original xargs
invocation had fragile nested shell quoting; the while-read loop is
both null-delimiter safe and more readable.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR replaces three independent name demangling implementations
(Lean, C++, Python) with a single source of truth in
`Lean.Compiler.NameDemangling`. The new module handles the full
pipeline: prefix parsing (`l_`, `lp_`, `_init_`, `initialize_`,
`lean_apply_N`, `_lean_main`), postprocessing (suffix flags, private
name stripping, hygienic suffix stripping, specialization contexts),
backtrace line parsing, and C exports via `@[export]`.
The C++ runtime backtrace handler now calls the Lean-exported functions
instead of its own 792-line reimplementation. This is safe because
`print_backtrace` is only called from `lean_panic_impl` (soft panics),
not `lean_internal_panic`.
The Python profiler demangler (`script/profiler/lean_demangle.py`) is
replaced with a thin subprocess wrapper around a Lean CLI tool,
preserving the `demangle_lean_name` API so downstream scripts work
unchanged.
**New files:**
- `src/Lean/Compiler/NameDemangling.lean` — single source of truth (483
lines)
- `tests/lean/run/demangling.lean` — comprehensive tests (281 lines)
- `script/profiler/lean_demangle_cli.lean` — `c++filt`-style CLI tool
**Deleted files:**
- `src/runtime/demangle.cpp` (792 lines)
- `src/runtime/demangle.h` (26 lines)
- `script/profiler/test_demangle.py` (670 lines)
Net: −1,381 lines of duplicated C++/Python code.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a false positive in `release_checklist.py` where the check
for the dev cycle being started would fail even when it was correctly
set up.
The script was looking for `set(LEAN_VERSION_IS_RELEASE 0)` as an exact
prefix match, but CMakeLists.txt uses the CMake cache variable form:
`set(LEAN_VERSION_IS_RELEASE 0 CACHE STRING "")`. The fix uses a regex
that handles both syntaxes.
This was discovered during the v4.29.0-rc4 release when the checklist
incorrectly reported that a "begin dev cycle" PR was needed, even though
PR #12526 had already set `LEAN_VERSION_IS_RELEASE 0` and
`LEAN_VERSION_MINOR 30` on master.
🤖 Prepared with Claude Code
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR fixes `release_steps.py` for `verso`. After running `lake
update` in the root, the `test-projects/*/lake-manifest.json` files
retain stale subverso pins, causing verso's "SubVerso version
consistency" CI check to fail. The fix syncs the root manifest's
subverso rev into all test-project sub-manifests.
Root cause: verso has nested Lake projects in `test-projects/` each with
their own `lake-manifest.json`. Running `lake update` in the root
updates the root manifest but doesn't touch the nested ones.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
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 parsing bug in \`release_checklist.py\` introduced by
https://github.com/leanprover/lean4/pull/12700, which reformatted
\`src/CMakeLists.txt\` to use \`CACHE STRING \"\"\`:
\`\`\`cmake
set(LEAN_VERSION_MINOR 30 CACHE STRING "")
\`\`\`
The old code used \`split()[-1].rstrip(")")\` to extract the version
number, which now yields \`""\` (the empty string argument) instead of
the minor version. Use a regex to extract the digit directly.
🤖 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>
MacOS uses a very old version of bash where `"${FOO[@]}"` fails if `set
-u` is enabled and `FOO` is undefined. Newer versions of bash expand
this to zero arguments instead.
Also, `lint.py` used the shebang `#!/usr/bin/env python` instead of
`python3`, which fails on some systems.
In CI, all macos tests run on nscloud runners. Presumably, they have
installed newer versions of various software, hence this didn't break in
CI.
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 changes all `lean-toolchain` to use relative toolchain paths
instead of `lean4` and `lean4-stage0` identifiers, which removes the
need for manually linking toolchains via Elan.
After this PR, at least Elan 4.2.0 and 0.0.224 of the Lean VS Code
extension will be needed to edit core.
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR removes the batteries dependency from ProofWidgets4 in
`release_repos.yml`. ProofWidgets4 no longer has any `require`
statements in its lakefile, so it doesn't depend on batteries.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds tooling for profiling Lean programs with human-readable
function names in Firefox Profiler:
- **`script/lean_profile.sh`** — One-command pipeline: record with
samply, symbolicate, demangle, and open in Firefox Profiler
- **`script/profiler/lean_demangle.py`** — Faithful port of
`Name.demangleAux` from `NameMangling.lean`, with a postprocessor that
folds compiler suffixes into compact annotations (`[λ, arity↓]`, `spec
at context[flags]`)
- **`script/profiler/symbolicate_profile.py`** — Resolves raw addresses
via samply's symbolication API
- **`script/profiler/serve_profile.py`** — Serves demangled profiles to
Firefox Profiler without re-symbolication
- **`PROFILER_README.md`** — Documentation including a guide to reading
demangled names
### Example output in Firefox Profiler
| Raw C symbol | Demangled |
|---|---|
| `l_Lean_Meta_Sym_main` | `Lean.Meta.Sym.main` |
| `l_Lean_Meta_foo___redArg___lam__0` | `Lean.Meta.foo [λ, arity↓]` |
| `l_Lean_MVarId_withContext___at__...___spec__2___boxed` |
`Lean.MVarId.withContext [boxed] spec at Lean.Meta.bar[λ, arity↓]` |
Example:
<img width="1145" height="570" alt="image"
src="https://github.com/user-attachments/assets/8d23cc6a-1b89-4c60-9f4a-9f9f0f6e7697"
/>
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a release workflow bug where the reference-manual
repository would get tagged with a stale release notes title (e.g.,
still showing "-rc1" for a stable release).
The root cause was a sequencing issue: `release_steps.py` didn't update
the release notes title when bumping the reference-manual toolchain, and
`release_checklist.py` only checked the title while the bump PR was
open. Once merged, it went straight to tagging without rechecking.
Two fixes:
- `release_checklist.py`: add a title correctness check before tagging
reference-manual (blocks tagging if the title is wrong)
- `release_steps.py`: automatically update the `#doc` title line in the
release notes file when bumping reference-manual (handles both
RC-to-stable and RC-to-RC transitions)
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds automatic ProofWidgets4 version pin updates to
`release_steps.py` when processing mathlib4. ProofWidgets4 uses
sequential version tags (`v0.0.X`) rather than toolchain-based tags
(`v4.X.Y`), so the existing regex that updates dependency versions in
lakefiles doesn't match it. This has caused CI failures in two
consecutive releases where the mathlib4 PR was created with a stale
ProofWidgets4 pin.
Changes:
- `script/release_steps.py`: Add `find_proofwidgets_tag()` to look up
the latest ProofWidgets4 tag compatible with the target toolchain, and
use it to update mathlib4's lakefile automatically
- `doc/dev/release_checklist.md`: Document the ProofWidgets4 pin update
step for mathlib4
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds support for manually re-releasing nightlies when a build
issue or critical fix requires it. When a `workflow_dispatch` triggers
the nightly release job and a `nightly-YYYY-MM-DD` tag already exists,
the CI now creates `nightly-YYYY-MM-DD-rev1` (then `-rev2`, etc.)
instead of silently skipping.
### Lake `ToolchainVer`
- Extend `ToolchainVer.nightly` with an optional `rev : Option Nat`
field
- Parse `-revK` suffixes from nightly tags in `ofString`
- Ordering: `nightly-YYYY-MM-DD` < `nightly-YYYY-MM-DD-rev1` < `-rev2` <
`nightly-YYYY-MM-DD+1`
- Round-trip: `toString (ofString s) == s` for both variants
### CI workflow
- "Set Nightly" step probes existing tags on `workflow_dispatch` to find
next available `-revK`
- Scheduled nightlies retain existing behavior (skip if commit already
tagged)
- Changelog grep updated from `nightly-[-0-9]*` to `nightly-[^ ,)]*` to
match `-revK` suffixes
### `lean-bisect`
- Updated `NIGHTLY_PATTERN` regex, sort key, error messages, and help
text
### Companion PRs
- https://github.com/leanprover-community/mathlib4/pull/35220: update
`nightly_bump_and_merge.yml` tag grep and `nightly_detect_failure.yml`
warning message
-
https://github.com/leanprover-community/leanprover-community.github.io/pull/787:
update `tags_and_branches.md` documentation
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <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>
verso depends on plausible, but this wasn't recorded in
release_repos.yml. This caused the release checklist to not properly
track the dependency ordering.
This PR adds a check to the release checklist script that verifies the
reference-manual release notes title matches the release type:
- For RC releases (e.g., v4.27.0-rc1): verifies the title contains the
exact
RC suffix (e.g., "Lean 4.27.0-rc1")
- For final releases (e.g., v4.27.0): verifies the title does NOT
contain
any "-rc" suffix (e.g., "Lean 4.27.0")
The check looks at the PR branch (bump_to_vX.Y.Z) for the release notes
file
at `Manual/Releases/v4_X_Y.lean` and parses the `#doc (Manual) "Lean
..."` line.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds `lake shake` as a built-in Lake command, moving the shake
functionality from `script/Shake.lean` into the Lake CLI.
## Motivation
Per discussion with @Kha and @tydeu, having shake as a top-level Lake
command is preferable to `lake exe shake` because:
- Avoids the awkwardness of accessing core tools via `lake exe`
- Compiles shake into the Lake binary, avoiding lakefile issues
- No benefit to lazy compilation on user machines for this tool
## Changes
- Move shake logic from `script/Shake.lean` to
`src/lake/Lake/CLI/Shake.lean`
- Add `lake shake` command dispatch in `Lake/CLI/Main.lean`
- Add help text in `Lake/CLI/Help.lean`
- Remove the standalone shake executable from `script/lakefile.toml`
## Usage
```
lake shake [OPTIONS] [<MODULE>...]
```
See `lake shake --help` for full documentation.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR adds a Python script that helps find which commit introduced a
behavior change in Lean. It supports multiple bisection modes and
automatically downloads CI artifacts when available.
- [x] depends on: #11735
## Usage
```
usage: lean-bisect [-h] [--timeout SEC] [--ignore-messages] [--verbose]
[--selftest] [--clear-cache] [--nightly-only]
[file] [RANGE]
Bisect Lean toolchain versions to find where behavior changes.
positional arguments:
file Lean file to test (must only import Lean.* or Std.*)
RANGE Range to bisect: FROM..TO, FROM, or ..TO
options:
-h, --help show this help message and exit
--timeout SEC Timeout in seconds for each test run
--ignore-messages Compare only exit codes, ignore stdout/stderr differences
--verbose, -v Show stdout/stderr from each test
--selftest Run built-in selftest to verify lean-bisect works
--clear-cache Clear CI artifact cache (~600MB per commit) and exit
--nightly-only Stop after finding nightly range (don't bisect individual
commits)
Range Syntax:
FROM..TO Bisect between FROM and TO
FROM Start from FROM, bisect to latest nightly
..TO Bisect to TO, search backwards for regression start
If no range given, searches backwards from latest nightly to find regression.
Identifier Formats:
nightly-YYYY-MM-DD Nightly build date (e.g., nightly-2024-06-15)
Uses pre-built toolchains from leanprover/lean4-nightly.
Fast: downloads via elan (~30s each).
v4.X.Y or v4.X.Y-rcN Version tag (e.g., v4.8.0, v4.9.0-rc1)
Converts to equivalent nightly range.
Commit SHA Git commit hash (short or full, e.g., abc123def)
Bisects individual commits between two points.
Tries CI artifacts first (~30s), falls back to building (~2-5min).
Commits with failed CI builds are automatically skipped.
Artifacts cached in ~/.cache/lean-bisect/artifacts/
Bisection Modes:
Nightly mode: Both endpoints are nightly dates.
Binary search through nightlies to find the day behavior changed.
Then automatically continues to bisect individual commits.
Use --nightly-only to stop after finding the nightly range.
Version mode: Either endpoint is a version tag.
Converts to equivalent nightly range and bisects.
Commit mode: Both endpoints are commit SHAs.
Binary search through individual commits on master.
Output: "Behavior change introduced in commit abc123"
Examples:
# Simplest: just provide the file, finds the regression automatically
lean-bisect test.lean
# Specify an endpoint if you know roughly when it broke
lean-bisect test.lean ..nightly-2024-06-01
# Full manual control over the range
lean-bisect test.lean nightly-2024-01-01..nightly-2024-06-01
# Only find the nightly range, don't continue to commit bisection
lean-bisect test.lean nightly-2024-01-01..nightly-2024-06-01 --nightly-only
# Add a timeout (kills slow/hanging tests)
lean-bisect test.lean --timeout 30
# Bisect commits directly (if you already know the commit range)
lean-bisect test.lean abc1234..def5678
# Only compare exit codes, ignore output differences
lean-bisect test.lean --ignore-messages
# Clear downloaded CI artifacts to free disk space
lean-bisect --clear-cache
```
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds a standalone script to download pre-built CI artifacts from
GitHub Actions. This allows us to quickly switch commits without
rebuilding.
**Features:**
- Downloads artifacts for current HEAD or specified commit (`--sha`)
- Caches in `~/.cache/lean_build_artifact/` for reuse
- Platform detection (Linux/macOS, x86_64/aarch64)
**Usage:**
```
build_artifact.py # Download for current HEAD
build_artifact.py --sha abc1234 # Download for specific commit
build_artifact.py --clear-cache # Clear cache
```
This is extracted to be shared with `lean-bisect`.
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds the following repositories to the release configuration:
- lean4-unicode-basic
- BibtexQuery (depends on lean4-unicode-basic)
- verso-web-components (depends on verso)
It also updates dependencies:
- doc-gen4 now depends on BibtexQuery
- lean-fro.org now depends on verso-web-components
🤖 Prepared with Claude Code
This PR updates the release checklist script. The cslib repository no
longer has a docs subdirectory, so the release script was failing when
trying to update lakefile.toml and lean-toolchain in that nonexistent
directory.
This PR implements new flags and annotations for `shake` for use in
Mathlib:
> Options:
> --keep-implied
> Preserves existing imports that are implied by other imports and thus
not technically needed
> anymore
>
> --keep-prefix
> If an import `X` would be replaced in favor of a more specific import
`X.Y...` it implies,
> preserves the original import instead. More generally, prefers
inserting `import X` even if it
> was not part of the original imports as long as it was in the original
transitive import closure
> of the current module.
>
> --keep-public
> Preserves all `public` imports to avoid breaking changes for external
downstream modules
>
> --add-public
> Adds new imports as `public` if they have been in the original public
closure of that module.
> In other words, public imports will not be removed from a module
unless they are unused even
> in the private scope, and those that are removed will be re-added as
`public` in downstream
> modules even if only needed in the private scope there. Unlike
`--keep-public`, this may
> introduce breaking changes but will still limit the number of inserted
imports.
>
> Annotations:
> The following annotations can be added to Lean files in order to
configure the behavior of
> `shake`. Only the substring `shake: ` directly followed by a directive
is checked for, so multiple
> directives can be mixed in one line such as `-- shake:
keep-downstream, shake: keep-all`, and they
> can be surrounded by arbitrary comments such as `-- shake: keep
(metaprogram output dependency)`.
>
> * `module -- shake: keep-downstream`:
> Preserves this module in all (current) downstream modules, adding new
imports of it if needed.
>
> * `module -- shake: keep-all`:
> Preserves all existing imports in this module as is. New imports now
needed because of upstream
> changes may still be added.
>
> * `import X -- shake: keep`:
> Preserves this specific import in the current module. The most common
use case is to preserve a
> public import that will be needed in downstream modules to make sense
of the output of a
> metaprogram defined in this module. For example, if a tactic is
defined that may synthesize a
> reference to a theorem when run, there is no way for `shake` to detect
this by itself and the
> module of that theorem should be publicly imported and annotated with
`keep` in the tactic's
> module.
> ```
> public import X -- shake: keep (metaprogram output dependency)
>
> ...
>
> elab \"my_tactic\" : tactic => do
> ... mkConst ``f -- `f`, defined in `X`, may appear in the output of
this tactic
> ```
Not tested carefully: I will shake out any problems during the next
release. This script would have detected the mistakes I made in recent
releases of `v4.24.1` / `v4.25.1` and `v4.25.2`. (And #11374 would have
prevented these mistakes.)
This PR adds a new [radar]-based [temci]-less bench suite that replaces
the `stdlib` benchmarks from the old suite and also measures per-module
instruction counts. All other benchmarks from the old suite are
unaffected.
The readme at `tests/bench-radar/README.md` explains in more detail how
the bench suite is structured and how it works. The readmes in the
benchmark subdirectories explain what each benchmark does and which
metrics it collects.
All metrics except `stdlib//max dynamic symbols` were ported to the new
suite, though most have been renamed.
[radar]: https://github.com/leanprover/radar
[temci]: https://github.com/parttimenerd/temci
This PR renames `String.ValidPos` to `String.Pos`, `String.endValidPos`
to `String.endPos` and `String.startValidPos` to `String.startPos`.
Accordingly, the deprecations of `String.Pos` to `String.Pos.Raw` and
`String.endPos` to `String.rawEndPos` are removed early, after an
abbreviated deprecation cycle of two releases.
This PR fixes fallout of the closure allocator changes in #10982. As far
as we know
this bug only meaningfully manifests in non default build configurations
without mimalloc such as:
`cmake --preset release -DUSE_MIMALLOC=OFF`
The issue is that I forgot to update the deallocation functions for
closures. However, this only
seems to matter if we disable mimalloc which is why this slipped through
testing.
This PR implements the `#grind_lint` command, a diagnostic tool for
analyzing the behavior of theorems annotated for theorem instantiation.
The command helps identify problematic theorems that produce excessive
or unbounded instance generation during E-matching, which can lead to
performance issues.
The main entry point is:
```
#grind_lint check
```
which analyzes all theorems marked with the `@[grind]` attribute.
For each theorem, it creates an artificial goal and runs `grind`,
collecting statistics about the number of instances produced.
Results are summarized using info messages, and detailed breakdowns are
shown for lemmas exceeding a configurable threshold.
Additional subcommands are provided for targeted inspection and control:
* `#grind_lint inspect thm`: analyzes one or more specific theorems in
detail
* `#grind_lint mute thm`: excludes a theorem from instantiation during
analysis
* `#grind_lint skip thm`: omits a theorem from being analyzed by
`#grind_lint check`
This PR renames `String.endPos` to `String.rawEndPos`, as in a future
release the name `String.endPos` will be taken by the function that is
currently called `String.endValidPos`.
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.
