This commit ensures binaries are only stripped in the `release` build
preset, not in any of the other presets.
Since `release` is used for development, the commit adds a non-stripping
copy called `dev` that can be used via `cmake --preset dev`.
This PR fixes the Windows dev build by using
`CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY` instead of the hardcoded
`lib/lean` path for the Lake plugin. On Windows, DLLs must be placed
next to executables in `bin/`, but the plugin path was hardcoded to
`lib/lean`, causing stage0 DLLs to not be found.
The `CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY` variable was introduced
precisely for this purpose — it resolves to `bin` on Windows and
`lib/lean` elsewhere.
Closes#13126🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR replaces eager let-expression zeta-reduction in the sym-based
mvcgen with on-demand unfolding that mirrors the production mvcgen's
behavior.
Previously, all let-expressions in the program head were immediately
zeta-reduced. Now, let-expressions are hoisted to the top of the goal
target, and the value is only inlined if it is duplicable (literals,
fvars, consts, `OfNat.ofNat`). Complex values are introduced into the
local context via `introsSimp`, preserving SymM's maximal sharing
invariants, and unfolded on demand when the fvar later appears as the
program head.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes several issues in `Init.Data.String`, most of them typos.
We also move the remaining material out of `Init.Data.String.Lemmas` to
`Init.Data.String.Lemmas.StringOrder`, which shortens the pole.
This PR extends the `missingDocs` linter to detect and warn about empty
doc strings (e.g. `/---/` or `/-- -/`), in addition to missing doc
strings. Previously, an empty doc comment would silence the linter even
though it provides no documentation value. Now empty doc strings produce
a distinct "empty doc string for ..." warning, while `@[inherit_doc]`
still suppresses warnings as before.
This PR switches the mvcgen worklist from BFS (queue) to DFS (stack)
ordering for subgoal processing.
With the new do elaborator, `if`-without-`else` generates asymmetric
bind depth between branches (`pure () >>= cont` is optimized to just
`cont` in the else branch). This caused BFS-based VC numbering to depend
on elaborator internals, swapping vc10/vc11 in test cases. DFS ordering
follows the syntactic program structure more naturally and is robust to
such bind-depth asymmetries.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes the handling of anonymous dependent `if` (`if _ : cond
then ... else ...`) inside `do` blocks when using the new do elaborator.
The `_%$tk` binder pattern was incorrectly quoted as `$(⟨tk⟩):hole` in
the generated `dite` syntax, causing "elaboration function for
`termDepIfThenElse` has not been implemented" errors. The fix quotes it
correctly as `_%$tk`.
A test case is added to verify both anonymous (`if _ : ...`) and named
(`if h : ...`) dependent `if` work in do blocks.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
The stage0 tree hash used by Lake to invalidate stage 1 oleans was
computed via `git ls-tree HEAD`, which fails in jj workspaces (no .git
directory). Fall back to discovering the backing git repo via `jj git
root` and resolving the current workspace's commit via `jj log -r @`
(since git's HEAD points to the root jj workspace, not the current one).
This PR adds a `@[deprecated_arg]` attribute that marks individual
function parameters as deprecated. When a caller uses the old parameter
name, the elaborator emits a deprecation warning with a code action hint
to rename or delete the argument, and silently forwards the value to the
correct binder.
Supported forms:
- `@[deprecated_arg old new (since := "...")]` — renamed parameter,
warns and forwards
- `@[deprecated_arg old new "reason" (since := "...")]` — with custom
message
- `@[deprecated_arg removed (since := "...")]` — removed parameter,
errors with delete hint
- `@[deprecated_arg removed "reason" (since := "...")]` — removed with
custom message
A warning is emitted if `(since := "...")` is omitted.
When a parameter is deprecated without a replacement, the elaborator
treats it as no longer present: using it as a named argument produces an
error. Note that positional uses of deprecated arguments are not checked
— if a function's arity changed, the caller will simply get a "function
expected" error.
The `linter.deprecated.arg` option (default `true`) controls behavior:
when enabled, renamed args produce warnings and removed args produce
specific deprecation errors with code action hints; when disabled, both
fall through to the standard "invalid argument name" error. This lets
library authors phase out old parameter names without breaking
downstream code immediately.
Example (renamed parameter):
```lean
@[deprecated_arg old new (since := "2026-03-18")]
def f (new : Nat) : Nat := new
/--
warning: parameter `old` of `f` has been deprecated, use `new` instead
Hint: Rename this argument:
o̵l̵d̵n̲e̲w̲
---
info: f 42 : Nat
-/
#guard_msgs in
#check f (old := 42)
```
Example (removed parameter):
```lean
@[deprecated_arg removed (since := "2026-03-18")]
def g (x : Nat) : Nat := x
/--
error: parameter `removed` of `g` has been deprecated
Hint: Delete this argument:
(̵r̵e̵m̵o̵v̵e̵d̵ ̵:̵=̵ ̵4̵2̵)̵
-/
#guard_msgs in
#check g (removed := 42)
```
This PR adds `simplifying_assumptions [Nat.add_assoc]` to the
`vcgen_get_throw_set_grind` benchmark, recovering hypothesis
simplification lost in a54eafb ("refactor: decouple solve from grind").
That refactor introduced `PreTac.processHypotheses` which wraps
`simpNewHyps`, but the call sites in `work` and `main` call
`Grind.processHypotheses` directly, leaving `simpNewHyps` as dead code.
Without it, long `s + 1 + … + 1` chains are never collapsed, causing an
asymptotic slowdown visible by a factor of 2 at n=150 (largest radar
input size).
Benchmark results (VCGen time in ms):
| n | Before | After | Speedup |
|---|--------|-------|---------|
| 50 | 222 | 186 | 1.2× |
| 100 | 391 | 251 | 1.6× |
| 150 | 647 | 329 | 2.0× |
| 200 | 995 | 415 | 2.4× |
| 300 | 1894 | 589 | 3.2× |
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds `@[expose]` to `Lean.Grind.abstractFn` and
`Lean.Grind.simpMatchDiscrsOnly` so that the kernel can unfold them when
type-checking `grind`-produced proofs inside `module` blocks. Other
similar gadgets (`nestedDecidable`, `PreMatchCond`, `alreadyNorm`) were
already exposed; these two were simply missed.
Closes https://github.com/leanprover/lean4/issues/13167
This PR introduces the `Body` type class, the `ChunkStream` and `Full`
types that are used to represent streaming bodies of Requests and
Responses.
This contains the same code as #10478, divided into separate pieces to
facilitate easier review.
The pieces of this feature are:
- Core data structures: #12126
- Headers: #12127
- URI: #12128
- Body: #12144
- H1: #12146
- Server: #12151
- Client:
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR changes `lake cache get` to fetch artifact cloud storage URLs
from Reservoir in a single bulk POST request rather than relying on
per-artifact HTTP redirects. When downloading many artifacts, the
redirect-based approach sends one request per artifact to the Reservoir
web host (Netlify), which can be slow and risks hitting rate limits. The
bulk endpoint returns all URLs at once, so curl only talks to the CDN
after that.
Non-Reservoir cache services are unaffected and continue using direct
URLs as before.
🤖 Prepared with Claude Code
This PR replaces the `grind` canonicalizer with a new type-directed
normalizer (`Sym.canon`) that goes inside binders and applies targeted
reductions in type positions, eliminating the O(n^2) `isDefEq`-based
approach.
The old canonicalizer maintained a map from `(function,
argument_position)` to previously seen arguments, iterating the list and
calling `isDefEq` for each new argument. This produced performance
problems in some goal. For example, for a goal containing `n` numeric
literals, it would produce O(n^2) `isDefEq` comparisons.
The new canonicalizer normalizes types directly:
- **Instances**: re-synthesized via `synthInstance` with the type
normalized first, so `OfNat (Fin (2+1)) 0` and `OfNat (Fin 3) 0` produce
the same instance.
- **Types**: normalized with targeted reductions — eta, projection,
match/ite/cond, and Nat arithmetic (`n.succ + 1` → `n + 2`, `2 + 1` →
`3`).
- **Values**: traversed but not reduced, preserving lambdas for grind's
beta module.
The canonicalizer enters binders (the old one did not), using separate
caches for type-level and value-level contexts. Propositions are not
normalized to avoid interfering with grind's proposition handling.
Move `SynthInstance` from `Grind` to `Sym` since the canonicalizer now
lives in `Sym` and needs instance synthesis. The `Grind` namespace
re-exports the key functions.
Add `no_index` annotations to `val_addNat` and `val_castAdd` patterns in
`Fin/Lemmas.lean` — arithmetic in type positions is now normalized, so
patterns must not rely on the un-normalized form for e-matching
indexing.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR changes `Lake.proc` to always log process output as `info` if
the process exits with a nonzero return code. This way it behaves the
same as `captureProc` on errors.
This PR renames `goalDotAlt` to `invariantDotAlt` and `goalCaseAlt` to
`invariantCaseAlt` to better reflect that these syntax nodes are
specific
to invariant alternatives in `mvcgen`, not general goal alternatives.
Part 2 of #13137, which made `elabInvariants` resilient to this rename
by using positional dispatch instead of quotation pattern matching.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR informs the RC optimizer that tagged values can also be
considered as "borrowed" in the sense that we do not need to consider
them as owned values for the borrow analysis (they do of course not have
an allocation they actually borrow from).
Implementation note: For the derived borrows analysis we instead just
disregard parents that are tagged. Note that we cannot match on types in
passes before boxing as the IR might still be type incorrect at that
point.
This PR replaces the manual `simpForallDomains` / `implies_congr`
machinery in `introsSimp` with `Sym.Simp.simpTelescope` as the
pre-combinator, which already handles simplifying forall telescope
domains.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR replaces quotation pattern matches on `goalDotAlt`/`goalCaseAlt`
in `elabInvariants` with positional/structural dispatch based on
`getNumArgs`. This is part 1 of renaming `goalDotAlt` to
`invariantDotAlt` and `goalCaseAlt` to `invariantCaseAlt`; the
elaborator change lands first so that the subsequent rename does not
require a stage0 update.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `simplifying_assumptions` clause to the `mvcgen'` tactic
that allows users to specify Sym.simp rewrite theorems for simplifying
hypotheses during VC generation. The syntax is `mvcgen'
simplifying_assumptions [thm₁, thm₂, ...]`. This replaces the previous
approach of hardcoding `reassocNatAdd` in `mvcgen' with grind` mode,
making hypothesis simplification user-extensible and independent of
grind.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR switches all usages from `@[mvcgen_invariant_type]` to
`@[spec_invariant_type]` and removes the old attribute registration.
Concludes the work of #13153.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR registers the new `spec_invariant_type` attribute alongside the
old
`mvcgen_invariant_type`, renames internal identifiers, and replaces the
hardcoded `Invariant` check in `Spec.lean` with `isSpecInvariantType`.
A follow-up PR will switch all usages to `spec_invariant_type` and
remove
the old attribute after stage0 is updated.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR re-enables `#print axioms` under the module system by computing
axiom dependencies at olean serialization time. It reverts #8174 and
replaces it with a proper fix.
Depends on #13142, which refactors `exportEntriesFnEx` to return all
three olean levels at once via a new `OLeanEntries` structure, allowing
extensions to share expensive computation.
The axiom extension uses `exportEntriesFnEx` to walk bodies of all
public declarations in the current module, collecting axiom dependencies
in a single batch with a shared cache across declarations. The results
are stored sorted for binary search and exported uniformly to all olean
levels. Downstream modules look up pre-computed axiom data from imported
oleans, so axiom collection never crosses module boundaries. During
elaboration of the current module, `collectAxioms` walks bodies directly
since they are always available locally.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR introduces coalescing of RC operations to the RC optimizer.
Whenever we perform multiple `inc`s for a single value within one basic
block it is legal to instead perform all of these `inc`s at once at the
first `inc` side. This is the case because the value will stay alive
until at least the last `inc` and was thus never observable with `RC=1`.
Hence, this change of `inc` location never destroys reuse opportunities.
This PR replaces the per-level `OLeanLevel → Array α` return type of
`exportEntriesFnEx` with a new `OLeanEntries (Array α)` structure that
bundles exported, server, and private entries together. This allows
extensions to share expensive computation across all three olean levels
instead of being called three separate times.
A new `computeExtEntries` function in `Environment.lean` calls each
extension's export function once and distributes results across levels.
`mkModuleData` accepts optional pre-computed entries, and `writeModule`
uses `computeExtEntries` to compute once for all three olean parts.
Extensions that previously relied on `env.setExporting` being
pre-applied by `mkModuleData` now call `env.setExporting true`
internally for their exported/server-level filtering, since the export
function is called once rather than per-level.
Extracted from #13117 to be reviewed independently.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR simplifies the `grind` canonicalizer by removing dead state and
unnecessary
complexity, and fixes two bugs discovered during the cleanup.
## Changes
**Canonicalizer cleanup:**
- Remove dead `Canon.State.canon` field — values were inserted but never
read.
The canonicalizer uses a transient `HashMap` local to each `canonImpl`
invocation.
- Remove `proofCanon` — it deduplicated `Grind.nestedProof` terms by
mapping
canonicalized propositions to a single representative, but different
proofs may
reference different hypotheses, making the result context-dependent and
preventing
cache sharing across goals.
- Remove `isDefEqBounded` — a fallback that retried `isDefEq` at default
transparency
with a heartbeat budget. The one test that depended on it was actually
masking a
transparency bug in `propagateCtorHomo`.
**Bug fixes:**
- Use `withDefault` for `mkAppOptM` in `propagateCtorHomo` (`Ctor.lean`)
— the
injectivity proof construction needs default transparency to unify
implicit
arguments of indexed inductive types like `Vector`.
- Add `Grind.abstractFn` gadget to protect lambda abstractions created
by
`abstractGroundMismatches?` from beta reduction during preprocessing.
Without
this, `Core.betaReduce` in `preprocessLight` collapses `(fun x => body)
arg`
back to `body[arg/x]`, undoing the abstraction that congruence closure
needs.
**Eta reduction infrastructure:**
- Lower `etaReduceAll` from `MetaM` to `CoreM` — it only performs
structural
operations, no `MetaM` needed.
- Add `etaReduceWithCache` that takes and returns an explicit `HashMap`
cache,
enabling callers to thread a single cache across multiple expressions.
The net effect on `Canon.State` is removing 3 fields (`canon`,
`proofCanon`)
and the `isDefEqBounded` function, along with the `useIsDefEqBounded`
and
`parent` parameters from `canonElemCore`.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR adds three new `lake cache` subcommands for staged cache
uploads: `stage`, `unstage`, and `put-staged`. These are designed to
function as parallels for the commands of the same name in Mathlib's
`lake exe cache`.
- `lake cache stage`: Copies the build outputs of a mappings file from
the Lake cache to a staging directory.
- `lake cache unstage`: Copies the build outputs from a staging
directory back into the Lake cache.
- `lake cache put-staged`: Uploads build outputs from a staging
directory to a remote cache service. Unlike `lake cache put`, this
command does not load the workspace configuration. As a result, platform
and toolchain settings must be supplied manually via `--platform` and
`--toolchain` if needed.
This PR also removes deprecation warnings when using environment
variables to configure the cache service for `lake cache put` (and `lake
cache put-staged`).
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
