This PR adds a `sym =>` tactic that enters an interactive symbolic
simulation
mode built on `grind`. Unlike `grind =>`, it does not eagerly introduce
hypotheses or apply by-contradiction, giving users explicit control over
`intro`, `apply`, and `internalize` steps.
New tactics available in `sym =>` mode:
- `intro` / `intros`: introduce binders and internalize into the E-graph
by
default. Use `intro~` or `intro (internalize := false)` to skip
internalization.
- `apply t`: apply backward rules with caching for `repeat`.
- `internalize` / `internalize_all`: internalize hypotheses into the
E-graph.
- `by_contra`: apply proof by contradiction, negating the target.
Satellite solvers (`lia`, `ring`, `linarith`) automatically introduce
remaining
binders and apply by-contradiction in `sym =>` mode, matching their
behavior in
default tactic mode. All existing `grind =>` tactics (`finish`,
`instantiate`,
`cases`, etc.) also work in `sym =>` mode. The sym-specific tactics are
guarded
and rejected in regular `grind =>` mode.
```lean
example (x : Nat) : myP x → myQ x := by
sym [myP_myQ] =>
intro h
finish
example (x y z : Nat) : x > 1 → x + y + z > 0 := by
sym =>
lia
```
This PR fixes an issue where `realizeConst` would generate auxiliary
declarations
(like `_sparseCasesOn`) using the original defining module's private
name prefix
rather than the realizing module's prefix. When two modules
independently realized
the same imported constant, they produced identically-named auxiliary
declarations,
causing "environment already contains" errors on diamond import.
The fix re-privatizes the constant name under the current module before
passing it
to `withDeclNameForAuxNaming`, ensuring each realizing module generates
distinctly
named auxiliary declarations.
Fixes#12825
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a build failure on macOS introduced by #12540. macOS BSD
`ar` does not support the `@file` response file syntax that #12540
enabled unconditionally. On macOS, when building core (i.e., `bootsrap
:= true`), `recBuildStatic` now uses `libtool -static -filelist`, which
handles long argument lists natively.
Includes a `stage0/src/stdlib_flags.h` trigger so CI will automatically
run `update-stage0` after merge.
🤖 Prepared with Claude Code
Implementation adjusted by @tydeu
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR fixes a regression introduced in Lean 4.29.0-rc2 where `simp` no
longer simplifies inside type class instance arguments due to the
`backward.isDefEq.respectTransparency` change. This breaks proofs where
a term like `(a :: l).length` appears both in the main expression and
inside implicit instance arguments (e.g., determining a `BitVec` width).
**The problem:** After `simp only [List.length_cons]`, the main
expression has `l.length + 1` but instances still have `(a ::
l).length`. Since `simp` no longer simplifies inside instances, and
`isDefEq` won't unfold `List.length` at the default transparency,
subsequent lemma applications fail.
**Reproducer** (from Son Ho, reported by Sebastian Ullrich):
```lean
theorem BitVec.getElem!_eq_testBit_toNat {w : Nat} (x : BitVec w) (i : Nat) :
x[i]! = x.toNat.testBit i := by sorry
example (l : List Nat) (a : Nat) (j : Nat) :
(0#((a :: l).length))[j]! = (0#((a :: l).length)).toNat.testBit j := by
simp only [List.length_cons]
simp only [BitVec.getElem!_eq_testBit_toNat] -- works in 4.28.0-rc1, fails in 4.29.0-rc6
```
**The fix:** Mark `List.length` as `@[implicit_reducible]`, allowing
`isDefEq` to unfold it when checking implicit arguments. Several proofs
that previously needed a trailing `rfl` after `simp` now close directly,
since `simp` can see through `List.length` in more positions.
**Longer term:** The root cause is that `GetElem` carries complex proof
obligations in its type class instances, making implicit arguments
sensitive to definitional equality of collection sizes. We are
considering a redesign with a noncomputable `GetElemV` variant based on
`Nonempty` that avoids these casts entirely, but that is a larger change
planned for a future release.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds simp lemmas equating kernel-friendly function names with
their operator notation equivalents: `Nat.land_eq`, `Nat.lor_eq`,
`Nat.xor_eq`, `Nat.shiftLeft_eq'`, `Nat.shiftRight_eq'`, and
`Bool.rec_eq`. These are useful when proofs involve reflection and need
to simplify kernel-reduced terms back to operator notation.
Closes#12716
Co-authored-by: Claude <noreply@anthropic.com>
This PR changes the Lake `CacheMap` data structure to track the
platform-dependence of outputs. Platform-independent packages will no
longer include platform-dependent mappings in the output files produced
by `lake build -o`.
This PR ensures that when a function is marked `export` its borrow
annotations (if present) are always ignored.
This was the previous behavior in the C++ version of this file but
slightly modified when porting to the old IR and thus subsequently
ported to LCNF wrongly as well.
This PR moves `RequestCancellationToken` from `IO.Ref` to
`IO.CancelToken`.
They consist of the same data, but the constructor of `CancelToken` is
private. Hence there is no way to take the `Ref` in a
`RequestCancellationToken` and turn it into a `CancelToken`. This in
turn means that we can't set `Core.Context.cancelTk?` to be the one in
`RequestContext` when launching `CoreM` tasks in request handlers.
This PR fixes some process signals that were incorrectly numbered.
From what I can tell, the code used signals and signal numbers for
Alpha/SPARC, not x86/ARM. The test was also broken and always green,
hiding the mistake.
This PR changes the interaction between `@[cbv_opaque]` and
`@[cbv_eval]`
attributes in the `cbv` tactic. Previously, `@[cbv_opaque]` completely
blocked
all reduction including `@[cbv_eval]` rewrite rules. Now, `@[cbv_eval]`
rules
can fire on `@[cbv_opaque]` constants, allowing users to provide custom
rewrite
rules without exposing the full definition. Equation theorems, unfold
theorems,
and kernel reduction remain suppressed for opaque constants.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR introduces the `Headers` data type, that provides a good and
convenient abstraction for parsing, querying, and encoding HTTP/1.1
headers.
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 fixes a segfault when running `idbgClientLoop`. `@[extern]`
expects that the function doesn't include erased arguments in the
signature; however, `@[export]` exports the function with all arguments,
including erased ones. This causes a function signature mismatch between
`idbgClientLoopImpl` and `idbgClientLoop`, causing segfaults. However,
instead of solving the deeper problem that `@[extern]` - `@[export]`
pairs can cause such problems, this PR removes the erased arguments from
`idbgClientLoopImpl` and replaces occurrences of `α` with `NonScalar`.
This PR extends Lake's use of response files (`@file`) from Windows-only
to all platforms, avoiding `ARG_MAX` limits when invoking `clang`/`ar`
with many object files.
Lake already uses response files on Windows to avoid exceeding CLI
length limits. On macOS and Linux, linking Mathlib's ~15,000 object
files into a shared library can exceed macOS's `ARG_MAX` (262,144
bytes). Both `clang` and `gcc` support `@file` response files on all
platforms, so this is safe to enable unconditionally.
Reported as a macOS issue at
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/The.20clang.20command.20line.20with.20all.20~15.2C000.20Mathlib.20.2Ec.2Eo.2Eexport/near/574369912:
the Mathlib cache ships Linux `.so` shared libs but not macOS `.dylib`
files, so `precompileModules` on macOS triggers a full re-link that
exceeds `ARG_MAX`.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds the `fixedToolchain` Lake package configuration option.
Setting this to `true` informs Lake that the package is only expected to
function on a single toolchain (like Mathlib). This causes Lake's
toolchain update procedure to prioritize its toolchain and avoids the
need to separate input-to-output mappings for the package by toolchain
version in the Lake cache.
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 the `HSub PlainTime Duration` instance, which had its
operands reversed: it computed `duration - time` instead of `time -
duration`. For example, subtracting 2 minutes from `time("13:02:01")`
would give `time("10:57:59")` rather than the expected
`time("13:00:01")`. We also noticed that `HSub PlainDateTime
Millisecond.Offset` is similarly affected.
Closes#12918
This PR places `set_option compiler.ignoreBorrowAnnotation true in` on
to all `export`/`extern`
pairs. This is necessary because `export` forces all arguments to be
passed as owned while `extern`
respects borrow annotations. The current approach to the
`export`/`extern` trick was always broken
but never surfaced. However, with upcoming changes many
`export`/`extern` pairs are going to be
affected by borrow annotations and would've broken without this.
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 changes `lake cache get` to download artifacts by default.
Artifacts can be downloaded on demand with the new `--mappings-only`
option (`--download-arts` is now obsolete).
In the future, the plan is to have Lake download mappings when cloning
dependencies. Then, `lake cache get` will primarily be used to download
artifacts eagerly. Thus, it makes sense to have that as the default.
This PR removes unused functions (`mkPatternCoreFromLambda`,
`mkPatternFromLambda`, `mkSimprocPatternFromExpr`) and the `import
Lean.Meta.AbstractMVars` that were added to `Lean.Meta.Sym.Pattern`
after merging #12597.
This PR fixes a bug where `max u v` and `max v u` fail to match in
SymM's pattern matching. Both `processLevel` (Phase 1) and
`isLevelDefEqS` (Phase 2) treated `max` positionally, so `max u v ≠ max
v u` structurally even though they are semantically equal.
The fix has three parts:
- Eagerly normalize universe levels in patterns at creation time
(`preprocessDeclPattern`, `preprocessExprPattern`,
`mkSimprocPatternFromExpr`)
- Normalize the target level in `processLevel` before matching, using a
`where go` refactor
- Add `tryApproxMaxMax` to `processLevel` and `isLevelDefEqS`: when
positional `max/max` matching would fail, check if one argument from
each side matches structurally and match the remaining pair
Also moves `normalizeLevels` from `Grind.Util` to `Sym.Util` to avoid
code duplication, since both Sym and Grind need it.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds eta reduction to the sym discrimination tree lookup
functions (`getMatch`, `getMatchWithExtra`, `getMatchLoop`). Without
this, expressions like `StateM Nat` that unfold to eta-expanded forms
`(fun α => StateT Nat Id α)` fail to match discrimination tree entries
for the eta-reduced form `(StateT Nat Id)`.
Also optimizes `etaReduce` with an early exit for non-lambda expressions
and removes a redundant `n == 0` check.
Includes a test verifying that `P (StateM Nat)` matches a disc tree
entry for `P (StateT Nat Id)`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR optimizes the `String.reduceEq`, `String.reduceNe`, and
`Sym.Simp` string equality simprocs to produce kernel-efficient proofs.
Previously, these used `String.decEq` which forced the kernel to run
UTF-8 encoding/decoding and byte array comparison, causing 86+ kernel
unfoldings on short strings.
The new approach reduces string inequality to `List Char` via
`String.ofList_injective`, then uses two strategies depending on the
difference:
- **Different characters at position `i`**: Projects to `Nat` via
`congrArg (fun l => (List.get!Internal l i).toNat)`, then uses
`Nat.ne_of_beq_eq_false rfl`. This avoids `Decidable` instances entirely
— the kernel only evaluates `Nat.beq` on two concrete natural numbers.
- **One string is a prefix of the other**: Uses `congrArg (List.drop n
·)` with `List.cons_ne_nil`, which is a definitional proof requiring no
`decide` step at all.
For equal strings, `eq_true rfl` avoids kernel evaluation entirely.
The shared proof construction is in `Lean.Meta.mkStringLitNeProof`
(`Lean/Meta/StringLitProof.lean`), used by both the standard simprocs
and the `Sym.Simp` ground evaluator.
Kernel max unfolds for `"hello" ≠ "foo"`: 86+ → 6.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adjusts the JSON encoding of RPC references from `{"p": "n"}` to
`{"__rpcref": "n"}`. Existing clients will continue to work unchanged,
but should eventually move to the new format by advertising the
`rpcWireFormat` client capability.
- This came up in leanprover/vscode-lean4#712.
- The new encoding is far less likely to clash with real-world names,
and is now documented as a "reserved internal name".
- At 8 bytes vs. 1 byte, it incurs a ~5% size increase on the JSON size
of interactive terms, e.g. from 868KiB to 903KiB on the
leanprover/vscode-lean4#500 test.
- Make `deriving RpcEncodable` throw an error when it encounters the
reserved name. We cannot easily guard against clashes in user-provided
JSON, however, so we just assume it does not clash.
- Add a notion of *RPC wire format* with corresponding `rpcWireFormat`
client and server capabilities. The format before this PR is now called
`v0`, whereas here we implement `v1`. Existing clients should eventually
implement compatibility with `v1` (because doing so fixes the above
bug), but will continue to work in the meantime. The format may be
revised again in the future (but we don't expect to revise it so often
that semver would be useful).
- Document everything.
## Alternative designs (abandoned for now)
- Option 1. Add a method `$/lean/rpc/metadata` which, given the name of
an RPC method `foo`, returns metadata containing a description of where
the RPC refs in any return value of `foo` would be (essentially a
description of the structure of the return type).
- Option 2. Wrap every response to `$/lean/rpc/call` in such metadata.
This would be a different change to the wire format.
- To implement this in an extensible way, we extend `RpcEncodable` by a
`refPaths` field. But how does `refPaths` describe where the refs are?
- Option A. Emit the code of a JS method that extracts the refs. This is
maybe simplest, but it would leave non-JS clients (e.g. `lean.nvim`)
behind.
- Option B. Give the description in some query language. The query
language must be able to describe paths into arbitrary inductive types.
- The most popular option,
[JSONPath](https://www.rfc-editor.org/rfc/rfc9535), seemingly cannot
describe non-uniform paths (e.g. both the `a`s in `{a: 1, {b: {a:
2}}}`).
- [JMESPath](https://jmespath.org/) can describe non-uniform paths, and
has 'fully compliant' implementations in many languages, but doesn't
seem to handle recursive paths.
- The most expressive option is [jq](https://github.com/jqlang/jq), but
the most popular way to run it is via an Emscripten WASM blob in
[jq-web](https://github.com/fiatjaf/jq-web) which seems heavy. There is
[jqjs](https://github.com/mwh/jqjs) as well; I'm not sure how
production-ready that is.
This PR makes `@[cbv_opaque]` unconditionally block all evaluation of a
constant
by `cbv`, including `@[cbv_eval]` rewrite rules. Previously,
`@[cbv_eval]` could
bypass `@[cbv_opaque]`, and for bare constants (not applications),
`isOpaqueConst`
could fall through to `handleConst` which would unfold the definition
body.
The intended usage pattern is now: mark subterm-producing functions
(like
`DHashMap.insert`) as `@[cbv_opaque]` to prevent unfolding, and provide
`@[cbv_eval]` theorems on the *consuming* function (like
`DHashMap.contains`)
which pattern-matches against the opaque subterms.
