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.
This PR generalizes the sym MVCGen's match splitting from `ite`-only to
`ite`, `dite`, and arbitrary matchers. Previously, only `ite` was
supported; `dite` and match expressions were rejected with an error.
`mkBackwardRuleForSplit` uses `SplitInfo.splitWith` to build the
splitting proof. Hypothesis types are discovered via `rwIfOrMatcher`
inside the splitter telescope, and `TransformAltFVars.all` provides the
proper fvars for `mkForallFVars`. Subgoal type metavariables use
`mkFreshExprSyntheticOpaqueMVar` so that `rwIfOrMatcher`'s internal
`assumption` tactic cannot assign them.
Adds `DiteSplit`, `MatchSplit`, and `MatchSplitState` test cases and a
`vcgen_match_split` benchmark.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR introduces a `TransformAltFVars` structure to replace the flat
`Array Expr`
parameter in the `onAlt` callback of `MatcherApp.transform`. The new
structure gives
callers structured access to the different kinds of fvars introduced in
matcher
alternative telescopes: constructor fields, overlap parameters,
discriminant equations,
and extra equations from `addEqualities`.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds support for ignoring user defined borrow annotations. This
can be useful when defining
`extern`/`export` pairs as the `extern` might be infected by borrow
annotations while in `export`
they are already ignored.
This PR adds a benchmark that measures `simp` performance on string
literal equality and inequality for various string lengths and
difference positions.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR ports the C emission pass from IR to LCNF, marking the last step
of the IR/LCNF conversion and thus enabling end-to-end code generation
through the new compilation infrastructure.
This PR adds an `@[mvcgen_witness_type]` tag attribute, analogous to
`@[mvcgen_invariant_type]`, that allows users to mark types as witness
types. Goals whose type is an application of a tagged type are
classified as witnesses rather than verification conditions, and appear
in a new `witnesses` section in the `mvcgen` tactic syntax (before
`invariants`).
Witnesses are concrete values the prover supplies (inspired by
zero-knowledge proofs), as opposed to invariants (predicates maintained
across iterations) or verification conditions (propositions to prove).
The test uses a ZK-inspired example where a `SquareRootWitness` value
must be provided by the prover, with the resulting constraint
auto-discharged.
Changes:
- `src/Lean/Elab/Tactic/Do/Attr.lean`: register `@[mvcgen_witness_type]`
tag attribute and `isMVCGenWitnessType` helper
- `src/Lean/Elab/Tactic/Do/VCGen/Basic.lean`: add `witnesses` field to
`State`, three-way classification in `addSubGoalAsVC`
- `src/Std/Tactic/Do/Syntax.lean`: add `witnesses` section syntax
(before `invariants`), extract shared `goalDotAlt`/`goalCaseAlt` syntax
kinds
- `src/Lean/Elab/Tactic/Do/VCGen.lean`: extract shared
`elabGoalSection`, add `elabWitnesses`, wire up witness labeling and
elaboration
- `tests/elab/mvcgenWitnessType.lean`: end-to-end tests for
witness-only, witness with `-leave`, and combined witness+invariant
scenarios
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds `Invariant.withEarlyReturnNewDo`,
`StringInvariant.withEarlyReturnNewDo`, and
`StringSliceInvariant.withEarlyReturnNewDo` which use `Prod` instead of
`MProd` for the state tuple, matching the new do elaborator's output.
The existing `withEarlyReturn` definitions are reverted to `MProd` for
backwards compatibility with the legacy do elaborator. Tests and
invariant suggestions are updated to use the `NewDo` variants.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR applies `@[mvcgen_invariant_type]` to `Std.Do.Invariant` and
removes the hard-coded fallback in `isMVCGenInvariantType` that was
needed for bootstrapping (cf. #12874). It also extracts
`StringInvariant` and `StringSliceInvariant` as named abbreviations
tagged with `@[mvcgen_invariant_type]`, so that `mvcgen` classifies
string and string slice loop invariants correctly.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds an `@[mvcgen_invariant_type]` tag attribute so that users
can mark
custom types as invariant types for the `mvcgen` tactic. Goals whose
type is an
application of a tagged type are classified as invariants rather than
verification
conditions. The hard-coded check for `Std.Do.Invariant` is kept as a
fallback
until a stage0 update allows applying the attribute directly.
A follow-up PR (after a stage0 update) will apply
`@[mvcgen_invariant_type]` to
`Std.Do.Invariant` and remove the hard-coded fallback.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a CMake error when the `lake-ci` label is used. The
previous
implementation appended the full `tests/lake/tests/` glob to a base list
that
already included `tests/lake/tests/shake/test.sh`, causing a duplicate
`add_test` name. This uses an if/else to select the appropriate glob
instead.
Discovered via https://github.com/leanprover/lean4/pull/12540 which has
the
`lake-ci` label.
🤖 Prepared with Claude Code
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR makes sure that identifiers with `Meta` or `Simproc` in their
name do not show up in library search results.
For example, `Nat.Simproc.eq_add_gt` can currently be suggested by
library search, even though it is an implementation detail.
Additionally, there are various declarations in mathlib in the
`Mathlib.Meta` namespace that we do not want to suggest.
This PR adds support for simp/equational spec theorems in the SymM-based
`mvcgen'` tactic,
catching up with a feature that the original `mvcgen` has supported for
a long time.
Users can write `@[spec] theorem : get (m := StateT σ m) = fun s => pure
(s, s) := rfl`
instead of manually specifying equivalent Hoare triples. The equational
form is more
concise and natural for specs that simply unfold definitions.
The universe level normalization (`normalizeLevelsExpr`) applied in
`work` and the backward
rule constructors is a workaround; ideally this should be integrated
into
`preprocessMVar`/`preprocessExpr` in the SymM framework so all users
benefit.
Changes:
- Add `SpecTheoremKind` to distinguish triple vs simp specs in
`SpecTheoremNew`
- Add `mkSpecTheoremNewFromSimpDecl?` to create spec entries from
equational lemmas, filtering no-op equations
- Add `mkBackwardRuleFromSimpSpec` to build backward rules via
`Eq.mpr`/`congrArg`, with instance synthesis, projection reduction, and
`unfoldReducible` on the RHS
- Migrate simp theorems from `SimpTheorems` database during
`migrateSpecTheoremsDatabase`
- Normalize universe levels so structural matching in
`BackwardRule.apply` succeeds when `max u v` vs `max v u` arise from
different code paths
- Simplify `mkSpecContext` by removing the mock `simp` context
construction
- Use `mkBackwardRuleFromExpr` instead of `mkAuxLemma` for triple specs,
since the proof may contain free variables from the goal context
- Add `AddSubCancelSimp` benchmark case and test exercising the simp
spec code path
- Change `AddSubCancel` spec proofs from `mvcgen` to `mvcgen'`
(dogfooding)
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR extracts the example programs from the sym mvcgen benchmarks
into
shared `Cases.*` modules so that both benchmarks and a new fast test
suite
can reuse them. It also renames `vcgen_deep_add_sub_cancel` to
`vcgen_add_sub_cancel_deep` for consistency.
The test suite (`test_vcgen.lean`) runs all cases at n=10, completing in
~2s vs minutes for the full benchmarks. It is wired up as a `lake test`
driver and integrated with the lean4 test/bench infrastructure via
`run_test`/`run_bench` scripts registered in `CMakeLists.txt`.
Benchmark output now uses aligned `CaseName(n):` labels. The `run_bench`
script extracts per-case vcgen and kernel timings into
`measurements.jsonl`.
Benchmarks run single-threaded (`LEAN_NUM_THREADS=1`) for
reproducibility.
`vcgen_get_throw_set` is excluded from benchmarks due to pathological
`instantiateMVars` behavior.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
