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 moves the compiled Lake configurations (e.g., `lakefile.olean`)
from the package's `.lake/config` directory to the workspace's
`.lake/config`. This removes a potential source contention between
workspaces sharing a dependency.
This PR pins the `test-summary/action` GitHub Action to the immutable
commit SHA for `v2.4` to work around a broken upstream `v2` tag.
Upstream retagged `v2` to point at `v2.5`, which ships without the
bundled `index.js`, causing every job using the shared build template to
fail in the `Test Summary` post-step with `File not found:
'/home/runner/work/_actions/test-summary/action/v2/index.js'`, even when
all tests pass.
Pinning to the SHA (rather than another floating tag like `@v2.4`)
matches GitHub's [security
guidance](https://docs.github.com/en/actions/security-for-github-actions/security-guides/security-hardening-for-github-actions)
for third-party actions and avoids a repeat of this exact incident if
`v2.4` is later retagged. Dependabot is already configured for
`github-actions` updates in `.github/dependabot.yml`, so version bumps
remain low-cost.
Verification:
- `curl -sI
https://raw.githubusercontent.com/test-summary/action/v2/index.js`
returns 404
- `curl -sI
https://raw.githubusercontent.com/test-summary/action/31493c76ec9e7aa675f1585d3ed6f1da69269a86/index.js`
returns 200
The summary action is shared across every workflow that includes
`build-template.yml`, so this affects all CI Lake jobs, not just one.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR adds an experimental tactic `mvcgen'` that will soon replace
`mvcgen`. It has been reimplemented from the ground up using the new
`SymM`-based framework for efficient symbolic evaluation and can
outperform `mvcgen` by a factor of >100x for some synthetic benchmarks.
`mvcgen'` aspires to be feature-complete with `mvcgen`. Known exceptions
currently are join point sharing, introduction of local specs and
smaller bugs.
The implementation of `mvgen'` used to live in the benchmark suite for
rapid prototyping; this commit merely moves it into the Lean toolchain.
Doing so results in an build time instruction count increase in
seemingly unrelated tests such as `elab/delayed_assign//instructions`;
the reason is that the builtin elaborator attribute now pulls in
substantially more import code on startup.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR adds `whileM`, a counterpart to `Lean.Loop.forIn` that admits a
one-step unfolding lemma `whileM_eq` (impossible to prove for the
original `partial def`). `Lean.Loop.forIn` now expands to `whileM`, so
`repeat`/`while` keep working without source changes, and the
`Spec.whileM`/`Spec.forIn_loop` `@[spec]` theorems let `mvcgen`
discharge their bodies given a Nat variant and an `α ⊕ β` invariant.
`whileM.impl` is still a `partial def`, but returns a `Subtype
(whileM.Pred f a)` whose property pins the value to an `Acc.recOn` term
whenever an `Acc` and a `MonadAttach` witness exist; `whileM_eq`
extracts that property. A `@[implemented_by]` `whileM.erased` keeps the
runtime a tail call after specialization and would be unnecessary if the
compiler were able eta-expand through the trivial `Subtype` structure.
Supporting infrastructure:
`Internal.Ensures`/`MayReturn`/`ErasesTo`/`IsAttach` and `WPAdequate`
for `Id`/`ReaderT`/`StateT`/`ExceptT`/`OptionT`.
The resulting `while` loops take more work to optimize, hence a modest
increase in build time instructions.
This PR ensures that one can hover over the function name in
fun_induction. Fixes#13673
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This PR replaces `Meta.mkCongrArg` call sites in `handleProj` and
`simplifyAppFn` are replaced with direct `congrArg` constructions that
reuse types already in the `Sym` pointer cache. A few stray unqualified
`inferType` / `getLevel` / `isDefEq` calls in the same file are also
routed through the cached `Sym` equivalents.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR optimizes `lean_dec_ref_cold` by outlining the "freezing cold"
path and performing a small microarchitecural optimization. The latter
is better as it makes clear to LLVM that we believe the pointer to only
use 48 bits.
This PR adds support for blockquotes to Verso docstrings, which had been
missing before. It also substantially improves the robustness of
Verso->Markdown rendering of docstrings, especially the handling of
blockquote line prefixes.
This PR fixes the semantics of `mvcgen' with grind`: it now logs an
error per VC that `grind` cannot close and throws at the end, instead of
silently leaving the unsolved VC as a residual. The previous
silent-fallback behaviour is preserved as `mvcgen' with (try grind)`,
which `elabPreTac` recognises and routes to the same efficient `.grind`
path with a `silent` flag.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR adds a `+debug` config option to `mvcgen'` and a
`BackwardRule.applyChecked` wrapper around `BackwardRule.apply`. On
apply failure with `+debug` set, the wrapper retries on the
`unfoldReducible`-normalized goal type; if the retry succeeds, an
earlier step missed a normalization and `mvcgen'` raises a hard error
naming the rule (auto-derived from `rule.expr.getAppFn` when available)
and showing the original vs. normalized types.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR replaces the `check_cancel` two-way coordination protocol used
by
`tests/server_interactive/cancellation_par.lean` with a single tactic
`block_until_cancelled "<label>"`. The first invocation for a label
registers
a promise, prints `<label>: blocked`, and loops on
`Core.checkInterrupted`
until the cancel token fires (then `finally` resolves the promise). Any
later
invocation for the same label waits on that promise — so the test only
terminates if the first invocation actually exited the loop. If
cancellation
fails to propagate, the second invocation's `IO.wait` blocks forever and
the
test hangs (timeout = failure), with no false-success path.
The test was disabled in `tests/CMakeLists.txt` due to flakiness in the
old
two-way protocol; this PR re-enables it. Verified that reverting #13428
makes the test deadlock as expected.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This PR cleans up `tests/bench/mvcgen/sym/lib/VCGen/Util.lean`.
- Drops the four `mkApp{Rev,RevRange,Range,N}S` helpers that were
vendored locally; they are now public in `Lean.Meta.Sym.Internal`
(`Lean.Meta.Sym.AlphaShareBuilder`).
- Moves `Std.HashMap.getDM` out of the root `Std.HashMap` namespace into
`namespace VCGen` and relocates it to `RuleCache.lean`, where its only
call sites live.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR fixes an issue in the `mvcgen'` prototype where user-provided
invariant values were elaborated against a goal type containing
reducible abbreviations like `PostShape.args ps`, baking
`(PostShape.args PostShape.pure)` into the assignment instead of `[]`.
After `tryInlineInvariant` confirms the user tactic assigned the
invariant metavariable, reduce its assignment with `unfoldReducible`.
Fixes the `mvcgen'` migration path for several `tests/elab/*` proofs
that had been blocked on the entailment-phase apply failure.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR fixes an "Unknown constant" error when `set_option diagnostics
true` is enabled in module mode under a `public section`. Diagnostic
output may reference private declarations such as `_match_*` and
`_sparseCasesOn_*` that are recorded in unfold counters; constructing
the message previously failed because the environment was in exporting
mode and could not resolve those names. The diagnostic-printing paths in
`Lean.Meta.Diagnostics.reportDiag` and
`Lean.Meta.Tactic.Simp.Diagnostics.reportDiag` now run under
`withoutExporting`.
Closes https://github.com/leanprover/lean4/issues/13581.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes possible corruption when recovering from memory
exhaustion.
This code threw an `std::bad_alloc` in the case of memory exhaustion,
but left the small allocator in an inconsistent state when doing so.
This would mean any code catching and recovering from the allocation
failure would likely find itself with a corrupt small allocator.
While we could try and make this code exception safe in future, simply
making it panic is better than the status quo, and is consistent with
how we handle most other allocation failures.
changelog-please-rerun-the-changelog-ci
This PR makes the elaborator reject `@[foo]` when the module that
registers `foo` is not visibly imported into the current file but merely
loaded as IR. Previously such uses silently elaborated but led to
divergence of cmdline and server behavior and caused `lake shake --fix`
to flip-flop on successive runs (#13599).
This PR renames the `lake lint --clippy` flag to `--extra` and broadens
its scope so that it runs the default builtin linters together with the
non-default ones, instead of only the non-default ones. Use `--lint-all`
to additionally enable any other off-by-default linters.
The matching internal names follow: the namespace `Lean.Linter.Clippy`
becomes `Lean.Linter.Extra`, the option `linter.clippy` becomes
`linter.extra`, and the env-linter attribute form `@[builtin_env_linter
clippy]` becomes `@[builtin_env_linter extra]`.
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR adds the ability to specify a name for the initialization
function of a Lean plugin on load.
* The `Lean.loadPlugin` API has gained a `initFn?` argument that
defaults to `none`. When `none`, the initialization function name will
be inferred from the shared library's name (as before).
* The CLI `--plugin` option can now have a initialization function
specified via `--plugin=path:initFn`.
* The `--setup` JSON configuration now also accepts`{"path": ...,
"initFn": ...}` for plugins.
This PR fixes the termination checker reporting errors at the wrong
recursive call site when a function contains structurally-identical
recursive calls at different source locations.
The `_recApp` `MData` attached to recursive applications carried the
attached `Syntax`, but two structurally-equal `MData` wrappers could be
merged by hashconsing/simplification, so the syntax of the first call
ended up associated with both call sites. We now also store the source
byte position as `_recAppPos`, which keeps the wrappers distinct.
Closes#13444.
This PR makes radar use the LLVM that we actually ship to users (stored
at https://github.com/leanprover/lean-llvm). In doing so it also makes
the lake build compatible with lean-llvm, allowing us to do potential
release builds with lake in the future.
Those action runs don't have access to the READ_RUNNERS_TOKEN secret, so
they should just fall back to the namespace runner.
Also, this PR removes the permission checks again. They are failing for
some non-user authors (e.g. copilot) and could be removed anyways by a
malicious actor in a PR.
This PR brings the Sym-based `mvcgen'` to feature parity with `mvcgen`;
the only remaining gap is `+jp` (join-point handling).
The slight benchmark regressions are due to simplifying VCs out of
`SPred` form, hitting hardest on cases with linearly many VCs like
`PurePreCond`. The ~10% vcgen slowdown is worth it for the cleaner
user-visible VCs.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a trace event emitted whenever a `dsimp` (or rfl-only
`simp`) rewrite fires
because of a `[backward_defeq]`-tagged theorem (i.e., one that would not
have applied without `set_option backward.defeqAttrib.useBackward
true`).
Useful for finding where downstream code is silently relying on the
backwards escape hatch — a precursor to either re-tagging the lemma as
`[defeq]` or restructuring the proof so it works under the strict
defeq rules.
This PR ensures that the `lean --error=tag` flag actually sets a
non-zero exit code on promoted errors.
Closes#13588, fixing the feature introduced in #6362.
This PR prevents undefined behavior in `readModuleDataParts #[]` on
configurations without `LEAN_MMAP`. Previously this would lead to
out-of-bounds indexing.
This PR ensures that `import` gracefully processes `EINTR` errors from
the filesystem.
`read()` is allowed to return fewer bytes than requested, if it is
interrupted. If it is interrupted before returning any bytes, then it
returns `EINTR`. In either case, Lean should keep reading the file.
This PR makes `readModuleDataParts` report a clearer error if there is
insufficient memory to load a module.
changelog-ignores-my-messages-unless-i-edit-the-description-afterwards
This PR fixes a `Sym.simp` panic ("unexpected kernel projection term
during simplification") that triggered when matcher iota-reduction
exposed kernel `Expr.proj` terms via struct-eta. For example, a `do`
block with a `for` loop whose state is a tuple, where `Sym.simp`
unfolds the equational lemma and then descends into a destructuring
match.
This PR renames `UInt8.ofNatTruncate` to `UInt8.ofNatClamp`.
The new name is more consistent with the rest of the library (e.g.,
`Int8.toNatClampNeg`) and also more clear. See also [#lean4 > Name of
UInt32.ofNatTruncate etc may be
wrong](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Name.20of.20UInt32.2EofNatTruncate.20etc.20may.20be.20wrong/with/591873604).
Historical note: during prehistoric times (in January 2024),
`UInt32.ofNatTruncate` (only the 32 bit version) was introduced for use
in the `simp` configuration. When I looked at the `UIntX` API more
properly later, I added the missing variants but didn't reconsider the
name.
This PR changes Lake's module import graph processing to await the
completion of any `needs` targets or other extra dependencies (such as
cloud releases). This both enables the `needs` targets to influence
header processing and prevents them from racing with said processing.
**Known Limitation:** This PR currently blocks on the `needs` targets
rather than running the import processing in a callback. This is done to
keep import processing simple and in a single thread. If this proves to
be a performance issue, this can be restructured in a future PR with a
more sophisticated refactor.
Closes#13598
This PR fixes a Lake issue where the IR for a `meta import`'s transitive
imports was not included in the import artifacts Lake provided to Lean
(e.g., via `--setup`). When using the Lake artifact cache, this could
produce "missing data file" errors due to absent IR.
Closes#13419
---------
Co-authored-by: Claude Code <noreply@anthropic.com>
This PR fixes a `grind` congruence-table invariant violation that could
panic
when an `ite` branch was internalized lazily (after the condition became
`True`
or `False`) and that branch's equivalence class was later merged with
another.
`Internalize.lean` has a special case for `ite` that internalizes only
the
condition; the `then`/`else` branches are skipped and only internalized
later
on demand by `propagateIte`. The on-demand path (`applyCongrFun`) called
`internalize` for the branch but never called `registerParent` to add
the
parent `ite` to the branch's parent set in the e-graph. Subsequent
merges of
the branch's equivalence class then skipped re-hashing the `ite` in the
congruence table, leaving an orphan entry whose `congr` chain no longer
matched
the table's representative.
The fix adds the explicit `registerParent e rhs` that the standard
`for arg in args` loop in `Internalize.lean` would have made for an
ordinary
application argument; we are simply mirroring that pattern lazily. The
same
helper is reused by `propagateDIte`, but with parent registration
disabled
(controlled by a new `ite : Bool` parameter): for `dite` the `rhs`
propagated
upwards is a *constructed* reduction (built via `mkApp` from `e`'s
children,
possibly post-`preprocess`), not a structural argument of `e`, so
registering
`e` as its parent would be incorrect. The lambda branches of a `dite`
are
already eagerly internalized as parents of `e` by `Internalize.lean`, so
this
case does not need the fix.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
