This PR fixes a comment that said "implicit arguments" when the code
actually checks `isInstImplicit`, which is specifically for instance
implicit arguments (`[...]` binders), not all implicit arguments.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude <noreply@anthropic.com>
This PR bumps the version to 4.29.0 to begin the next development cycle
after v4.28.0-rc1.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds two benchmarks for mvcgen in the style of Leo's SymM
benchmarks.
While performance on add_sub_cancel_StateM.lean is in the same order of
magnitude as the corresponding MetaM benchmark, add_if_sub_StateM.lean
is far slower.
Measurements for add_sub_cancel:
```
goal_10: 245.576221 ms, kernel: 134.134182 ms
goal_20: 613.945320 ms, kernel: 115.453811 ms
goal_30: 1074.053596 ms, kernel: 179.076070 ms
goal_40: 1680.678302 ms, kernel: 252.066677 ms
goal_50: 2457.209584 ms, kernel: 293.974096 ms
goal_60: 3271.773330 ms, kernel: 368.394386 ms
goal_70: 3981.247921 ms, kernel: 434.297822 ms
goal_80: 5077.300540 ms, kernel: 507.047772 ms
goal_90: 6486.990060 ms, kernel: 556.952095 ms
goal_100: 7791.399986 ms, kernel: 623.605163 ms
```
Measurements for add_if_sub:
```
goal_2: 89.762349 ms, kernel: 43.320205 ms
goal_3: 190.655546 ms, kernel: 38.888499 ms
goal_4: 434.461936 ms, kernel: 75.234581 ms
goal_5: 1110.295284 ms, kernel: 161.698707 ms
goal_6: 3241.383031 ms, kernel: 326.137173 ms
goal_7: 11675.609970 ms, kernel: 684.907188 ms
```
Much room for improvement.
This PR adds `Option.of_wp_eq` and `Except.of_wp_eq`, similar to the
existing `Except.of_wp`. `Except.of_wp` is deprecated because applying
it requires prior generalization, at which point it is more convenient
to use `Except.of_wp_eq`.
This PR makes the compiler produce C code that statically initializes
close terms when possible. This change reduces startup time as the terms
are directly stored in the binary instead of getting computed at
startup.
The set of terms currently supported by this mechanism are:
- string literals
- ctors called with other statically initializeable arguments
- `Name.mkStrX` and other `Name` ctors as they require special support
due to their computed field and occur frequently due to name literals.
In core there are currently 152,524 closed terms and of these 103,929
(68%) get initialized statically with this PR. The remaining 48585 ones
are not extracted because they use (potentially transitively) various
non trivial pieces of code like `stringToMessageData` etc. We might
decide to add special support for these in the future but for the moment
this feels like it's overfitting too much for core.
This extracts a `postCallback` helper so that only the actual callback
is inlined.
Part of the motivation here is to exclude these tracing frames from
flame graph profiles.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
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 `simpTelescope`, a simproc that simplifies telescope
binders (`have`-expression values and arrow hypotheses) but not the
final body. This is useful for simplifying targets before introducing
hypotheses.
This PR adds `simpArrowTelescope`, a simproc that simplifies telescopes
of non-dependent arrows (p₁ → p₂ → ... → q) while avoiding quadratic
proof growth.
When using `Expr.forallE` to represent nested implications, each nesting
level bumps de Bruijn indices in subterms, destroying sharing even with
hash-consing. For example, a free variable `x` gets different de Bruijn
representations at each depth, causing proof terms to grow.
`simpArrowTelescope` works by:
- Converting arrows to `Arrow p q` (a definitional wrapper)
- Simplifying each component
- Converting back to `→` form
Since `Arrow` arguments are not under binders, subterms remain identical
across nesting levels and can be shared.
The `simp_4` benchmark demonstrates the improvement:
With `forallE`: ~160ms, proof_size ≈ 173k
With `Arrow`: ~43ms, proof_size ≈ 16k
Tradeoff: `simpArrowTelescope` misses simplifications that depend on the
arrow structure (e.g., `p → p` to `True`), since post-methods aren't
applied to intermediate arrows. Thus, it is not used by default. to use
it, one has to set `simpArrowTelescope` as a `pre`-method.
This PR reverts #12000, which introduced a regression where `simp`
incorrectly rejects valid rewrites for perm lemmas.
The issue is that `NameGenerator.mkChild` creates names that don't
maintain the ordering assumption used by `acLt` for perm lemma
decisions. For example, after the change:
- Child generator creates names like `_uniq.102.2`
- Parent continues with `_uniq.7`
- But `Name.lt (.num (.num `_uniq 102) 2) (.num `_uniq 7)` is true
This causes fvars created later (in async tasks) to compare as smaller
than fvars created earlier, breaking the assumption that later fvars
compare greater according to `Name.lt`.
Fixes#12136.
🤖 Prepared with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds an API for building symbolic simulation engines and
verification
condition generators that leverage `grind`. The API wraps `Sym`
operations to
work with `grind`'s `Goal` type, enabling lightweight symbolic execution
while
carrying `grind` state for discharge steps.
New operations on `Goal`:
- `mkGoal`: create a `Goal` from an `MVarId`
- `introN`, `intros`: introduce binders
- `apply`: apply backward rules
- `simp`, `simpIgnoringNoProgress`: simplify using `Sym.Simp`
- `internalize`, `internalizeAll`: add hypotheses to the E-graph
- `grind`: attempt to close the goal using `grind`
- `assumption`: close by matching a hypothesis
A new test demonstrates the API on a stateful program with conditionals,
using `grind` to discharge arithmetic side conditions.
This PR fixes a bug introduced in #12086 where a `lake build :release
--no-build` would exit with code 1 rather than the `--no-build ` code 3.
Now both the bug from #12086 and this bug are fixed.
This PR adds a new benchmark `shallow_add_sub_cancel.lean` that
demonstrates symbolic simulation using a shallow embedding into monadic
`do` notation, as opposed to the deep embedding approach in
`add_sub_cancel.lean`.
The shallow embedding approach:
- Uses Lean's `StateM` monad directly instead of a custom command
language
- Defines `Exec s k post` as a simple predicate: `post (k s).1 (k s).2`
- Proves helper theorems for reasoning about monadic operations (`pure`,
`bind`, `get`, `set`, `modify`, `ite`)
- Programs are written in actual `do`-notation rather than a custom AST
The benchmark solves goals using both the `MetaM` and `SymM` frameworks,
showing that the shallow embedding integrates well with the symbolic
simulation infrastructure. `SymM` is again way faster than `MetaM`
### Symbolic simulation benchmark — tactic time only
Problem size `n` corresponds to a program with `4·n` monadic actions.
| n | MetaM tactic (ms) | SymM tactic (ms) | Speedup |
|-----|-------------------|------------------|---------|
| 10 | 82.10 | 11.37 | ~7.2× |
| 20 | 176.21 | 17.71 | ~9.9× |
| 30 | 306.47 | 25.39 | ~12.1× |
| 40 | 509.52 | 34.53 | ~14.7× |
| 50 | 689.19 | 43.51 | ~15.8× |
| 60 | 905.86 | 52.47 | ~17.3× |
| 70 | 1172.31 | 62.50 | ~18.8× |
| 80 | 1448.48 | 70.65 | ~20.5× |
| 90 | 1787.15 | 80.89 | ~22.1× |
| 100 | 2128.12 | 90.77 | ~23.5× |
<img width="580" height="455" alt="image"
src="https://github.com/user-attachments/assets/3511aaab-4d53-4520-8302-65d2d100df4a"
/>
This PR fixes a bug in the CI version validation where `grep -oE
'[0-9]+'` matches
multiple numbers from the comment on the same line:
```
set(LEAN_VERSION_IS_RELEASE 1) # This number is 1 in the release revision, and 0 otherwise.
```
The grep extracts `1`, `1`, and `0`, causing the comparison to fail.
🤖 Prepared with Claude Code
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 documentation about the nightly build infrastructure to the
`/release` command to help future release managers understand the
relationship between branches and tags:
- `nightly` and `nightly-with-mathlib` are **branches** in
`leanprover/lean4`
- Dated tags like `nightly-YYYY-MM-DD` are **tags** in
`leanprover/lean4-nightly`
- When a nightly succeeds with mathlib, all three should point to the
same commit
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR fixes an issue that may sporadically trigger ASAN to got into a
deadlock when running a subprocess through the `IO.Process.spawn`
framework.
The general issue here is that we run `fork()` and then perform an
allocation in the child before going to `execvp` (for allocating the
arguments to `execvp`). As it turns out, doing this can cause a race
condition in ASAN that ultimately causes a deadlock in the child. This
was fixed upstream but then rolled back (see
https://github.com/google/sanitizers/issues/774). Thus, we must avoid
allocating any memory in between `fork` and `execvp`.
This PR fixes the verso hint that appears when using `sorry` in an
example block. It previously said: `` The `+error` flag indicates that
warnings are expected: +warning `` This PR replaces `error` with
`warning`. Fixes#12064
This PR revives the ability to specify modules in dependencies via the
basic `+mod` target key.
Implementation-wise, this removes deprecation of `BuildKey.module` and
once again uses it for `+mod` target keys. It also adds a test for
depending on a module of a dependency via `needs`.
This PR fixes the `lake query` output for targets which produce an
`Array` or `List` of a value with a custom `QueryText` or `QueryJson`
instance (e.g., `deps` and `transDeps`).
The most important change is that all bench scripts now must always
output to `measurements.jsonl` instead of being allowed to output
results on stdout/err.
This PR implements iteration over ranges for `Fin` and `Char`.
To this end, we introduce machinery for pulling back lawfulness of
`UpwardEnumerable` along an injective map and study the function
`Char.ordinal : Char -> Fin Char.numCodePoints`.
This PR fixes two Lake cache issues: a bug where a failed upload would
not produce an error and a mistake in the `--wfail` checks of the cache
commands.
This PR adds a comparison between `MetaM` and `SymM` for a benchmark was
proposed during the Lean@Google Hackathon.
### Benchmark description
In this benchmark, we define the semantics of a very simple imperative
language using an inductive predicate
```
Exec prog events mem lctx post
```
The predicate holds if, when executing the program `prog` with an
initial list of events `events`, memory `mem`, and local context `lctx`,
the postcondition `post` holds.
We then consider the following program:
```
input b
a := b
a := a + a
a := a - b
...
a := a + a
a := a - b
```
That is, after reading an input value `b`, the program repeatedly
updates the variable `a` by doubling it and then subtracting `b`.
We prove that, for any initial memory `m` and local context `l`, and
starting from the empty list of events, the following postcondition
holds:
```
fun t' m' l' =>
m' = m ∧ -- memory did not change
∃ v : Word,
t' = [IOEvent.IN v] ∧ -- exactly one input event
l'.get "a" = some v -- `a` contains the input value
```
In other words, executing the program produces exactly one input event,
leaves the memory unchanged, and ensures that the final value of `a` is
equal to the input value.
### Symbolic simulation benchmark (problem size `n`, with `2·n + 2`
instructions)
| Problem size (n) | MetaM time (ms) | MetaM kernel (ms) | SymM time
(ms) | SymM kernel (ms) | Total speedup |
|------------------|------------------|-------------------|----------------|------------------|---------------|
| 10 | 94.83 | 6.60 | 7.04 | 6.18 | ~13.5× |
| 20 | 218.92 | 13.33 | 14.15 | 13.02 | ~15.5× |
| 30 | 375.10 | 22.95 | 26.51 | 19.81 | ~14.2× |
| 40 | 563.82 | 34.99 | 40.42 | 29.55 | ~14.0× |
| 50 | 815.89 | 53.78 | 60.84 | 42.25 | ~13.4× |
| 60 | 1081.09 | 73.46 | 80.99 | 53.52 | ~13.3× |
| 70 | 1400.80 | 102.70 | 106.02 | 68.61 | ~13.2× |
| 80 | 1772.19 | 126.65 | 134.23 | 87.64 | ~13.2× |
| 90 | 2203.41 | 161.68 | 168.26 | 115.52 | ~13.1× |
| 100 | 2474.09 | 191.23 | 209.13 | 143.86 | ~11.8× |
<img width="580" height="455" alt="image"
src="https://github.com/user-attachments/assets/bc7058fa-e71a-4c2c-be28-860f39166965"
/>
### Symbolic simulation with extra simplification (SymM)
Problem size `n` corresponds to a program with `2·n + 2` instructions.
| n | Total time (ms) | Kernel time (ms) | Non-kernel time (ms) |
|-----|------------------|------------------|----------------------|
| 10 | 6.33 | 3.97 | 2.36 |
| 20 | 10.30 | 5.59 | 4.71 |
| 30 | 13.72 | 7.38 | 6.34 |
| 40 | 17.85 | 8.84 | 9.01 |
| 50 | 21.90 | 10.63 | 11.27 |
| 60 | 27.00 | 12.56 | 14.44 |
| 70 | 32.02 | 14.04 | 17.98 |
| 80 | 37.25 | 15.76 | 21.49 |
| 90 | 42.55 | 17.95 | 24.60 |
| 100 | 49.30 | 20.03 | 29.27 |
| 200 | 125.56 | 38.21 | 87.36 |
| 300 | 293.58 | 66.79 | 226.79 |
| 400 | 361.87 | 78.96 | 282.91 |
| 500 | 518.51 | 102.51 | 416.00 |
| 600 | 716.63 | 122.81 | 593.82 |
This PR fixes a bug where a `lake build --no-build` would exit with code
`3` if the optional job to fetch a GitHub or Reservoir release for a
package failed (even if nothing else needed rebuilding).
This PR fixes the procedure for finding the mangled symbol name of boxed
variants of native functions. Previously, the wrong symbol name has been
used for names ending in `_`: For example `test_` mangles to `l_test__`
but `test_._boxed` mangles to `l_test___00__boxed`, not
`l_test_____boxed` which the compiler would previously wrongly use.
This probably didn't affect anybody though since the failure condition
is pretty rare: the name of a native function that the interpreter tries
to execute would've had to end in `_`.
This PR adds the debugging helper functions `Expr.checkMaxShared` and
`MVarId.checkMaxShared` to `Sym`, and fixes a bug when visiting
telescopes in `Sym.simp`.
This PR adds additional debugging information to a run of `lake build
--no-build` via a `.nobuild` trace file. When a build fails due to
needing a rebuild, Lake emits the new expected trace next as `.nobuild`
file next to the build's old `.trace`. The inputs recorded in these
files can then be compared to debug what caused the mismatch.
To help keep the build directory clean, the `.nobuild` trace file is
removed on the next successful build.
This PR makes the automatic first token detection in tactic docs much
more robust, in addition to making it work in modules and other contexts
where builtin tactics are not in the environment. It also adds the
ability to override the tactic's first token as the user-visible name.
Previously, first token detection would look up the parser descriptor in
the environment and process its syntax. This would be incorrect for
builtin parsers, as well as for modules in which the definition is not
loaded. Now, it instead consults the Pratt parsing table for the
`tactic` syntax category. Tests are added that ensure this keeps working
in modules, and also that the first token of all tactics that ship with
Lean are either detected unambiguously or annotated to remove ambiguity.
Closes#12038.
This PR fixes a bug where the unknown identifier code actions were
broken in NeoVim due to the language server not properly setting the
`data?` field for all code action items that it yields.
This PR adds support for offset terms in `SymM`. This is essential for
handling equational theorems for functions that pattern match on natural
numbers in `Sym.simp`. Without this, it cannot handle simple examples
such as
```lean
def pw (n : Nat) : Nat :=
match n with
| 0 => 1
| n+1 => 2 * pw n
example : pw 4 = 16 := by
sym_simp [pw.eq_1, pw.eq_2]
example : pw (a + 2) = 2 * (2 * pw a) := by
sym_simp [pw.eq_2]
```
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 moves `String.ofList` to `Init.Prelude`. It is a function that
the Lean kernel expects to be present and has special support for (when
reducing string literals). By moving this to `Init.Prelude`, all
declarations that are special to the kernel are in that single module.
After #12001, it was no longer true that `lean_trace(name(...), ...)`
would only perform the name allocation if no trace option was set. This
PR instead avoids the allocation in any case by avoiding this pattern.
This PR changes the default of `enableArtifactCache` to use the
workspace's `enableArtifactCache` setting if the package is a dependency
and `LAKE_ARTIFACT_CACHE` is not set. This means that dependencies of a
project with `enableArtifactCache` set will also, by default, use Lake's
local artifact cache.
This PR adds `simpControl`, a simproc that handles control-flow
expressions such as `if-then-else`. It simplifies conditions while
avoiding unnecessary work on branches that won't be taken.
The key behavior of `simpControl`:
- Simplifies the condition of `if-then-else` expressions
- If the condition reduces to `True` or `False`, returns the appropriate
branch, and continue simplifying.
- If the condition simplifies to a new expression, rebuilds the
`if-then-else` with the simplified condition (synthesizing a new
`Decidable` instance), and mark it as "done". That is, simplifier main
loop will not visit branches.
- Does **not** visit branches unless the condition becomes `True` or
`False`
This is useful for symbolic simplification where we want to avoid
wasting effort
simplifying branches that may be eliminated after the condition is
resolved.
This PR also fixes a bug in `Sym/Simp/EvalGround.lean`, and adds some
helper functions.
This PR adds `Sym.Simp.evalGround`, a simplification procedure for
evaluating ground terms of builtin numeric types. It is designed for
`Sym.simp`.
Key design differences from `Meta.Simp` simprocs:
- Pure value extraction: `getValue?` functions are `OptionT Id` rather
than
`MetaM`, avoiding `whnf` overhead since `Sym` maintains canonical forms
- Specialized predicate lemmas: comparisons use pre-proved lemmas like
`Int.lt_eq_true` applied with `rfl`, avoiding `Decidable` instance
reconstruction at each call site
- Type dispatch via `match_expr`: assumes standard instances, no
synthesis
Supported types: `Nat`, `Int`, `Rat`, `Fin n`, `BitVec n`,
`UInt8/16/32/64`,
`Int8/16/32/64`.
Supported operations: arithmetic (`+`, `-`, `*`, `/`, `%`, `^`), bitwise
(`&&&`, `|||`, `^^^`, `~~~`), shifts (`<<<`, `>>>`), comparisons (`<`,
`≤`,
`>`, `≥`, `=`, `≠`, `∣`), and boolean predicates (`==`, `!=`).
This PR fixes an issue where attributes like `@[irreducible]` would not
be allowed under the module system unless combined with `@[exposed]`,
but the former may be helpful without the latter to ensure downstream
non-`module`s are also affected.
Fixes#12025
Drastically speeds up `isTracingEnabledFor` in the common case, which
has evolved from "no options set" to "`Elab.async` and probably some
linter options set but no `trace`".
## Breaking changes
`Lean.Options` is now an opaque type. The basic but not all of the
`KVMap` API has been redefined on top of it.
Ensure that individual definitions known statically to be unreachable
are stripped out by the linker instead of only whole modules. Achieves
sizeable savings today and will do more so with upcoming module system
compilation refinements.
This PR allows 'Go to Definition' to look through reducible definition
when looking for typeclass instance projections.
Specifically, this means that using 'Go to Definition' on uses of
`GT.gt` will now yield the corresponding `LT` instance as well.
This PR fixe a superliniear behavior in the closed subterm extractor.
Consider an LCNF of the shape:
```
let x1 := f arg
let x2 := f x1
let x3 := f x2
let x4 := f x3
...
```
In this case the previous closed term extraction algorithm would visit
`x1`, then `x2` and `x1`,
then `x3`,`x2`,`x1` and so on, failing each time. We now introduce a
cache to avoid this behavior.
This PR splits up the SCC that the compiler manages into (potentially)
multiple ones after
performing lambda lifting. This aids both the closed term extractor and
the elimDeadBranches pass as
they are both negatively influenced when more declarations than required
are within one SCC.
This PR fixes the pretty-printing of the `extract_lets` tactic.
Previously, the pretty-printer would expect a space after the
`extract_lets` tactic, when it was followed by another tactic on the
same line: for example,
`extract_lets; exact foo`
would be changed to
`extract_lets ; exact foo`.
This PR fixes this oversight. Found by using the pretty-printer for
formatting linting in leanprover-community/mathlib4#30658.
This PR fixes an issue where go-to-definition would jump to the wrong
location in presence of async theorems.
While the elaborator does not explicitly depend on `FVar`s not being
reused between declarations, the language server turned out to do so. As
we would have to split the name generator in any case as soon as we add
any parallelism within proofs, we now do so for any async code in order
to uphold this invariant again.
---------
Co-authored-by: mhuisi <mhuisi@protonmail.com>
This PR adds support for simplifying the arguments of over-applied and
under-applied function application terms in `Sym.simp`, completing the
implementation for all three congruence strategies (fixed prefix,
interlaced, and congruence theorems).
This PR adds missing dependencies in `src/CMakeLists.txt` to ensure that
leanrt_initial-exec, leanrt, and leancpp_1 targets wait for copy-leancpp
to complete before building. Fixes potential build race conditions in
stage 2+ builds on systems with large `nproc`.
Closes https://github.com/leanprover/lean4/issues/11808
This PR removes the need to write `.ofNat` for numeric options in
`lakefile.lean`. Note that `lake translate-config` incorrectly assumed
this was already legal in earlier revisions.
This replaces #11771.
This PR implements support for auto-generated congruence theorems in
`Sym.simp`, enabling simplification of functions with complex argument
dependencies such as proof arguments and `Decidable` instances.
Previously, `Sym.simp` used basic congruence lemmas (`congrArg`,
`congrFun`, `congrFun'`, `congr`) to construct proofs when simplifying
function arguments. This approach is efficient for simple cases but
cannot handle functions with dependent proof arguments or `Decidable`
instances that depend on earlier arguments.
The new `congrThm` function applies pre-generated congruence theorems
(similar to the main simplifier) to handle these complex cases.
This PR fixes the `floatLetIn` pass to not move variables in case it
could break linearity (owned variables being passed with RC 1). This
mostly improves the situation in the parser which previously had many
functions that were supposed to be linear in terms of `ParserState` but
the compiler made them non-linear. For an example of how this affected
parsers:
```lean-4
def optionalFn (p : ParserFn) : ParserFn := fun c s =>
let iniSz := s.stackSize
let iniPos := s.pos
let s := p c s
let s := if s.hasError && s.pos == iniPos then s.restore iniSz iniPos else s
s.mkNode nullKind iniSz
```
previously moved the `let iniSz := ...` declaration into the `hasError`
branch. However, this means that at the point of calling the inner
parser (`p c s`), the original state `s` needs to have RC>1 because it
is used later in the `hasError` branch, breaking linearity. This fix
prevents such moves, keeping `iniSz` before the `p c s` call.
This PR introduces two induction principles for bitvectors, based on the
concat and cons operations. We show how this principle can be useful to
reason about bitvectors by refactoring two population count lemmas
(`cpopNatRec_zero_le` and `toNat_cpop_append`) and introducing a new
lemma (`toNat_cpop_not`).
To use the induction principle we also move `cpopNatRec_cons_of_le` and
`cpopNatRec_cons_of_lt` earlier in the popcount section (they are the
building blocks enabling us to take advantage of the new induction
principle).
---------
Co-authored-by: luisacicolini <luisacicolini@gmail.com>
Co-authored-by: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
This PR adds missing type checking for pattern variables during pattern
matching/unification to prevent incorrect matches.
Previously, the pattern matcher could incorrectly match expressions even
when pattern variable types were incompatible with the matched subterm
types. For example, a pattern like `x` where `x : BitVec 0` could match
any term, ignoring the specific type constraint on `x`.
This PR introduces a two-phase type checking approach:
1. **Static analysis** (`mkCheckTypeMask`): Identifies which pattern
variables require type checking based on their syntactic position.
Variables that appear only as arguments to function applications skip
checking (the application structure already constrains their types),
while variables in function position, binder contexts, or standalone
positions must be checked.
2. **Runtime validation**: During matching, when a pattern variable is
assigned, its type is checked against the matched subterm's type if
flagged by the mask. Checking uses `withReducible` to balance soundness
and performance.
The PR also adds helper functions for debugging (`Sym.mkMethods`,
`Sym.simpWith`, `Sym.simpGoal`) and fixes a minor issue where
`Theorem.rewrite` could return `.step` with identical expressions
instead of `.rfl`.Body:
This PR optimizes congruence proof construction in `Sym.simp` by
avoiding
`inferType` calls on expressions that are less likely to be cached.
Instead of
inferring types of expressions like `@HAdd.hAdd Nat Nat Nat instAdd 5`,
we infer
the type of the function prefix `@HAdd.hAdd Nat Nat Nat instAdd` and
traverse
the forall telescope.
The key insight is that function prefixes are more likely shared across
many call sites
(e.g., all `Nat` additions use the same `@HAdd.hAdd Nat Nat Nat
instAdd`), so they
benefit from `inferType` caching.
Benchmark results show improvements on workloads with shared function
prefixes:
- `many_rewrites_5000`: 48.8ms → 43.1ms (-12%)
- `term_tree_5000`: 53.4ms → 30.5ms (-43%)
This PR implements a new strategy for simplifying `have`-telescopes in
`Sym.simp` that achieves linear kernel type-checking time instead of
quadratic.
## Problem
When simplifying deep `have`-telescopes, the previous approach using
`have_congr'` produced proofs that type-checked in quadratic time. The
simplifier itself was fast, but the kernel became the bottleneck for
large telescopes.
For example, at n=100:
- **Before**: simp = 2.4ms, kernel = **225ms**
- **After**: simp = 3.5ms, kernel = **10ms**
The quadratic behavior occurred because the kernel creates fresh free
variables for each binder when type-checking, destroying sharing and
producing O(n²) intermediate terms.
## Solution
We transform sequential `have`-telescopes into a parallel
beta-application form:
```
have x₁ := v₁; have x₂ := v₂[x₁]; b[x₁, x₂]
↓ (definitionally equal)
(fun x₁ x₂' => b[x₁, x₂' x₁]) v₁ (fun x₁ => v₂[x₁])
```
This parallel form leverages the efficient simplifier for lambdas in
`Sym.simp`. This form enables:
1. Independent simplification of each argument
2. Proof construction using standard congruence lemmas
3. Linear kernel type-checking time
The algorithm has three phases:
1. **`toBetaApp`**: Transform telescope → parallel beta-application
2. **`simpBetaApp`**: Simplify using `congr`/`congrArg`/`congrFun'` and
`simpLambda`
3. **`toHave`**: Convert back to `have` form
## Benchmark Results
### Benchmark 1: Chain with all variables used in body
| n | Before (simp) | Before (kernel) | After (simp) | After (kernel) |
|---|---------------|-----------------|--------------|----------------|
| 50 | 1.2ms | 32ms | 1.6ms | 4.4ms |
| 100 | 2.4ms | **225ms** | 3.5ms | **10ms** |
| 200 | 4.5ms | — | 8.4ms | 27ms |
| 500 | 11.7ms | — | 33.6ms | 128ms |
### Benchmark 3: Parallel declarations (simplified values)
| n | Before (simp) | Before (kernel) | After (simp) | After (kernel) |
|---|---------------|-----------------|--------------|----------------|
| 50 | 0.5ms | 24ms | 0.8ms | 1.8ms |
| 100 | 1.2ms | **169ms** | 1.8ms | **5.3ms** |
| 200 | 2.2ms | — | 3.9ms | 17ms |
| 500 | 5.9ms | — | 12.3ms | 93ms |
### Benchmark 5: Chain with single dependency
| n | Before (simp) | Before (kernel) | After (simp) | After (kernel) |
|---|---------------|-----------------|--------------|----------------|
| 100 | 1.6ms | 6.2ms | 1.8ms | 6.2ms |
| 200 | 2.8ms | 21.6ms | 4.4ms | 16.5ms |
| 500 | 7.3ms | **125ms** | 12.8ms | **72ms** |
Key observations:
- Kernel time is now **linear** in telescope depth (previously
quadratic)
- Simp time increases slightly due to the transformation overhead
- Total time (simp + kernel) is dramatically reduced for large
telescopes
- The improvement is most pronounced when the body depends on many
variables
## Trade-offs
- Proof sizes are larger (more congruence lemma applications)
- Simp time has ~1.5x overhead from the transformation
- For very small telescopes (n < 10), the overhead may not pay off
The optimization targets the critical path: kernel type-checking was the
bottleneck preventing scaling to realistic symbolic simulation
workloads.
This PR fixes a panic that occurred when a theorem had a docstring on an
auxiliary definition within a `where` clause.
Reproducer:
```lean
theorem foo : True := aux where /-- -/ aux := True.intro
```
The issue was that `asyncMayModify` used `.any` to check if a nested
declaration could have its extension state modified, which returned
`false` when the declaration wasn't yet in `asyncConsts`. Using `.all`
instead returns `true` for `none` (vacuously true), allowing
modification
of extension state for nested declarations that haven't been added to
`asyncConsts` yet.
Closes#11799🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR fixes library suggestions to include private proof-valued
structure fields.
Private proof-valued structure fields (like `private size_keys' :
keys.size = values.size`) generate projections with `_private.*` mangled
names. These were being filtered out by `isDeniedPremise` because
`isInternalDetail` returns true for names starting with `_`.
The fix allows private names through by checking `!isPrivateName name`,
following the pattern from #11946. This enables `grind +suggestions` to
discover and use private proof-valued structure fields from the current
module.
Soon I would like to fix the semantics of `isInternalDetail`, as the
current behaviour is clearly wrong, but as there are many call sites, I
would like to get the behaviour of tactics correct first.
Also switches `currentFile` to use `wasOriginallyTheorem` instead of
matching on `.thmInfo`, which correctly identifies both theorems and
proof-valued projections.
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds guidance for investigating CI failures promptly rather than
waiting for other jobs to complete.
---
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR moves the `deriving instance BEq for Option` from
`Init.Data.Option.Basic` to `Init.Core`, making `BEq (Option α)`
available earlier in the import chain.
This is preparatory work for adding `maxSuggestions : Option Nat` fields
to `Grind.Config` and `Simp.Config`, which need `BEq (Option Nat)` for
the `deriving BEq` clause.
The duplicate derivation in `Init.Data.Option.Basic` is kept because
proofs there need the definition to be exposed.
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds a new `first_par` tactic combinator that runs multiple
tactics in parallel and returns the first successful result (cancelling
the others).
The `try?` tactic's `atomicSuggestions` step now uses `first_par` to try
three grind variants in parallel:
- `grind? +suggestions` - uses library suggestion engine
- `grind? +locals` - unfolds local definitions from current file
- `grind? +locals +suggestions` - combines both
This leverages `TacticM.parFirst` which already provides the "first
success wins" parallel execution with cancellation.
### Depends on
- [x] depends on: #11946🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR provides a `Decidable` instance for `Nat.isPowerOfTwo` based on
the formula `(n ≠ 0) ∧ (n &&& (n - 1)) = 0`.
To do this it includes theorems about `Nat.testBit` to show that the
`n.log2`th bit is set in `n` and `n - 1` for non powers of two.
Bitwise lemmas are needed to reason about the `&&&` so the file
`Init.Data.Nat.Power2` is renamed to `Init.Data.Nat.Power2.Basic` and
`Init.Data.Nat.Power2.Lemmas` introduced that depends on
`Init.Data.Nat.Bitwise.Lemmas` to prevent circular includes.
---------
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
This PR changes the runtime implementation of the `Decidable (xs = #[])`
and `Decidable (#[] = xs)` instances to use `Array.isEmpty`. Previously,
`decide (xs = #[])` would first convert `xs` into a list and then
compare it against `List.nil`.
This PR adds a `+locals` configuration option to the `simp`, `simp_all`,
and `dsimp` tactics that automatically adds all definitions from the
current file to unfold.
Example usage:
```lean
def foo (n : Nat) : Nat := n + 1
-- Without +locals, simp doesn't know about foo
example (n : Nat) : foo n = n + 1 := by simp -- fails
-- With +locals, simp can unfold foo
example (n : Nat) : foo n = n + 1 := by simp +locals -- succeeds
```
The implementation iterates over `env.constants.map₂` (which contains
constants defined in the current module) and adds definitions to unfold.
Instance definitions and internal details are filtered out.
**Note:** For local theorems, use `+suggestions` instead, which will
include relevant local theorems via the library suggestion engine.
🤖 Prepared with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds a `+locals` configuration option to the `grind` tactic that
automatically adds all definitions from the current file as e-match
theorems. This provides a convenient alternative to manually adding
`[local grind]` attributes to each definition. In the form `grind?
+locals`, it is also helpful for discovering which local declarations it
may be useful to add `[local grind]` attributes to.
Example usage:
```lean
def foo (n : Nat) : Nat := n + 1
-- Without +locals, grind doesn't know about foo
example (n : Nat) : foo n = n + 1 := by grind -- fails
-- With +locals, grind can use the equation
example (n : Nat) : foo n = n + 1 := by grind +locals -- succeeds
```
Instance definitions and internal details are filtered out.
🤖 Prepared with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude <noreply@anthropic.com>
This PR makes the external checker lean4checker available as the
existing `leanchecker` binary already known to elan, allowing for
out-of-the-box access to it.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds utility functions for managing the message log during
tactic
evaluation, and refactors existing code to use them.
**New helpers in `Lean.Elab.Tactic`:**
- `withSuppressedMessages`: executes an action while suppressing new
messages
- `withCapturedMessages`: executes an action and returns any new
messages
- `hasErrorMessages`: checks if a message list contains errors
**Refactored to use these helpers:**
- `LibrarySearch.tryDischarger`: now uses `withSuppressedMessages`
- `Try.evalAndSuggest`: now uses `withSuppressedMessages`
- `Try.evalAndSuggestWithBy`: now uses `withSuppressedMessages`
These helpers provide a standard pattern for tactic validation that
needs to
inspect error messages (e.g., filtering out suggestions that produce
errors).
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR ensures that pretty-printing of unification hints inserts a
space after |- resp. ⊢.
All uses in Lean core and mathlib add a space after the |- or ⊢ symbol;
this makes the output match usage in practice.
This was discovered in leanprover-community/mathlib4#30658, adding a
formatting linter using pretty-printing as initial guide.
This PR filters deprecated lemmas from `exact?` and `rw?` suggestions.
Previously, both tactics would suggest deprecated lemmas, which could be
confusing for users since using the suggestion would trigger a
deprecation warning.
Now, lemmas marked with `@[deprecated]` are filtered out in the
`addImport` functions that populate the discrimination trees used by
these tactics.
**Example (before this PR):**
```lean
import Mathlib.Logic.Basic
example (h : ∃ n : Nat, n > 0) : True := by
choose (n : Nat) (hn : n > 0 + 0) using h
guard_hyp hn : n > 0 -- `rw?` would suggest `Eq.rec_eq_cast` which is deprecated
```
Zulip discussion:
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/deprecated.20lemma.20from.20rw.3F/near/554106870🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR improves the error message when `initialize` (or `opaque`) fails
to find an `Inhabited` or `Nonempty` instance.
**Before:**
```
failed to synthesize
Inhabited Foo
```
**After:**
```
failed to synthesize 'Inhabited' or 'Nonempty' instance for
Foo
If this type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
```
Prompted by
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/initialize.20structure.20with.20IO.2ERef/near/564936030🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds a symbol to the runtime for marking `Array`
non-linearities. This should allow users to
spot them more easily in profiles or hunt them down using a debugger.
This PR adds a new option to the function `simpHaveTelescope` in which
the `have` telescope is simplified in two passes:
* In the first pass, only the values and the body are simplified.
* In the second pass, unused declarations are eliminated.
This new mode eliminates **superlinear** behavior in the benchmark
`simp_3.lean`. Note that the kernel type checker still **exhibits**
quadratic behavior in this example, because it **does not have support**
for expanding a `have`/`let` telescope in a single step.
This PR adds two features to the message testing commands:
## `#guard_panic` command
A new `#guard_panic` command that succeeds if the nested command
produces a panic message. Unlike `#guard_msgs`, it does not check the
exact message content, only that a panic occurred.
This is useful for testing commands that are expected to panic, where
the exact panic message text may be volatile. It is particularly useful
when minimizing a panic discovered "in the wild", while ensuring the
panic behaviour is preserved.
## `substring := true` option for `#guard_msgs`
Adds a `substring := true` option to `#guard_msgs` that checks if the
docstring appears as a substring of the output (after whitespace
normalization), rather than requiring an exact match. This is useful
when you only care about part of the message.
Example:
```lean
/-- Unknown identifier -/
#guard_msgs (substring := true) in
example : α := x
```
## Refactoring
Also refactors `runAndCollectMessages` as a shared helper function used
by both `#guard_msgs` and `#guard_panic`.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR factors out the `have`-telescope support used in `simp`, and
implements it using the `MonadSimp` interface. The goal is to
use this nice infrastructure for both `Meta.simp` and `Sym.simp`.
This PR covers tactic docstrings in the documentation style guide.
At the Mathlib Initiative we want to ensure that tactics have good
documentation. Since this will involve adding documentation to tactics
built into core Lean, I discussed with David that we should write a
shared set of documentation guidelines that allow me to do my work both
on the Lean and on the Mathlib repositories.
I have already shown an earlier version of this guideline to David who
made some helpful suggestions but would be away for a few days. So to
make sure the discussion doesn't get lost, I've made a PR with the
version I ended up with after the first round of comments.
---------
Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com>
This PR reorganizes the monad hierarchy for symbolic computation in
Lean.
## Motivation
We want a clean layering where:
1. A foundational monad (`SymM`) provides maximally shared terms and
structural/syntactic `isDefEq`
2. `GrindM` builds on this foundation, adding E-graphs, congruence
closure, and decision procedures
3. Symbolic execution / VCGen uses `GrindM` directly without introducing
a third monad
## Changes
The core symbolic computation layer still lives in `Lean.Meta.Sym`. This
monad (`SymM`) provides:
- Maximally shared terms with pointer-based equality
- Structural/syntactic `isDefEq` and matching (no reduction, predictable
cost)
- Monotonic local contexts (no `revert` or `clear`), enabling O(1)
metavariable validation
- Efficient `intro`, `apply`, and `simp` implementations
The name "Sym" reflects that this is infrastructure for symbolic
computation: symbolic simulation, verification condition generation, and
decision procedures.
### Updated hierarchy
```
Lean.Meta.Sym -- SymM: shared terms, syntactic isDefEq, intro, apply, simp
Lean.Meta.Grind -- GrindM: E-graphs, congruence closure (extends SymM)
```
Symbolic execution is a usage pattern of `GrindM` operating on
`Grind.Goal`, not a separate monad. This keeps the API surface minimal:
users learn two monads, and VCGen is "how you use `GrindM`" (for users
that want to use `grind`) rather than a third abstraction to understand.
This PR implements `PersistentHashMap.findKeyD` and
`PersistentHashSet.findD`. The motivation is avoid two memory
allocations (`Prod.mk` and `Option.some`) when the collections contains
the key.
This PR fixes an issue where `grind` failed to prove `f ≠ 0` from `f * r
≠ 0` when using `Lean.Grind.CommSemiring`, but succeeded with
`Lean.Grind.Semiring`.
The `propagateMul` propagator handles `0 * a = 0` and `a * 0 = 0` rules
for semirings that don't have full ring support in grind. Previously,
`CommSemiring` was excluded because it uses a ring envelope for
normalization, but that approach doesn't propagate these equalities back
to the original terms. Now `CommSemiring` also uses `propagateMul`.
Reported as
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Grind.20failure.20for.20CommSemiring.2C.20not.20Semiring🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds `gcd_left_comm` lemmas for both `Nat` and `Int`:
- `Nat.gcd_left_comm`: `gcd m (gcd n k) = gcd n (gcd m k)`
- `Int.gcd_left_comm`: `gcd a (gcd b c) = gcd b (gcd a c)`
These lemmas establish the left-commutativity property for gcd,
complementing the existing `gcd_comm` and `gcd_assoc` lemmas.
Upstreamed from
https://github.com/leanprover-community/mathlib4/pull/33235🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds a `done` flag to the result returned by `Simproc`s in
`Sym.simp`.
The `done` flag controls whether simplification should continue after
the result:
- `done = false` (default): Continue with subsequent simplification
steps
- `done = true`: Stop processing, return this result as final
## Use cases for `done = true`
### In `pre` simprocs
Skip simplification of certain subterms entirely:
```
def skipLambdas : Simproc := fun e =>
if e.isLambda then return .rfl (done := true)
else return .rfl
```
### In `post` simprocs
Perform single-pass normalization without recursive simplification:
```
def singlePassNormalize : Simproc := fun e =>
if let some (e', h) ← tryNormalize e then
return .step e' h (done := true)
else return .rfl
```
With `done = true`, the result `e'` won't be recursively simplified.
This PR adds support for simplifying lambda expressions in `Sym.simp`.
It is much more efficient than standard simp for very large lambda
expressions with many binders. The key idea is to generate a custom
function extensionality theorem for the type of the lambda being
simplified.
This technique is compatible with the standard `simp` tactic, and will
be ported in a separate PR.
<img width="581" height="455" alt="image"
src="https://github.com/user-attachments/assets/5911dc6c-03f0-48ed-843b-b8cb4f67ee61"
/>
### `lambda` benchmark summary
| Lambda size | MetaM (ms) | SymM (ms) | Speedup |
|-------------|------------|-----------|---------|
| 50 | 22.7 | 0.74 | ~31× |
| 100 | 120.5 | 1.75 | ~69× |
| 150 | 359.6 | 2.90 | ~124× |
| 200 | 809.5 | 4.51 | ~180× |
This PR adds a guard to `TagDeclarationExtension.tag` to check if the
declaration name is anonymous and return early if so. This prevents a
panic that could occur when modifiers like `meta` or `noncomputable` are
used in combination with syntax errors.
Reproducer:
```lean
public meta section
def private
```
Previously this would panic with:
```
PANIC at Lean.EnvExtension.modifyState: called on `async` extension,
must set `asyncDecl` in that case
```
This follows the same pattern as the fix in #10131 for `addDocString`
and the existing guard in `markNotMeta`.
See
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/panic.20on.20doc-string/near/566110399🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR ensures that `Sym.simp` checks thresholds for maximum recursion
depth and maximum number of steps. It also invokes `checkSystem`.
Additionally, this PR simplifies the main loop. Assigned metavariables
and `zetaDelta` reduction are now handled by installing `pre`/`post`
methods.
This PR adds `getMatch` and `getMatchWithExtra` for retrieving patterns
from
discrimination trees in the symbolic simulation framework.
The PR also adds uses `DiscrTree` to implement indexing in `Sym.simp`.
This PR adds discrimination tree support for the symbolic simulation
framework.
The new `DiscrTree.lean` module converts `Pattern` values into
discrimination
tree keys, treating proof/instance arguments and pattern variables as
wildcards
(`Key.star`). Motivation: efficient pattern retrieval during rewriting.
This PR adds a `with_unfolding_none` tactic that sets the transparency
mode to `.none`, in which no definitions are unfolded. This complements
the existing `with_unfolding_all` tactic and provides tactic-level
access to the `TransparencyMode.none` added in
https://github.com/leanprover/lean4/pull/11810.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds the directory `Meta/DiscrTree` and reorganizes the code
into different files. Motivation: we are going to have new functions for
retrieving simplification theorems for the new structural simplifier.
This PR improves the performance of `getLine` by coalescing the locking
of the underlying `FILE*`.
Unfortunately we cannot use `getline` or `fgets` for this as our code
needs to handle `\0` chars
and Windows.
This PR makes `mvcgen with tac` fail if `tac` fails on one of the VCs,
just as `induction ... with tac` fails if `tac` fails on one of the
goals. The old behavior can be recovered by writing `mvcgen with try
tac` instead.
This PR adds configuration flag `Meta.Context.cacheInferType`. You can
use it to disable the `inferType` cache at `MetaM`. We use this flag to
implement `SymM` because it has its own cache based on pointer equality.
This PR adds `CongrInfo` analysis for function applications in the
symbolic simulator framework. `CongrInfo` determines how to build
congruence proofs for rewriting subterms efficiently, categorizing
functions into:
- `none`: no arguments can be rewritten (e.g., proofs)
- `fixedPrefix`: common case where implicit/instance arguments form a
fixed prefix and explicit arguments can be rewritten (e.g., `HAdd.hAdd`,
`Eq`)
- `interlaced`: rewritable and non-rewritable arguments alternate (e.g.,
`HEq`)
- `congrTheorem`: uses auto-generated congruence theorems for functions
with dependent proof arguments (e.g., `Array.eraseIdx`)
This PR changes `bv_decide`'s heuristic for what kinds of structures to
split on to also allow
splitting on structures where the fields have dependently typed widths.
For example:
```lean
structure Byte (w : Nat) where
/-- A two's complement integer value of width `w`. -/
val : BitVec w
/-- A per-bit poison mask of width `w`. -/
poison : BitVec w
```
This is to allow handling situations such as `(x : Byte 8)` where the
width becomes concrete after
splitting is done.
This PR adds an incremental variant of `shareCommon` for expressions
constructed from already-shared subterms. We use this when an expression
`e` was produced by a Lean API (e.g., `inferType`, `mkApp4`) that does
not preserve maximal sharing, but the inputs to that API were already
maximally shared. Unlike `shareCommon`, this function does not use a
local `Std.HashMap ExprPtr Expr` to track visited nodes. This is more
efficient when the number of new (unshared) nodes is small, which is the
common case when wrapping API calls that build a few constructor nodes
around shared inputs.
This PR changes the definition of the iterator combinators `takeWhileM`
and `dropWhileM` so that they use `MonadAttach`. This is only relevant
in rare cases, but makes it sometimes possible to prove such combinators
finite when the finiteness depends on properties of the monadic
predicate.
This PR fixes a bug in the new pattern matching procedure for the Sym
framework. It was not correctly handling assigned metavariables during
pattern matching.
It also improves the support for free variables.
This PR adds performance comparison tests between the new `SymM` monad
and the standard `MetaM` for `intros`/`apply` operations.
The tests solve problems of the form:
```lean
let z := 0; ∀ x, ∃ y, x = z + y ∧ let z := z + x; ∀ x, ∃ y, x = z + y ∧ ... ∧ True
```
using repeated `intros` and `apply` with `Exists.intro`, `And.intro`,
`Eq.refl`, and `True.intro`.
**Results show 10-20x speedup:**
| Size | MetaM | SymM | Speedup |
|------|-------|------|---------|
| 1000 | 226ms | 21ms | 10.8x |
| 2000 | 582ms | 44ms | 13.2x |
| 3000 | 1.08s | 72ms | 15.0x |
| 4000 | 1.72s | 101ms | 17.0x |
| 5000 | 2.49s | 125ms | 19.9x |
| 6000 | 3.45s | 157ms | 22.0x |
This PR adds `BackwardRule` for efficient goal transformation via
backward chaining in `SymM`.
`BackwardRule` stores a theorem expression, precomputed pattern for
fast unification, and argument indices that become new subgoals. The
subgoal ordering lists non-dependent goals first to match the behavior
of `MetaM.apply`.
`BackwardRule.apply` unifies the goal type with the rule's pattern,
assigns the goal metavariable to the theorem application, and returns
new subgoals for unassigned arguments.
This PR makes the `FinitenessRelation` structure, which is helpful when
proving the finiteness of iterators, part of the public API. Previously,
it was marked internal and experimental.
This PR expands the pull request creation section with detailed
formatting guidelines including title format (type prefixes, imperative
present tense) and body format requirements (starting with "This PR").
Adds a concrete example for reference.
All modifications were suggested by Claude.
This PR adds `num?` parameter to `mkPatternFromTheorem` to control how
many leading quantifiers are stripped when creating a pattern. This
enables matching theorems where only some quantifiers should be
converted to pattern variables.
For example, to match `mk_forall_and : (∀ x, P x) → (∀ x, Q x) → (∀ x, P
x ∧ Q x)` against a goal `∀ x, q x 0 ∧ q (f (f x)) y`, we use
`mkPatternFromTheorem ``mk_forall_and (some 5)` to create the pattern `∀
x, ?P x ∧ ?Q x`, keeping the outermost `∀` in the pattern rather than
converting it to a pattern variable.
This PR completes the new pattern matching and unification procedures
for the symbolic simulation framework using a two-phase approach.
**Phase 1 (Syntactic Matching):**
- Patterns use de Bruijn indices for expression variables and renamed
level params for universe variables
- Purely structural matching after reducible definitions are unfolded
- Universe levels treat `max`/`imax` as uninterpreted functions
- Proof arguments skipped via proof irrelevance
- Instance and binder constraints deferred to Phase 2
**Phase 2 (Pending Constraints):**
- Level constraints: structural equality with mvar assignment
- Instance constraints: `isDefEqI` (full `isDefEq` for TC synthesis)
- Expression constraints: `isDefEqS` with Miller pattern support
- Unassigned instance pattern variables synthesized via
`trySynthInstance`
**`isDefEqS` (Structural DefEq):**
- Miller pattern detection and assignment (`?m x y z := rhs` → `?m :=
fun x y z => rhs`)
- Scope checking via `maxFVar` to prevent out-of-scope assignments
- Optional zeta-delta reduction for let-declarations
- Proof irrelevance and instance delegation to `isDefEqI`
**Key optimizations:**
- `abstractFVars` skips metavariables and uses `maxFVar` for early
cutoff
- Per-pattern `ProofInstInfo` cache for fast argument classification
- Maximal sharing.
This PR implements `isDefEqS`, a lightweight structural definitional
equality for the symbolic simulation framework. Unlike the full
`isDefEq`, it avoids expensive operations while still supporting Miller
pattern unification.
**Key features:**
- Structural matching with optional zeta-delta reduction for
let-declarations
- Miller pattern detection and assignment (`?m x y z := rhs` → `?m :=
fun x y z => rhs`)
- Scope checking via `maxFVar` to prevent out-of-scope assignments
- Proof arguments skipped via proof irrelevance
- Instance arguments delegated to full `isDefEq` (need TC machinery)
- Universe levels treated structurally (`max`/`imax` as uninterpreted)
This PR adds optimized `abstractFVars` and `abstractFVarsRange` for
converting free variables to de Bruijn indices during pattern
matching/unification.
**Optimizations:**
- Metavariables are skipped (their contexts must not include abstracted
fvars)
- Subterms whose `maxFVar` is below the minimal abstracted fvar are
skipped via early cutoff
- Results are maximally shared via `AlphaShareBuilderM`
These optimizations are sound for Miller pattern matching where
metavariables are created before entering binders.
This PR implements `instantiateRevBetaS`, which is similar to
`instantiateRevS` but beta-reduces nested applications whose function
becomes a lambda after substitution.
For example, if `e` contains a subterm `#0 a` and we apply the
substitution `#0 := fun x => x + 1`, then `instantiateRevBetaS` produces
`a + 1` instead of `(fun x => x + 1) a`.
This is useful when applying theorems. For example, when applying
`Exists.intro`:
```lean
Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p
```
to a goal of the form `∃ x : Nat, p x ∧ q x`, we create metavariables
`?w` and `?h`. With `instantiateRevBetaS`, the type of `?h` becomes `p
?w ∧ q ?w` instead of `(fun x => p x ∧ q x) ?w`.
This PR introduces a fast pattern matching and unification module for
the symbolic simulation framework (`Sym`). The design prioritizes
performance by using a two-phase approach:
**Phase 1 (Syntactic Matching)**
- Patterns use de Bruijn indices for expression variables and renamed
level params (`_uvar.0`, `_uvar.1`, ...) for universe variables
- Matching is purely structural after reducible definitions are unfolded
during preprocessing
- Universe levels treat `max` and `imax` as uninterpreted functions (no
AC reasoning)
- Binders and term metavariables are deferred to Phase 2
**Phase 2 (Pending Constraints)** [WIP]
- Handles binders (Miller patterns) and metavariable unification
- Converts remaining de Bruijn variables to metavariables
- Falls back to `isDefEq` when necessary
**Key design decisions:**
- Preprocessing unfolds reducible definitions and performs beta/zeta
reduction
- Kernel projections are expected to be folded as projection
applications before matching
- Assignment conflicts are deferred to pending rather than invoking
`isDefEq` inline
- `instantiateRevS` ensures maximal sharing of result expressions
**TODO:**
- Skip instance arguments during matching, synthesize later
- Skip proof arguments (proof irrelevance)
- Implement `processPending` for Phase 2 constraints
This PR refactors the `Goal` type used in `grind`. The new
representation allows multiple goals with different metavariables to
share the same `GoalState`. This is useful for automation such as
symbolic simulator, where applying theorems create multiple goals that
inherit the same E-graph, congruence closure and solvers state, and
other accumulated facts.
This PR implements `intro` (and its variants) for `SymM`. These versions
do not use reduction or infer types, and ensure expressions are
maximally shared.
This PR adds the function `Sym.instantiateS` and its variants, which are
similar to `Expr.instantiate` but assumes the input is maximally shared
and ensures the output is also maximally shared.
This PR adds the function `Sym.replaceS`, which is similar to
`replace_fn` available in the kernel but assumes the input is maximally
shared and ensures the output is also maximally shared. The PR also
generalizes the `AlphaShareBuilder` API.
This PR simplifies `AlphaShareCommon.State` by separating the persistent
and transient parts of the state.
The `map` field caches visited sub-expressions during a single
`shareCommonAlpha` call to handle DAGs efficiently, the input expression
may contain shared sub-expressions that are not yet maximally shared.
However, this cache does not need to persist between different
`shareCommonAlpha` calls.
**Changes:**
- Moved `map` from the persistent `AlphaShareCommon.State` to a private
`State` used only within individual `shareCommonAlpha` calls.
- Replaced `PHashMap ExprPtr Expr` with (the more efficient)
`Std.HashMap ExprPtr Expr` for `map`, since it is now local to each call
and does not need persistence.
- The public `AlphaShareCommon.State` now only contains the `set` of
alpha-equivalent expressions that should persist
This PR adds functions for creating maximally shared terms from
maximally shared terms. It is more efficient than creating an expression
and then invoking `shareCommon`. We are going to use these functions for
implementing the symbolic simulation primitives.
This PR introduces `SymM`, a new monad for implementing symbolic
simulators (e.g., verification condition generators) in Lean. The monad
addresses performance issues found in symbolic simulators built on top
of user-facing tactics like `apply` and `intros`.
**Key features:**
- Goals are represented by `Grind.Goal` objects, enabling incremental
hypothesis processing
- No `revert` or `clear` operations, allowing O(1) local context checks
instead of O(n log n)
- Carries `GrindM` state across goals to avoid reprocessing shared
hypotheses
- Provides `mkGoal` for creating new goals within the monad
This is the foundational infrastructure for `SymM`. Future PRs will add
operations like `intro`, `apply`, and the optimized definitional
equality test.
This PR adds support for incrementally processing local declarations in
`grind`. Instead of processing all hypotheses at once during goal
initialization, `grind` now tracks which local declarations have been
processed via `Goal.nextDeclIdx` and provides APIs to process new
hypotheses incrementally.
This feature will be used by the new `SymM` monad for efficient symbolic
simulation.
This PR disables closed term extraction in the reflection terms used by
`bv_decide`. These terms do
not profit at all from closed term extraction but can in practice cause
thousands of new closed term
declarations which in turn slows down the compiler.
This PR improves the performance of and flattening in `bv_decide`.
The two main insights of this PR are:
1. When embedded constraint substitution is disabled it makes no sense
to have and flattening on in
the first place, given that we do not profit from it in any way.
2. The new fvars produced by and flattening can also be inserted into
the rewriting caches of the
preprocessing pipeline if the fvar they were derived from is already in
the cache. This
drastically decreases the amount of work we have to do in the second
rewriting pass after running
and flattening.
This PR adds the attributes `[grind norm]` and `[grind unfold]` for
controlling the `grind` normalizer/preprocessor.
The `norm` modifier instructs `grind` to use a theorem as a
normalization rule. That is, the theorem is applied during the
preprocessing step. This feature is meant for advanced users who
understand how the preprocessor and `grind`'s search procedure interact
with each other.
New users can still benefit from this feature by restricting its use to
theorems that completely eliminate a symbol from the goal. Example:
```lean
theorem max_def : max n m = if n ≤ m then m else n
```
For a negative example, consider:
```lean
opaque f : Int → Int → Int → Int
theorem fax1 : f x 0 1 = 1 := sorry
theorem fax2 : f 1 x 1 = 1 := sorry
attribute [grind norm] fax1
attribute [grind =] fax2
example (h : c = 1) : f c 0 c = 1 := by
grind -- fails
```
In this example, `fax1` is a normalization rule, but it is not
applicable to the input goal since `f c 0 c` is not an instance of `f x
0 1`. However, `f c 0 c` matches the pattern `f 1 x 1` modulo the
equality `c = 1`. Thus, `grind` instantiates `fax2` with `x := 0`,
producing the equality `f 1 0 1 = 1`, which the normalizer simplifies to
`True`. As a result, nothing useful is learned. In the future, we plan
to include linters to automatically detect issues like these. Example:
```lean
opaque f : Nat → Nat
opaque g : Nat → Nat
@[grind norm] axiom fax : f x = x + 2
@[grind norm ←] axiom fg : f x = g x
example : f x ≥ 2 := by grind
example : f x ≥ g x := by grind
example : f x + g x ≥ 4 := by grind
```
The `unfold` modifier instructs `grind` to unfold the given definition
during the preprocessing step. Example:
```lean
@[grind unfold] def h (x : Nat) := 2 * x
example : 6 ∣ 3*h x := by grind
```
This PR fixes a mismatch between the behavior of `foldlM` and
`foldlMUnsafe` in the three array
types. This mismatch is only exposed when manually specifying a `stop`
value greater than the size
of the array and only exploitable through `native_decide`.
The mismatch was introduced as part of
4ba21ea10c which introduced
`foldlMUnsafe` and thus likely a mistake when building the `unsafe`
implementation instead of a
specification mistake.
Closes#11773
This PR implements support for user-defined attributes at
`grind_pattern`. Suppose we have declared the `grind` attribute
```lean
register_grind_attr my_grind
```
Then, we can now write
```lean
opaque f : Nat → Nat
opaque g : Nat → Nat
axiom fg : g (f x) = x
grind_pattern [my_grind] fg => g (f x)
```
This PR uses the new support for user-defined `grind` attributes to
implement the default `[grind]` attribute.
A manual update-stage0 is required because it affects the .olean files.
This PR implements user-defined `grind` attributes. They are useful for
users that want to implement tactics using the `grind` infrastructure
(e.g., `progress*` in Aeneas). New `grind` attributes are declared using
the command
```lean
register_grind_attr my_grind
```
The command is similar to `register_simp_attr`. After the new attribute
is declared. Recall that similar to `register_simp_attr`, the new
attribute cannot be used in the same file it is declared.
```lean
opaque f : Nat → Nat
opaque g : Nat → Nat
@[my_grind] theorem fax : f (f x) = f x := sorry
example theorem fax2 : f (f (f x)) = f x := by
fail_if_success grind
grind [my_grind]
```
TODO: remove leftovers after update stage0
This PR allows `grind` to use `List.eq_nil_of_length_eq_zero` (and
`Array.eq_empty_of_size_eq_zero`), but only when it has already proved
the length is zero.
This PR moves the grind pattern from `Sublist.eq_of_length` to the
slightly more general `Sublist.eq_of_length_le`, and adds a grind
pattern guard so it only activates if we have a proof of the hypothesis.
This PR adds additional test coverage for #11758 (fix for #11745:
nonstandard instances in grind and simp +arith).
The existing test `grind_11745.lean` only covers Int LE with `grind
-order` and `lia -order`. This adds tests for:
- LT instances (Int and Nat)
- Nat LE instances
- Mixed canonical and non-canonical instances in the same goal
- Equality derived from two LE constraints
- `simp +arith` with non-canonical instances
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
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 fixes an issue where `grind` fails when trying to unfold a
definition by pattern matching imported by `import all` (or from a
non-`module`).
Fixes#11715
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR turns even more commonly used bv_decide theorems that require
unification into fast simprocs
using syntactic equality. This pushes the overall performance across
sage/app7 to <= 1min10s for
every problem.
This PR replaces `ffi.md` with links to the corresponding sections of
the manual, so we don't have to keep two documents up to date.
A corresponding reference manual PR re-synchronizes them:
https://github.com/leanprover/reference-manual/pull/714
This PR upstreams dependency-management commands from Mathlib:
- `#import_path Foo` prints the transitive import chain that brings
`Foo` into scope
- `assert_not_exists Foo` errors if declaration `Foo` exists (for
dependency management)
- `assert_not_imported Module` warns if `Module` is transitively
imported
- `#check_assertions` verifies all pending assertions are eventually
satisfied
These commands help maintain the independence of different parts of a
library by catching unintended transitive dependencies early.
### Example usage
```lean
-- Find out how Nat got into scope
#import_path Nat
-- Declaration Nat is imported via
-- Init.Prelude,
-- which is imported by Init.Coe,
-- which is imported by Init.Notation,
-- ...
-- which is imported by this file.
-- Assert that a declaration should not be in scope yet
assert_not_exists SomeAdvancedType
-- Assert that a module should not be imported
assert_not_imported Some.Heavy.Module
-- Verify all assertions are eventually satisfied
#check_assertions
```
Addresses
https://lean-fro.zulipchat.com/#narrow/channel/398861-general/topic/path.20of.20an.20import🤖 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 fixes an issue where `exact?` would not suggest private
declarations defined in the current module.
## Problem
When using `exact?` in a file with private declarations, those private
declarations were not being suggested even though they are valid and
accessible:
```lean
module
axiom P : Prop
private axiom p : P
example : P := by exact? -- error: could not find lemma
```
The problem was that `blacklistInsertion` in `LazyDiscrTree` was
filtering out all declarations whose names matched `isInternalDetail`,
which includes private names due to their `_private.Module.0.name`
structure.
## Solution
The fix adds a helper function `isPrivateNameOf` that checks if a
private declaration belongs to a specific module. The
`blacklistInsertion` function now allows private declarations belonging
to the current module (`env.header.mainModule`) to pass through the
filter.
Private declarations from imported modules are still filtered out, as
they may reference internal declarations that aren't accessible (which
would cause processing errors).
Zulip discussion:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60exact.3F.60.20and.20private.20declarations/near/564586152🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR introduces some additional lemmas around `BitVec.extractLsb'`
and `BitVec.extractLsb`.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This PR internalizes all arguments of Quot.lift during LCNF conversion,
preventing panics in certain
non trivial programs that use quotients.
Fixes#11719.
This PR improves the performance of the functions for generating
congruence lemmas, used by `simp`
and a few other components.
It is a followup to (though not dependent on) #11717 and improves the
performance of `bv_decide` on the benchmark
in question further down to 20 seconds (from 1min 23s in #11717 and 8min
originally). We are thus at approximately a 24x speedup from the
original run.
This PR improves the performance of `bv_decide`'s rewriter on large
problems.
The baseline for this PR is `QF_BV/sage/app7/bench_1222.smt2` on
`chonk3` at 8 minutes. After this
PR it takes about 1min and 23 seconds. This improvement is achieved by
turning frequently used simp
rules into simprocs in order to avoid spending time performing
unification to see if they are
applicable.
This PR renames the namespace `Std.Range` to `Std.Legacy.Range`. Instead
of using `Std.Range` and `[a:b]` notation, the new range type `Std.Rco`
and its corresponding `a...b` notation should be used. There are also
other ranges with open/closed/infinite boundary shapes in
`Std.Data.Range.Polymorphic` and the new range notation also works for
`Int`, `Int8`, `UInt8`, `Fin` etc.
This PR adds more MPL spec lemmas for all combinations of `for` loops,
`fold(M)` and the `filter(M)/filterMap(M)/map(M)` iterator combinators.
These kinds of loops over these combinators (e.g. `it.mapM`) are first
transformed into loops over their base iterators (`it`), and if the base
iterator is of type `Iter _` or `IterM Id _`, then another spec lemma
exists for proving Hoare triples about it using an invariant and the
underlying list (`it.toList`). The PR also fixes a bug that MPL always
assigns the default priority to spec lemmas if `Std.Tactic.Do.Syntax` is
not imported and a bug that low-priority lemmas are preferred about
high-priority ones.
For context, the MPL bug was related to the fact that the `Attr.spec`
syntax is not built-in. Therefore, Lean falls back to the `Attr.simple`
syntax, which *basically* also works, but which stores the priority at a
different position. The routine to extract the priority does not
consider this and so it falls back to the default priority given an
`Attr.simple` syntax object.
This PR improves the performance of autocompletion and fuzzy matching by
introducing an ASCII fast path into one of their core loops and making
Char.toLower/toUpper more efficient.
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR gives a focused error message when a user tries to name an
example, and tweaks error messages for attempts to define multiple
opaque names at once.
## Example errors
```
example x : 1 == 1 := by grind
```
Current message:
```
Failed to infer type of binder `x`
Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be
```
New message:
```
Failed to infer type of binder `x`
Note: Examples don't have names. The identifier `x` is being interpreted as a parameter `(x : _)`.
```
## Plural-aware identifier lists
Both the example errors and opaque errors understand pluralization and
use oxford commas.
```
opaque a b c : Nat
```
Current message:
```
Failed to infer type of binder `c`
Note: Multiple constants cannot be declared in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`.
```
New message:
```
Failed to infer type of binder `c`
Note: Multiple constants cannot be declared in a single declaration. The identifiers `b` and `c` are being interpreted as parameters `(b : _)` and `(c : _)`.```
This PR extends the get-elem tactic for ranges so that it supports
subarrays. Example:
```lean
example {a : Array Nat} (h : a.size = 28) : Id Unit := do
let mut x := 0
for h : i in *...(3 : Nat) do
x := a[1...4][i]
```
This PR avoids invoking TC synthesis and other inference mechanisms in
the simprocs of bv_decide. This can give significant speedups on
problems that pressure these simprocs.
This PR enables the specializer to also recursively specialize in some
non trivial higher order situations.
The main motivation for this change is the upcoming changes to do
notation by sgraf. In there he uses combinators such as
```lean
@[specialize, expose]
def List.newForIn {α β γ} (l : List α) (b : β) (kcons : α → (β → γ) → β → γ) (knil : β → γ) : γ :=
match l with
| [] => knil b
| a :: l => kcons a (l.newForIn · kcons knil) b
```
in programs such as
```lean
def testing :=
let x := 42;
List.newForIn (β := Nat) (γ := Id Nat)
[1,2,3]
x
(fun i kcontinue s =>
let x := s;
List.newForIn
[i:10].toList x
(fun j kcontinue s =>
let x := s;
let x := x + i + j;
kcontinue x)
kcontinue)
pure
```
inspecting this IR right before we get to the specializer in the current
compiler we get:
```
[Compiler.eagerLambdaLifting] size: 22
def testing : Nat :=
fun _f.1 _y.2 : Nat :=
return _y.2;
let x := 42;
let _x.3 := 1;
fun _f.4 i kcontinue s : Nat :=
fun _f.5 j kcontinue s : Nat :=
let _x.6 := Nat.add s i;
let x := Nat.add _x.6 j;
let _x.7 := kcontinue x;
return _x.7;
let _x.8 := 10;
let _x.9 := Nat.sub _x.8 i;
let _x.10 := Nat.add _x.9 _x.3;
let _x.11 := 1;
let _x.12 := Nat.sub _x.10 _x.11;
let _x.13 := Nat.mul _x.3 _x.12;
let _x.14 := Nat.add i _x.13;
let _x.15 := @List.nil _;
let _x.16 := List.range'TR.go _x.3 _x.12 _x.14 _x.15;
let _x.17 := @List.newForIn _ _ _ _x.16 s _f.5 kcontinue;
return _x.17;
let _x.18 := 2;
let _x.19 := 3;
let _x.20 := @List.nil _;
let _x.21 := @List.cons _ _x.19 _x.20;
let _x.22 := @List.cons _ _x.18 _x.21;
let _x.23 := @List.cons _ _x.3 _x.22;
let _x.24 := @List.newForIn _ _ _ _x.23 x _f.4 _f.1;
return _x.24
```
Here the `kcontinue` higher order functions pose a special challenge
because they delay the discovery of new specialization opportunities.
Inspecting the IR after the current specializer (and a cleanup simp
step) we get functions that look as follows:
```
[simp] size: 7
def List.newForIn._at_.testing.spec_0 i kcontinue l b : Nat :=
cases l : Nat
| List.nil =>
let _x.1 := kcontinue b;
return _x.1
| List.cons head.2 tail.3 =>
let _x.4 := Nat.add b i;
let x := Nat.add _x.4 head.2;
let _x.5 := List.newForIn._at_.testing.spec_0 i kcontinue tail.3 x;
return _x.5
[simp] size: 14
def List.newForIn._at_.List.newForIn._at_.testing.spec_1.spec_1 _x.1 l b : Nat :=
cases l : Nat
| List.nil =>
return b
| List.cons head.2 tail.3 =>
fun _f.4 x.5 : Nat :=
let _x.6 := List.newForIn._at_.List.newForIn._at_.testing.spec_1.spec_1 _x.1 tail.3 x.5;
return _x.6;
let _x.7 := 10;
let _x.8 := Nat.sub _x.7 head.2;
let _x.9 := Nat.add _x.8 _x.1;
let _x.10 := 1;
let _x.11 := Nat.sub _x.9 _x.10;
let _x.12 := Nat.mul _x.1 _x.11;
let _x.13 := Nat.add head.2 _x.12;
let _x.14 := @List.nil _;
let _x.15 := List.range'TR.go _x.1 _x.11 _x.13 _x.14;
let _x.16 := List.newForIn._at_.testing.spec_0 head.2 _f.4 _x.15 b;
return _x.16
```
Observe that the specializer decided to abstract over `kcontinue`
instead of specializing further recursively. Thus this tight loop is now
going through an indirect call.
This PR now changes the specializer somewhat fundamentally to handle
situations like this. The most notable change is going to a fixpoint
loop of:
1. Specialize all current declarations in the worklist
2. If a declaration
- succeeded in specializing run the simplifier on it and put it back
onto the worklist
- if it didn't don't put it back onto the worklist anymore
3. Put all newly generated specialisations on the worklist
4. Recompute fixed parameters for the current SCC
5. Repeat until the worklist is empty
Furthermore, declarations that were already specialized:
- only consider `fixedHO` parameters for specialization, in order to
avoid termination issues with repeated specialization and abstraction of
type class parameters under binders
- recursively specialized declarations only allow specialization if at
least one of their fixedHO arguments is not a parameter itself. The
reason for allowing this in first generation specialization is that we
refrain from specializing inside the body of a declaration marked as
`@[specialize]`. Thus we need to specialize them even if their arguments
don't actually contain anything of interest in order to ensure that type
classes etc. are correctly cleaned up within their bodies.
There is one last trade-off to consider. When specializing code
generated by the new do elaborator we sometimes generate intermediate
specializations that are not actually part of any call graph after we
are done specializing. We could in principle detect these functions and
delete them but having them in cache is potentially helpful for further
specializations later. Once the new do elaborator lands we plan to test
this trade-off.
Closes#10924
This PR provides many lemmas about `Int` ranges, in analogy to those
about `Nat` ranges. A few necessary basic `Int` lemmas are added. The PR
also removes `simp` annotations on `Rcc.toList_eq_toList_rco`,
`Nat.toList_rcc_eq_toList_rco` and consorts.
This PR adds the definition of `BitVec.cpop`, which relies on the more
general `BitVec.cpopNatRec`, and build some theory around it. The name
`cpop` aligns with the [RISCV ISA
nomenclature](https://msyksphinz-self.github.io/riscv-isadoc/#_cpop).
Co-authored-by: @tobiasgrosser, @bollu
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Siddharth <siddu.druid@gmail.com>
This PR makes it possible to verify loops over iterators. It provides
MPL spec lemmas about `for` loops over pure iterators. It also provides
spec lemmas that rewrite loops over `mapM`, `filterMapM` or `filterM`
iterator combinators into loops over their base iterator.
This PR refactors match compilation, to handle “side-effect free”
patterns (`.var`, `.inaccessible`, `.as`) eagerly and for each
alternative separately. The idea is that there should be less interplay
between different alternatives, and prepares the ground for #11105.
This may cause some corner case match statements to compiler or fail
compile that behaved differently before. For example, it can now use a
sparse case where previously was using a full case, and pattern
completeness may not be clear to lean now. On the other hand, using a
sparse case can mean that match statements mixing matching in indicies
with matching on the indexed datatype can work.
This PR removes the unnecessary check for the batteries
`nightly-testing-YYYY-MM-DD` tag that blocks mathlib CI from running.
## Problem
Currently, when fixing mathlib's nightly-testing branch, the workflow
requires BOTH batteries and mathlib to have `nightly-testing-YYYY-MM-DD`
tags before mathlib CI can run on lean4 PRs. This creates a false
dependency:
1. Fix mathlib nightly-testing (including fixing batteries build)
2. Mathlib CI succeeds → creates mathlib tag → advances
`nightly-with-mathlib`
3. But batteries test suite fails → no batteries tag created
4. lean4 PR can't run mathlib CI because batteries tag doesn't exist
5. Bot suggests rebasing onto `nightly-with-mathlib`, but this doesn't
help
## Solution
Remove the batteries tag check because:
- Mathlib CI already depends on batteries (builds it as a dependency)
- If batteries is broken, mathlib CI will detect it
- The batteries testing branch creation already has fallback logic
(falls back to `nightly-testing` branch if tag doesn't exist)
This allows mathlib CI to run as soon as mathlib is ready, which is the
actual blocker.
See discussion at
https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20status.20updates/near/564136025🤖 Prepared with Claude Code
Co-authored-by: Claude Sonnet 4.5 <noreply@anthropic.com>
This PR fixes `grind` to support dot notation on declarations in the
lemma list.
When using `grind only [foo.le]` where `foo.le` is dot notation applying
`LT.lt.le` to a theorem `foo`, grind previously failed with "Unknown
constant `foo.le`" because it tried to look up `foo.le` as a constant
name rather than elaborating it as a term.
The fix adds a fallback in `processParam`: when constant lookup fails,
it now falls back to `processTermParam` which elaborates the identifier
as a term. This allows dot notation expressions like `log_two_lt_d9.le`
to work correctly.
Closes#11690🤖 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 adds the new operation `MonadAttach.attach` that attaches a
proof that a postcondition holds to the return value of a monadic
operation. Most non-CPS monads in the standard library support this
operation in a nontrivial way. The PR also changes the `filterMapM`,
`mapM` and `flatMapM` combinators so that they attach postconditions to
the user-provided monadic functions passed to them. This makes it
possible to prove termination for some of these for which it wasn't
possible before. Additionally, the PR adds many missing lemmas about
`filterMap(M)` and `map(M)` that were needed in the course of this PR.
This PR improves `match` generalization such that it abstracts
metavariables in types of local variables and in the result type of the
match over the match discriminants. Previously, a metavariable in the
result type would silently default to the behavior of `generalizing :=
false`, and a metavariable in the type of a free variable would lead to
an error (#8099). Example of a `match` that elaborates now but
previously wouldn't:
```lean
example (a : Nat) (ha : a = 37) :=
(match a with | 42 => by contradiction | n => n) = 37
```
This is because the result type of the `match` is a metavariable that
was not abstracted over `a` and hence generalization failed; the result
is that `contradiction` cannot pick up the proof `ha : 42 = 37`.
The old behavior can be recovered by passing `(generalizing := false)`
to the `match`.
Furthermore, programs such as the following can now be elaborated:
```lean
example (n : Nat) : Id (Fin (n + 1)) :=
have jp : ?m := ?rhs
match n with
| 0 => ?jmp1
| n + 1 => ?jmp2
where finally
case m => exact Fin (n + 1) → Id (Fin (n + 1))
case jmp1 => exact jp ⟨0, by decide⟩
case jmp2 => exact jp ⟨n, by omega⟩
case rhs => exact pure
```
This is useful for the `do` elaborator.
Fixes#8099.
This PR makes `simpH`, used in the match equation generator, produce a
proof term. This is in preparation for a bigger refactoring in #11512.
This removes some cases, these are no longer necessary since #11196.
This PR fixes an inconsistency in the way Lake and Lean view the
transitivity of a `meta import`. Lake now works as Lean expects and
includes the meta segment of all transitive imports of a `meta import`
in its transitive trace.
This PR adds the `Context` type for cancellation with context
propagation. It works by storing a tree of forks of the main context,
providing a way to control cancellation.
This PR changes the "declaration uses 'sorry'" warning to use backticks
instead of single quotes, consistent with Lean's conventions for
formatting code identifiers in diagnostic messages.
Fix a typo in the error message when an unknown role is used in a
docstring.
- Changes "Unkown role" to "Unknown role" in
`src/Lean/Elab/DocString.lean`
This PR fixes the `grind` support for `Nat.ctorIdx`. Nat constructors
appear in `grind` as offsets or literals, and not as a node marked
`.constr`, so handle that case as well.
This PR moves many constants of the iterator API from `Std.Iterators` to
the `Std` namespace in order to make them more convenient to use. These
constants include, but are not limited to, `Iter`, `IterM` and
`IteratorLoop`. This is a breaking change. If something breaks, try
adding `open Std` in order to make these constants available again. If
some constants in the `Std.Iterators` namespace cannot be found, they
can be found directly in `Std` now.
This PR adds a CI step that fails if the `src/stdlib_flags.h` file was
modified, to alert PR authors that they most likely wanted to modify
`stage0/src/stdlib_flags.h` instead.
This PR adds basic support for equality propagation in `grind linarith`
for the `IntModule` case. This covers only the basic case. See note in
the code.
We remark this feature is irrelevant for `CommRing` since `grind ring`
already has much better support for equality propagation.
This PR fixes an issue where a `by` in the public scope could create an
auxiliary theorem for the proof whose type does not match the expected
type in the public scope.
Fixes#11672
This PR adds support for `Nat.cast` in `grind linarith`. It now uses
`Grind.OrderedRing.natCast_nonneg`. Example:
```lean
open Lean Grind Std
attribute [instance] Semiring.natCast
variable [Lean.Grind.CommRing R] [LE R] [LT R] [LawfulOrderLT R] [IsLinearOrder R] [OrderedRing R]
example (a : Nat) : 0 ≤ (a : R) := by grind
example (a b : Nat) : 0 ≤ (a : R) + (b : R) := by grind
example (a : Nat) : 0 ≤ 2 * (a : R) := by grind
example (a : Nat) : 0 ≥ -3 * (a : R) := by grind
```
This PR fixes the `grind` pattern validator. It covers the case where an
instance is not tagged with the implicit instance binder. This happens
in declarations such as
```lean
ZeroMemClass.zero_mem {S : Type} {M : outParam Type} {inst1 : Zero M} {inst2 : SetLike S M}
[self : @ZeroMemClass S M inst1 inst2] (s : S) : 0 ∈ s
```
This PR adds explicit guidance to the `/release` command that Claude
should never merge PRs autonomously during the release process - always
wait for the user to do it.
🤖 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 adds support for `Int.sign`, `Int.fdiv`, `Int.tdiv`, `Int.fmod`,
`Int.tmod`, and `Int.bmod` to `grind`. These operations are just
preprocessed away. We assume that they are not very common in practice.
Examples:
```lean
example {x y : Int} : y = 0 → (x.fdiv y) = 0 := by grind
example {x y : Int} : y = 0 → (x.tdiv y) = 0 := by grind
example {x y : Int} : y = 0 → (x.fmod y) = x := by grind
example {x y : Int} : y = 1 → (x.fdiv (2 - y)) = x := by grind
example {x : Int} : x > 0 → x.sign = 1 := by grind
example {x : Int} : x < 0 → x.sign = -1 := by grind
example {x y : Int} : x.sign = 0 → x*y = 0 := by grind
```
See #11622
This PR adds propagation rules corresponding to the `Semiring`
normalization rules introduced in #11628. The new rules apply only to
non-commutative semirings, since support for them in `grind` is limited.
The normalization rules introduced unexpected behavior in Mathlib
because they neutralize parameters such as `one_mul`: any theorem
instance associated with such a parameter is reduced to `True` by the
normalizer.
This PR teaches `grind` how to reduce `.ctorIdx` applied to
constructors. It can also handle tasks like
```
xs ≍ Vec.cons x xs' → xs.ctorIdx = 1
```
thanks to a `.ctorIdx.hinj` theorem (generated on demand).
This PR fixes a SIGFPE crash on x86_64 when evaluating `INT_MIN / -1` or
`INT_MIN % -1` for signed integer types.
On x86_64, the `idiv` instruction traps when the quotient overflows the
destination register. For signed integers, `INT_MIN / -1` produces a
result that overflows (e.g., `-2147483648 / -1 = 2147483648` which
doesn't fit in Int32). ARM64's `sdiv` instruction wraps instead of
trapping.
The fix:
- For Int8/Int16/Int32: widen to the next larger type before
dividing/modding, then truncate back
- For Int64: explicitly check for the overflow case and return the
wrapped result
Fixes#11612🤖 Prepared with Claude Code
This PR fixes a typo in the docstring of `LeanLibConfig.defaultFacets`
and the Lake README that erroneously referred to `LeanLib.sharedLib`
instead of `LeanLib.sharedFacet`.
See e.g. `tests/lake/tests/targets/lakefile.lean` to verify that
`LeanLib.sharedFacet` is correct usage; `LeanLib.sharedLib` does not
exist.
This PR adds support for `BitVec.ofNat` in `grind lia`. Example:
```lean
example (x y : BitVec 8) : y < 254#8 → x > 2#8 + y → x > 1#8 + y := by
grind
```
This PR implements a linter that warns when a deprecated coercion is
applied. It also warns when the `Option` coercion or the
`Subarray`-to-`Array` coercion is used in `Init` or `Std`. The linter is
currently limited to `Coe` instances; `CoeFun` instances etc. are not
considered.
The linter works by collecting the `Coe` instance declaration names that
are being expanded in `expandCoe?` and storing them in the info tree.
The linter itself then analyzes the info tree and checks for banned or
deprecated coercions.
This PR ensures the pattern normalizer used in `grind` does violate
assumptions made by the gadgets `Grind.genPattern` and
`Grind.getHEqPattern`.
Closes#11633
This PR adjusts the new `meta` keyword of the experimental module system
not to imply `partial` for general consistency.
As the previous behavior can create confusion return types that are not
known to be `Nonempty` and few `def`s should be `meta` in the first
case, this special case does not appear to be worth the minor
convenience.
This PR adds BEq instance for `DTreeMap`/`TreeMap`/`TreeSet` and their
extensional variants and proves lemmas relating it to the equivalence of
hashmaps/equality of extensional variants.
Stacked on top of #11266
This PR adds `@[suggest_for ℤ]` on `Int` and `@[suggest_for ℚ]` on
`Rat`, following the pattern established by `@[suggest_for ℕ]` on `Nat`
in #11554.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR causes Lean to search through `@[suggest_for]` annotations on
certain errors that look like unknown identifiers that got incorrectly
autobound. This will correctly identify that a declaration of type
`Maybe String` should be `Option String` instead.
## Example
```
example : Except String Unit := return .ok ()
```
```
Function expected at
Result
but this term has type
?m.1
Note: Expected a function because this term is being applied to the argument
String
Hint: The identifier `Result` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
Perhaps you meant `Except` in place of `Result`?
```
The last line is added by this PR.
This PR allows Lean to present suggestions based on `@[suggest_for]`
annotations for unknown identifiers without internal dots. (The
annotations in #11554 only gave suggestion for dotted identifiers like
`Array.every`->`Array.all` and not for bare identifiers like
`Result`->`Except` or `ℕ`->`Nat`.)
This PR makes argument-less tactic invokations of `Std.Do` tactics such
as `mintro` emit a proper error message "`mintro` expects at least one
pattern" instead of claiming that `Std.Tactic.Do` needs to be imported.
Closes#11509.
This PR ensures we apply the ring normalizer to equalities being
propagated from the `grind` core module to `grind lia`. It also ensures
we use the safe/managed polynomial functions when normalizing.
Closes#11539
This PR improves the case-split heuristics in `grind`. In this PR, we do
not increment the number of case splits in the first case. The idea is
to leverage non-chronological backtracking: if the first case is solved
using a proof that doesn't depend on the case hypothesis, we backtrack
and close the original goal directly. In this scenario, the case-split
was "free", it didn't contribute to the proof. By not counting it, we
allow deeper exploration when case-splits turn out to be irrelevant.
The new heuristic addresses the second example in #11545
This PR removes the old ElimDeadBranches pass and shifts the new one
past lambda lifting.
The reason for dropping the old one is its general unsoundness and the
fact that we want to do refactorings on the IR part. The reason for
shifting the current pass past lambda lifting, is that its analysis is
imprecise in the presence of local function symbols. I experimented with
the exact placement for a while and it seems like it is optimal here.
Overall we observe a slight regression in the amount of C code
generated, likely because we don't propagate information into lambdas
before lifting them anymore. But generally measure a slight performance
improvement in general.
This PR fixes how theorems without parameters are handled in `grind`.
This is a better fix than #11579
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR moves Lake's `tests/lake/examples/targets` test from `examples`
to `tests` (and thus disabling it by default).
It is being
[flaky](https://github.com/leanprover/lean4/actions/runs/20111185289/attempts/1)
for some unknown reason, so I am disabling until I have a better
opportunity to debug it.
This PR ensures that ground theorems are properly handled as `grind`
parameters. Additionally, `grind [(thm)]` and `grind [thm]` should be
handled the same way.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR fixes `grind?` to include term parameters (like `[show P by
tac]`) in its suggestions. Previously, these were being dropped because
term arguments are stored in `extraFacts` and not tracked via E-matching
like named lemmas.
For example, `grind? [show False by exact h]` now correctly suggests
`grind only [show False by exact h]` instead of just `grind only`.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds a `+all` option to `exact?` and `apply?` that collects all
successful lemmas instead of stopping at the first complete solution.
When `+all` is enabled:
- `exact?` shows all lemmas that completely solve the goal (admits the
goal with `sorry`)
- `apply?` shows all lemmas including both complete and partial
solutions
🤖 Prepared with Claude Code
<!-- CURSOR_SUMMARY -->
---
> [!NOTE]
> Adds a +all flag to exact? and apply? to collect all successful
lemmas, updates library search to support aggregation and proper
star-lemma fallback, and extends the discriminator tree to
extract/append dropped entries; includes tests.
>
> - **Tactics / UI**:
> - Add `LibrarySearchConfig.all` and `+all` flag to `exact?`/`apply?`
to collect all successful lemmas.
> - `exact?` now aggregates complete solutions (via
`addExactSuggestions`); `apply?` shows both complete and partial
suggestions.
> - Updated help texts and error/hint messages.
> - **Library Search Core (`Lean.Meta.Tactic.LibrarySearch`)**:
> - Thread new `collectAll` option through `tryOnEach`,
`librarySearch'`, and `librarySearch`.
> - `tryOnEach` continues collecting complete solutions when `collectAll
= true`.
> - Star-lemma fallback now runs even when primary search yields only
partial results; include complete solutions when aggregating.
> - Cache and retrieve star-indexed lemmas via
`droppedEntriesRef`/`getStarLemmas`.
> - **Lazy Discriminator Tree (`Lean.Meta.LazyDiscrTree`)**:
> - Add `extractKey(s)`/`collectSubtreeAux` to extract and drop entries,
returning them.
> - Modify import/module tree building to optionally append dropped
entries to a shared ref (for star-lemmas), and pass this through
`findMatches`/`createModuleTreeRef`.
> - Minor comment/logic tweaks (append vs set) when handling dropped
entries.
> - **Elaboration (`Lean.Elab.Tactic.LibrarySearch`)**:
> - Integrate `collectAll` into `exact?`/`apply?`; partition and present
complete vs incomplete suggestions; admit goals appropriately when
aggregating.
> - **Tests**:
> - Update existing expectations and add
`tests/lean/run/library_search_all.lean` to verify `+all`, aggregation,
and star-lemma behavior.
>
> <sup>Written by [Cursor
Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit
cbfc9313af. This will update automatically
on new commits. Configure
[here](https://cursor.com/dashboard?tab=bugbot).</sup>
<!-- /CURSOR_SUMMARY -->
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR documents that tests in `tests/lean/run/` run with
`-Dlinter.all=false`, and explains how to enable specific linters when
testing linter behavior.
🤖 Prepared with Claude Code
This PR fixes `grind` rejecting dot notation terms, mistaking them for
local hypotheses.
When a grind parameter like `n.triv` is given, where `n` is a local
variable and `triv` is a theorem that takes `n` as an argument (so
`n.triv` means `Nat.triv n`), grind was incorrectly rejecting it with
"redundant parameter" because it detected that the identifier resolved
to a local variable via `resolveLocalName`.
The fix checks if `resolveLocalName` returns field projections
(non-empty list), indicating dot notation. In that case, we process the
parameter as a term expression to let elaboration resolve the dot
notation properly, rather than trying to resolve it as a global constant
name.
### Minimal reproducer
```lean
theorem Nat.triv (n : Nat) : n = n := rfl
example (n : Nat) : n = n := by
grind [n.triv] -- Previously: "redundant parameter `n.triv`"
```
This also fixes the issue where `grind [x.exp_pos]` was rejected even
though `x.exp_pos` elaborates to `Real.exp_pos x`, a valid theorem
application.
🤖 Prepared with Claude Code
This PR adds missing lemmas about how `ReaderT.run`, `OptionT.run`,
`StateT.run`, and `ExceptT.run` interact with `MonadControl` operations.
This also leaves some comments noting that the lemmas may look less
general than expected; but this is because the instances are also not
very general.
This PR fixes an issue where `grind` did not display deprecation
warnings when deprecated lemmas were used in its argument list.
The fix adds explicit calls to `Linter.checkDeprecated` after resolving
theorem names in both `processParam` (for theorem arguments) and
`elabGrindParams` (for the `-` erase syntax).
Closes#11582🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds a lemma that the cast of a natural number into any ordered
ring is non-negative. We can't annotate this directly for `grind`, but
will probably add this to `grind`'s linarith interrnals.
This PR adds `@[suggest_for]` annotations to Lean, allowing lean to
provide corrections for `.every` or `.some` methods in place of `.all`
or `.any` methods for most default-imported types (arrays, lists,
strings, substrings, and subarrays, and vectors).
Due to the need for stage0 updates for new annotations, the
`suggest_for` annotation itself was introduced in previous PRs: #11367,
#11529, and #11590.
## Example
```
example := "abc".every (! ·.isWhitespace)
```
Error message:
```
Invalid field `every`: The environment does not contain `String.every`, so it is not possible to project the field `every` from an expression
"abc"
of type `String`
Hint: Perhaps you meant `String.all` in place of `String.every`:
.e̵v̵e̵r̵y̵a̲l̲l̲
```
(the hint is added by this PR)
## Additional changes
Adds suggestions that are not currently active but that can be used to
generate autocompletion suggestions in the reference manual:
- `Either` -> `Except` and `Sum`
- `Exception` -> `Except`
- `ℕ` -> `Nat`
- `Nullable` -> `Option`
- `Maybe` -> `Option`
- `Optional` -> `Option`
- `Result` -> `Except`
This PR switches the way olean files store identifier suggestions. The
ordering introduced in #11367 and #11529 made sense if we were only
storing incorrect -> correct mappings, but for the reference manual we
want to store the correct -> incorrect mappings as well, and so it is
more sensible to store just the correct -> incorrect mapping that mimics
the author-generated data better.
Also tweaks error messages further in preparation for public-facing
@[suggest_for] annotations and forbids suggestions on non-public names.
Does not make generally-visible changes as there are no introduced uses
of @[suggest_for] annotations yet.
These complement the existing `ExceptT.mk` and `OptionT.mk`, and provide
a symbol to key `simp` lemmas on, to prevent getting stuck on
`StateT.run (fun s => f s) s`.
A future PR could insert these new `mk`s into the implementation of many
definitions, such that unfolding the definitions leaves appropriate
casts behind; but this is invasive, and by itself having `mk` provides
value.
This PR improves indexing for `grind` patterns. We now include symbols
occurring in nested ground patterns. This important to minimize the
number of activated E-match theorems.
This PR makes the noConfusion principles even more heterogeneous, by
allowing not just indices but also parameters to be differ.
This is a breaking change for manual use of `noConfusion` for types with
parameters. Pass suitable `rfl` arguments, and use `eq_of_heq` on the
resulting equalities as needed.
This fixes#11560.
This PR adds `BEq` instance for `DHashMap`/`HashMap`/`HashSet` and their
extensional variants and proves lemmas relating it to the equivalence of
hashmaps/equality of extensional variants.
This PR allows projections on `tagged` values in the IR type system.
While executing this branch of code should indeed never happen in
practice, enforcing this through
the type system would require the compiler to always optimize code to
the point where this is not
possible. For example in the code:
```
cases x with
| none => ....
| some =>
let val : obj := proj[0] x
...
```
static analysis might learn that `x` is always none and transform this
to:
```
let x : tagged := none
cases x with
| none => ....
| some =>
let val : obj := proj[0] x
...
```
Which would be type incorrect if projections on `tagged` were
illegitimate. However, we don't want
to force static analysis to always simplify code far enough on its own
to enforce this invariant.
This PR prevents `try` swallowing heartbeat errors from nested `simp`
calls, and more generally ensures the `isRuntime` flag is propagated by
`throwNestedTacticEx`. This prevents the behavior of proofs (especially
those using `aesop`) being affected by the current recursion depth or
heartbeat limit.
This breaks a single caller in Mathlib where `simp` uses a lemma of the
form `x = f (g x)` and stack overflows, which can be fixed by
generalizing over `g x`.
Closes#7811.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR fixes the tactic framework reporting file progress bar ranges
that cover up progress inside tactic blocks nested in tactic
combinators. This is a purely visual change, incremental re-elaboration
inside supported combinators was not affected.
Also adds a test though it is not elaborate enough to test proper timing
of progress events per se; see moddoc there.

This PR scans the environment for viable replacements for a dotted
identifier (like `.zero`) and suggests concrete alternatives as
replacements.
## Example
```
#example .zero
```
Error message:
```
Invalid dotted identifier notation: The expected type of `.cons` could not be determined
```
Additional hint added by this PR:
```
Hint: Using one of these would be unambiguous:
[apply] `BitVec.cons`
[apply] `List.cons`
[apply] `List.Lex.cons`
[apply] `List.Pairwise.cons`
[apply] `List.Perm.cons`
[apply] `List.Sublist.cons`
[apply] `List.Lex.below.cons`
[apply] `List.Pairwise.below.cons`
[apply] `List.Perm.below.cons`
[apply] `List.Sublist.below.cons`
[apply] `Lean.Grind.AC.Seq.cons`
```
## Additional changes
This PR also brings several related error message descriptions and code
actions more in line with each other, changing several "Suggested
replacement: " code actions to the more common "Change to " wording, and
sorts suggestions obtained from searching the context by the default
sort for Names (which prefers names with fewer segments).
This PR adds some information to Grove: a check that all
string/slice-transforming functions are tracked properly (which finds
dozens of missed cases), and some documentation of design designs around
naming in the string library.
The PR also bumps the Grove version to the latest version which contains
many new features and also processes the data a lot faster (40s to 2.5s
for the test project).
This PR ensures that `Nat`s in `.olean` files use a deterministic
serialization in the case where `LEAN_USE_GMP` is not set.
This is a simplified version of
https://github.com/leanprover/lean4/pull/2908.
This PR reviews the docstrings for `Std.Do` that will appear in the Lean
reference manual and adds those that were missing.
---------
Co-authored-by: Sebastian Graf <sgraf1337@gmail.com>
This PR adds a workspace-index to the name of the package used by build
target. To clarify the distinction between the different uses of a
package's name, this PR also deprecates `Package.name` for more
use-specific variants (e.g., `Package.keyName`, `Package.prettyName`,
`Package.origName`).
More to come. (WIP)
This PR introduces a new fixpoint combinator,
`WellFounded.extrinsicFix`. A termination proof, if provided at all, can
be given extrinsically, i.e., looking at the term from the outside, and
is only required if one intends to formally verify the behavior of the
fixpoint. The new combinator is then applied to the iterator API.
Consumers such as `toList` or `ForIn` no longer require a proof that the
underlying iterator is finite. If one wants to ensure the termination of
them intrinsically, there are strictly terminating variants available
as, for example, `it.ensureTermination.toList` instead of `it.toList`.
This PR introduces the new `tagged_return` attribute. It allows users to
mark `extern` declarations to be guaranteed to always return `tagged`
return values. Unlike with `object` or `tobject` the compiler does not
emit reference counting operations for them. In the future information
from this attribute will be used for a more powerful analysis to remove
reference counts when possible.
This PR ensures the auxiliary definitions created by
`register_try?_tactic` are internal implementation details that should
not be visible to user-facing linters.
🤖 Generated with Claude Code
This PR adds support for underscores as digit separators in
String.toNat?, String.toInt?, and related parsing functions. This makes
the string parsing functions consistent with Lean's numeric literal
syntax, which already supports underscores for readability (e.g.,
100_000_000).
The implementation validates that underscores:
- Cannot appear at the start or end of the number
- Cannot appear consecutively
- Are ignored when calculating the numeric value
This resolves a common source of friction when parsing user input from
command-line arguments, environment variables, or configuration files,
where users naturally expect to use the same numeric syntax they use in
source code.
## Examples
Before:
```lean
#eval "100_000_000".toNat? -- none
```
After:
```lean
#eval "100_000_000".toNat? -- some 100000000
#eval "1_000".toInt? -- some 1000
#eval "-1_000_000".toInt? -- some (-1000000)
```
## Testing
Added comprehensive tests in
`tests/lean/run/string_toNat_underscores.lean` covering:
- Basic underscore support
- Edge cases (leading/trailing/consecutive underscores)
- Both `toNat?` and `toInt?` functions
- String, Slice, and Substring types
All existing tests continue to pass.
Closes#11538🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Sonnet 4.5 <noreply@anthropic.com>
This PR makes it so that in the issue template a line about how to check
boxes is in comment form you can only see it when you are creating the
issue and it does not need to be displayed to everyone.
Hi, these are just some spelling corrections.
There is one I wasn't completely sure about in
src/Init/Data/List/Lemmas.lean:
> See also
> ...
> Also
> \* \`Init.Data.List.Monadic\` for **addiation** _(additional?)_ lemmas
about \`List.mapM\` and \`List.forM\`
This PR fixes a syntax-pattern-matching issue from #11367 that prevented
the addition of suggestions in Init prior to Lean.Parser being
introduced, which was a significant shortcoming. It preserves the
ability to have multiple suggestions for one annotation later in the
process.
Additionally, tweaks a (not-yet-user-visible) error message and modifies
the attribute declaration to store a wrongIdentifier ->
correctIdentifier mapping instead of a correctIdentifier ->
wrongIdentifier mapping.
This PR makes the LCNF simplifier eliminate cases where all alts are
`.unreach` to just an `.unreach`.
an `.unreach`
We considered dropping a cases in a situation like this but decided
against it because it might hinder reuse.
```
def test x : Bool :=
cases x : Bool
| Except.error a.1 =>
⊥
| Except.ok a.2 =>
let _x.3 := true;
return _x.3
```
This PR avoids generating hyps when not needed (i.e. if there is a
catch-all so no completeness checking needed) during matching on values.
This tweak was made possible by #11220.
This PR adds a difference operation on
`ExtDTreeMap`/`ExtTreeMap`/`TreeSet` and proves several lemmas about it.
Stacked on top of #11407
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
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
> ```
This PR implements `grind` propagators for `Nat` operators that have a
simproc associated with them, but do not have any theory solver support.
Examples:
```lean
example (a b : Nat) : a = 3 → b = 6 → a &&& b = 2 := by grind
example (a b : Nat) : a = 3 → b = 6 → a ||| b = 7 := by grind
example (a b : Nat) : a = 3 → b = 6 → a ^^^ b = 5 := by grind
example (a b : Nat) : a = 3 → b = 6 → a <<< b = 192 := by grind
example (a b : Nat) : a = 1135 → b = 6 → a >>> b = 17 := by grind
```
Closes#11498
This PR marks `Nat` power and divisibility theorems for `grind`. We use
the new `grind_pattern` constraints to control theorem instantiation.
Examples:
```lean
example {x m n : Nat} (h : x = 4 ^ (m + 1) * n) : x % 4 = 0 := by
grind
example (a m n o p : Nat) : a ∣ n → a ∣ m * n * o * p := by
grind
example {a b x m n : Nat}
: n > 0 → x = b * 4^m * a → a = 9^n → m > 0 → x % 6 = 0 := by
grind
example {a n : Nat}
: m > 4 → a = 2^(m^n) → a % 2 = 0 := by
grind
```
Closes#11515
Remark: We are adding support for installing extra theorems to `lia`
(aka `cutsat`). The example at #11515 can already be solved by `grind`
with this PR, but we still need to add the new theorems to the set for
`lia`.
cc @kim-em
This PR provides an additional hint when the type of an autobound
implicit is required to have function type or equality type — this
fails, and the existing error message does not address the fact that the
source of the error is an unknown identifier that was automatically
bound.
## Example
```
import Lean
example : MetaM String := pure ""
```
Current error message:
```
Function expected at
MetaM
but this term has type
?m
Note: Expected a function because this term is being applied to the argument
String
```
Additional error message provided by this PR:
```
Hint: The identifier `MetaM` is unknown, and Lean's `autoImplicit` option
causes an unknown identifier to be treated as an implicitly bound variable
with an unknown type. However, the unknown type cannot be a function, and a
function is what Lean expects here. This is often the result of a typo or a
missing `import` or `open` statement.
```
This PR re-enables star-indexed lemmas as a fallback for `exact?` and
`apply?`.
Star-indexed lemmas (those with overly-general discrimination tree keys
like `[*]`)
were previously dropped entirely for performance reasons. This caused
useful lemmas
like `Empty.elim`, `And.left`, `not_not.mp`, `Sum.elim`, and
`Function.mtr` to be
unfindable by library search.
The implementation adds a two-pass search strategy:
1. First, search using concrete discrimination keys (the current
behavior)
2. If no results are found, fall back to trying star-indexed lemmas
The star-indexed lemmas are extracted during tree initialization and
cached in an
environment extension, avoiding repeated computation.
Users can disable the fallback with `-star`:
```lean
example {α : Sort u} (h : Empty) : α := by apply? -star -- error: no lemmas found
example {α : Sort u} (h : Empty) : α := by apply? -- finds Empty.elim
```
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds support for the difference operation for
`ExtDHashMap`/`ExtHashMap`/`ExtHashSet` and proves several lemmas about
it.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR changes how match splitters are generated: Rather than rewriting
the match statement, the match compilation pipeline is used again.
The benefits are:
* Re-doing the match compilation means we can do more intelligent book
keeping, e.g. prove overlap assumptions only once and re-use the proof,
or prune the context of the MVar to speed up `contradiction`. This may
have allowed a different solution than #11200.
* It would unblock #11105, as the existing splitter implementation would
have trouble dealing with the matchers produced that way.
* It provides the necessary machinery also for source-exposed “none of
the above” bindings, a feature that we probably want at some point (and
we mostly need to find good syntax for, see #3136, although maybe I
should open a dedicated RFC).
* It allows us to skip costly things during matcher creation that would
only be useful for the splitter, and thus allows performance
improvements like #11508.
* We can drop the existing implementation.
It’s not entirely free:
* We have to run `simpH` twice, once for the match equations and once
for the splitter.
This PR introduces a new annotation that allows definitions to describe
plausible-but-wrong name variants for the purpose of improving error
messages.
This PR just adds the notation and extra functionality; a stage0 update
will allow standard Lean functions to have suggestion annotations.
(Hence the changelog-no tag: this should go in the changelog when some
preliminary annotations are actually added.)
## Example
```lean4
inductive MyBool where | tt | ff
attribute [suggest_for MyBool.true] MyBool.tt
attribute [suggest_for MyBool.false] MyBool.ff
@[suggest_for MyBool.not]
def MyBool.swap : MyBool → MyBool
| tt => ff
| ff => tt
/--
error: Unknown constant `MyBool.true`
Hint: Perhaps you meant `MyBool.tt` in place of `MyBool.true`:
M̵y̵B̵o̵o̵l̵.̵t̵r̵u̵e̵M̲y̲B̲o̲o̲l̲.̲t̲t̲
-/
#guard_msgs in
example := MyBool.true
/--
error: Invalid field `not`: The environment does not contain `MyBool.not`, so it is not possible to project the field `not` from an expression
MyBool.tt
of type `MyBool`
Hint: Perhaps you meant one of these in place of `MyBool.not`:
[apply] `MyBool.swap`: MyBool.tt.swap
-/
#guard_msgs in
example := MyBool.tt.not
```
This PR marks `Char -> Bool` patterns as default instances for string
search. This means that things like `" ".find (·.isWhitespace)` can now
be elaborated without error.
Previously, it was necessary to write `" ".find Char.isWhitespace`.
Thank you to David Christiansen for the idea of using a default
instance.
This PR gives suggestions based on the currently-available constants
when projecting from an unknown type.
## Example: single suggestion in namespace
This was the originally motivating example, as the string refactor led
to a number of anonymous-lambda-expressions with `Char` functions that
were no longer recognized as such.
```lean4
example := (·.isWhitespace)
```
Before:
```
Invalid field notation: Type of
x✝
is not known; cannot resolve field `isWhitespace`
```
The message is unchanged, but this PR adds a hint:
```
Hint: Consider replacing the field projection `.isWhitespace` with a call to the function `Char.isWhitespace`.
```
## Example: single suggestion in namespace
```lean4
example := fun n => n.succ
```
Before:
```
Invalid field notation: Type of
n
is not known; cannot resolve field `succ`
```
The message is unchanged, but this PR adds a hint:
```
Hint: Consider replacing the field projection with a call to one of the following:
• `Fin.succ`
• `Nat.succ`
• `Std.PRange.succ`
```
This PR adds a heterogeneous version of the constructor injectivity
theorems. These theorems are useful for indexed families, and will be
used in `grind`.
This PR adds a module resolution procedure to Lake to disambiguate
modules that are defined in multiple packages.
On an `import`, Lake will now check if multiple packages within the
workspace define the module. If so, it will verify that modules have
sufficiently similar definitions (i.e., artifacts with the same content
hashes). If not, Lake will report an error.
This verification is currently only done for direct imports. Transitive
imports are not checked for consistency. An overhaul of transitive
imports will come later.
This PR fixes a bug in `grind?`. The suggestion using the `grind`
interactive mode was dropping the configuration options provided by the
user. In the following account, the third suggestion was dropping the
`-reducible` option.
```lean
/--
info: Try these:
[apply] grind -reducible only [Equiv.congr_fun, #5103]
[apply] grind -reducible only [Equiv.congr_fun]
[apply] grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
-/
example :
(Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
= (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
grind? -reducible [Equiv.congr_fun]
```
This PR adds the `grind` option `reducible` (default: `true`). When
enabled, definitional equality tests expand only declarations marked as
`@[reducible]`.
Use `grind -reducible` to allow expansion of non-reducible declarations
during definitional equality tests.
This option affects only definitional equality; the canonicalizer and
theorem pattern internalization always unfold reducible declarations
regardless of this setting.
This PR refines several error error messages, mostly involving invalid
use of field notation, generalized field notation, and numeric
projection. Provides a new error explanation for field notation.
## Error message changes
In general:
- Uses a slightly different convention for expression-type pairs, where
the expression is always given `indentExpr` and the type is given
`inlineExpr` treatment. This is something of a workaround for the fact
that the `Format` type is awkward for embedding possibly-linebreaking
expressions in not-linebreaking text, which may be a separate issue
worth addressing.
- Tries to give slightly more "why" reasoning — the environment does not
contain `String.parse`, and _therefore you can't project `.parse` from a
`String`_.
Some specific examples:
### No such projection function
```lean4
#check "".parse
```
before:
```
error: Invalid field `parse`: The environment does not contain `String.parse`
""
has type
String
```
after:
```
error: Invalid field `parse`: The environment does not contain `String.parse`, so it is not possible to project the field `parse` from an expression
""
of type `String`
```
### Type does not have the correct form
```lean4
example (x : α) := (foo x).foo
```
before:
```
error: Invalid field notation: Type is not of the form `C ...` where C is a constant
foo x
has type
α
```
after:
```
error: Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
foo x
has type `α` which does not have the necessary form.
```
## Refactoring
Includes some refactoring changes as well:
- factors out multiple uses of number (1, 2, 3, 212, 222) to ordinal
("first", "second", "third", "212th", "222nd") conversion into
Lean.Elab.ErrorUtils
- significant refactoring of `resolveLValAux` in `Lean.Elab.App` — in
place of five helper functions, a special-case function case analysis,
and a case analysis on the projection type and structure, there's now a
single case analysis on the projection type and structure. This allows
several error messages to be more explicit (there were a number of cases
where index projection was being described as field projection in an
error messages) and gave the opportunity to slightly improve positining
for several errors: field *notation* errors should appear on `foo.bar`,
but field *projection* errors should appear only on the `bar` part of
`foo.bar`.
This PR moves the processing of options passed to the CLI from
`shell.cpp` to `Shell.lean`.
As with previous ports, this attempts to mirror as much of the original
behavior as possible, Benefits to be gained from the ported code can
come in later PRs. There should be no significant behavioral changes
from this port. Nonetheless, error reporting has changed some, hopefully
for the better. For instance, errors for improper argument
configurations has been made more consistent (e.g., Lean will now error
if numeric arguments fall outside the expected range for an option).
(Redo of #11345 to fix Windows issue.)
This PR generalizes the `noConfusion` constructions to heterogeneous
equalities (assuming propositional equalities between the indices). This
lays ground work for better support for applying injection to
heterogeneous equalities in grind.
The `Meta.mkNoConfusion` app builder shields most of the code from these
changes.
Since the per-constructor noConfusion principles are now more
expressive, `Meta.mkNoConfusion` no longer uses the general one.
In `Init.Prelude` some proofs are more pedestrian because `injection`
now needs a bit more machinery.
This is a breaking change for whoever uses the `noConfusion` principle
manually and explicitly for a type with indices.
Fixes#11450.
This PR adds lemmas stating that if a get operation returns a value,
then the queried key must be contained in the collection. These lemmas
are added for HashMap and TreeMap-based collections, with a similar
lemma also added for `Init.getElem`.
This PR adapts the lambda lifter in LCNF to eta contract instead of
lambda lift if possible. This prevents the creation of a few hundred
unnecessary lambdas across the code base.
This PR moves the `Inhabited` instances in constant `DTreeMap` (and
related) queries, such as `Const.get!`, where the `Inhabited` instance
can be provided before proving a key.
This PR fixes a panic in `getEqnsFor?` when called on matchers generated
from match expressions in theorem types.
When a theorem's type contains a match expression (e.g., `theorem bar :
(match ... with ...) = 0`), the compiler generates a matcher like
`bar.match_1`. Calling `getEqnsFor?` on this matcher would panic with:
```
PANIC: duplicate normalized declaration name bar.match_1.eq_1 vs. _private...bar.match_1.eq_1
```
This also affected the `try?` tactic, which internally uses
`getEqnsFor?`.
We make `shouldGenerateEqnThms` return `false` for matchers, since their
equations are already generated separately by
`Lean.Meta.Match.MatchEqs`. This prevents the equation generation
machinery from attempting to create duplicate equation theorems.
Closes#11461Closes#10390🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR fixes various typos across the codebase in documentation and
comments.
- `infered` → `inferred` (ParserCompiler.lean)
- `declartation` → `declaration` (Cleanup.lean)
- `certian` → `certain` (CasesInfo.lean)
- `wil` → `will` (Cache.lean)
- `the the` → `the` (multiple files - PrefixTree.lean, Sum/Basic.lean,
List/Nat/Perm.lean, Time.lean, Bounded.lean, Lake files)
- `to to` → `to` (MutualInductive.lean, simp_bubblesort_256.lean)
- Grammar improvements in Bounded.lean and Time.lean
All changes are to comments and documentation only - no functional
changes.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds `+suggestions` support to `solve_by_elim`, following the
pattern established by `grind +suggestions` and `simp_all +suggestions`.
Gracefully handles invalid/nonexistent suggestions by filtering them out
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds `solve_by_elim` as a fallback in the `try?` tactic's simple
tactics. When `rfl` and `assumption` both fail but `solve_by_elim`
succeeds (e.g., for goals requiring hypothesis chaining or
backtracking), `try?` will now suggest `solve_by_elim`.
The structure is `first | (attempt_all | rfl | assumption) |
solve_by_elim`, so `solve_by_elim` only runs when the faster tactics
fail.
This is a prerequisite for removing the "first pass" `solve_by_elim`
from `apply?`. Currently `apply?` calls `solve_by_elim` twice: once
before library search, and once after each lemma application. The first
pass can be removed once `try?` includes `solve_by_elim`.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR removes the "first pass" behavior where `exact?` and `apply?`
would try `solve_by_elim` on the original goal before doing library
search. This simplifies the `librarySearch` API and focuses these
tactics on their primary purpose: finding library lemmas.
Users who want to find proofs using local hypotheses should use `try?`
instead, which now includes `solve_by_elim` in its pipeline (see
https://github.com/leanprover/lean4/pull/11462).
Changes:
- Removed first pass from `librarySearch`
- Simplified `tactic` parameter from `Bool → List MVarId → MetaM (List
MVarId)` to `List MVarId → MetaM (List MVarId)`
- Updated test expectations
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR improves the error message when no library suggestions engine is
registered to recommend importing `Lean.LibrarySuggestions.Default` for
the built-in engine.
**Before:**
```
No library suggestions engine registered. (Note that Lean does not provide a default library suggestions engine, these must be provided by a downstream library, and configured using `set_library_suggestions`.)
```
**After:**
```
No library suggestions engine registered. (Add `import Lean.LibrarySuggestions.Default` to use Lean's built-in engine, or use `set_library_suggestions` to configure a custom one.)
```
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds recording functionality such that `shake` can more
precisely track whether an import should be preserved solely for its
`attribute` commands.
This PR adds the difference operation on `DTreeMap`/`TreeMap`/`TreeSet`
and proves several lemmas about it.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
The bench script expected no output on stdout from `compile.sh`, which
was not always the case. Now, it separates the compilation and size
measurement steps.
This PR slightly improves the types involved in creating boxed
declarations. Previously the type of
the vdecl used for the return was always `tobj` when returning a boxed
scalar. This is not the most
precise annotation we can give.
This PR modifies the error message for type synthesis failure for the
case where the type class in question is potentially derivable using a
`deriving` command. Also changes the error explanation for type class
instance synthesis failure with an illustration of this pattern.
## Example
```lean4
inductive MyColor where
| chartreuse | sienna | thistle
def forceColor (oc : Option MyColor) :=
oc.get!
```
Before this PR, this gives the potentially confusing impression that
Lean may have decided that `MyColor` is _not_ inhabited — people used to
Rust may be especially inclined towards this confusion.
```
failed to synthesize instance of type class
Inhabited MyColor
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
```
After this PR, a targeted hint suggests precisely the command that will
fix the issue:
```
error: failed to synthesize instance of type class
Inhabited MyColor
Hint: Adding the command `deriving instance Inhabited for MyColor` may allow Lean to derive the missing instance.
```
This PR lets recursive functions defined by well-founded recursion use a
different `fix` function when the termination measure is of type `Nat`.
This fix-point operator use structural recursion on “fuel”, initialized
by the given measure, and is thus reasonable to reduce, e.g. in `by
decide` proofs.
Extra provisions are in place that the fixpoint operator only starts
reducing when the fuel is fully known, to prevent “accidential” defeqs
when the remaining fuel for the recursive calls match the initial fuel
for that recursive argument.
To opt-out, the idiom `termination_by (n,0)` can be used.
We still use `@[irreducible]` as the default for such recursive
definitions, to avoid unexpected `defeq` lemmas. Making these functions
`@[semireducible]` by default showed performance regressions in lean.
When the measure is of type `Nat`, the system will accept an explicit
`@[semireducible]` without the usual warning.
Fixes#5234. Fixes: #11181.
This PR performs minor maintenance on the String API
- Rename `String.Pos.toCopy` to `String.Pos.copy` to adhere to the
naming convention
- Rename `String.Pos.extract` to `String.extract` to get sane dot
notation again
- Add `String.Slice.Pos.extract`
This PR reduces the memory consumption of the language server (the
watchdog process in particular). In Mathlib, it reduces memory
consumption by about 1GB.
It also fixes two bugs in the call hierarchy:
- When an open file had import errors (e.g. from a transitive build
failure), the call hierarchy would not display any usages in that file.
Now we use the reference information from the .ilean instead.
- When a command would not set a parent declaration (e.g. `#check`), the
result was filtered from the call hierarchy. Now we display it as
`[anonymous]` instead.
This PR documents the `grind_pattern` command for manually selecting
theorem instantiation patterns, including multi-patterns and the
constraint system (`=/=`, `=?=`, `size`, `depth`, `is_ground`,
`is_value`, `is_strict_value`, `gen`, `max_insts`, `guard`, `check`).
This PR implements support for **guards** in `grind_pattern`. The new
feature provides additional control over theorem instantiation. For
example, consider the following monotonicity theorem:
```lean
opaque f : Nat → Nat
theorem fMono : x ≤ y → f x ≤ f y := ...
```
We can use `grind_pattern` to instruct `grind` to instantiate the
theorem for every pair `f x` and `f y` occurring in the goal:
```lean
grind_pattern fMono => f x, f y
```
Then we can automatically prove the following simple example using
`grind`:
```lean
/--
trace: [grind.ematch.instance] fMono: f a ≤ b → f (f a) ≤ f b
[grind.ematch.instance] fMono: f a ≤ c → f (f a) ≤ f c
[grind.ematch.instance] fMono: f a ≤ a → f (f a) ≤ f a
[grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a))
[grind.ematch.instance] fMono: f a ≤ f a → f (f a) ≤ f (f a)
[grind.ematch.instance] fMono: f (f a) ≤ b → f (f (f a)) ≤ f b
[grind.ematch.instance] fMono: f (f a) ≤ c → f (f (f a)) ≤ f c
[grind.ematch.instance] fMono: f (f a) ≤ a → f (f (f a)) ≤ f a
[grind.ematch.instance] fMono: f (f a) ≤ f (f a) → f (f (f a)) ≤ f (f (f a))
[grind.ematch.instance] fMono: f (f a) ≤ f a → f (f (f a)) ≤ f (f a)
[grind.ematch.instance] fMono: a ≤ b → f a ≤ f b
[grind.ematch.instance] fMono: a ≤ c → f a ≤ f c
[grind.ematch.instance] fMono: a ≤ a → f a ≤ f a
[grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a))
[grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a)
[grind.ematch.instance] fMono: c ≤ b → f c ≤ f b
[grind.ematch.instance] fMono: c ≤ c → f c ≤ f c
[grind.ematch.instance] fMono: c ≤ a → f c ≤ f a
[grind.ematch.instance] fMono: c ≤ f (f a) → f c ≤ f (f (f a))
[grind.ematch.instance] fMono: c ≤ f a → f c ≤ f (f a)
[grind.ematch.instance] fMono: b ≤ b → f b ≤ f b
[grind.ematch.instance] fMono: b ≤ c → f b ≤ f c
[grind.ematch.instance] fMono: b ≤ a → f b ≤ f a
[grind.ematch.instance] fMono: b ≤ f (f a) → f b ≤ f (f (f a))
[grind.ematch.instance] fMono: b ≤ f a → f b ≤ f (f a)
-/
#guard_msgs in
example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
set_option trace.grind.ematch.instance true in
grind
```
However, many unnecessary theorem instantiations are generated.
With the new `guard` feature, we can instruct `grind` to instantiate the
theorem **only if** `x ≤ y` is already known to be true in the current
`grind` state:
```lean
grind_pattern fMono => f x, f y where
guard x ≤ y
x =/= y
```
If we run the example again, only three instances are generated:
```lean
/--
trace: [grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a)
[grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a))
[grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a))
-/
#guard_msgs in
example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
set_option trace.grind.ematch.instance true in
grind
```
Note that `guard` does **not** check whether the expression is
*implied*. It only checks whether the expression is *already known* to
be true in the current `grind` state. If this fact is eventually
learned, the theorem will be instantiated.
If you want `grind` to check whether the expression is implied, you
should use:
```lean
grind_pattern fMono => f x, f y where
check x ≤ y
x =/= y
```
Remark: we can use multiple `guard`/`check`s in a `grind_pattern`
command.
This PR adds per-module `.ilean` and `.olean` file size metrics, global
and per-module cycle counting, and adds back `lean --stat`-based
metrics. It also renames some `size/*` metrics to get rid of the name
`stdlib`.
This PR clarifies the bootstrap documentation to explain that to trigger
the automatic stage0 update mechanism, you should modify
`stage0/src/stdlib_flags.h` (not `src/stdlib_flags.h`). The existing
text was ambiguous about which file to modify.
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR reverts https://github.com/leanprover/lean4/pull/11396, which
changed `set_library_suggestions` to create an auxiliary definition
marked with `@[library_suggestions]`, rather than storing `Syntax`
directly in the environment extension.
It wasn't tested properly.
Co-authored-by: Claude <noreply@anthropic.com>
This PR fixes a kernel type mismatch error in grind's denominator
cleanup feature. When generating proofs involving inverse numerals (like
`2⁻¹`), the proof context is compacted to only include variables
actually used. This involves renaming variable indices - e.g., if
original indices were `{0: r, 1: 2⁻¹}` and only `2⁻¹` is used, it gets
renamed to index 0.
The bug was that polynomials were correctly renamed via `varRename`, but
the variable index `x` stored in `cancelDen` constraints was passed
directly to the proof without renaming, causing a mismatch between the
polynomial's variable references and the theorem's variable argument.
Added `ringVarDecls` to track ring variable indices that need renaming,
similar to how `ringPolyDecls` tracks polynomials. The `mkRingContext`
function now also renames these variable indices.
See zulip discussion at [#nightly-testing > Mathlib status updates @
💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20status.20updates/near/560575295).
🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR changes `set_library_suggestions` to create an auxiliary
definition marked with `@[library_suggestions]`, rather than storing
`Syntax` directly in the environment extension. This enables better
persistence and consistency of library suggestions across modules.
The change requires a stage0 update before tests can be restored. After
CI updates stage0, a follow-up PR will restore the test cases.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
This PR fixes an issue where `grind` would fail after multiple
`norm_cast`
calls with the error "unexpected metadata found during internalization".
The `norm_cast` tactic adds mdata nodes to expressions, and when called
multiple times it creates nested mdata. The `eraseIrrelevantMData`
preprocessing function was using `.continue e` when stripping mdata,
which causes `Core.transform` to reconstruct the mdata node around the
visited children. By changing to `.visit e`, the inner expression is
passed back to `pre` for another round of processing, allowing all
nested mdata layers to be stripped.
Closes#11411🤖 Prepared with Claude Code
Co-authored-by: Claude <noreply@anthropic.com>
This PR sorts the declarations fed into ElimDeadBranches in increasing
size. This can improve performance when we are dealing with a lot of
iterations.
The motivation for this change is as follows. Currently the algorithm
for doing one step of abstract interpretation is:
```
for decl in scc do
interpDecl
if summaryChanged decl then
return true
return false
```
whenever we return true we run another step. Now suppose we are in a
situation where we have an SCC with one big decl in the front and then
`n` small ones afterwards. For each time that the small ones change
their summary, we will re-run analysis of the big one in the front.
Currently the ordering is basically at "random" based on how other
compilers inject things into the SCC. This change ensures the behavior
is consistent and at least somewhat intelligent. By putting the small
declarations first, whenever we trigger a rerun of the loop we bias
analyzing the small declarations first, thus decreasing run time.
Note that this change does not have much effect on the current pipeline
because: We usually construct the SCCs in a way such that small ones
happen to be in front anyways. However, with upcomping changes on
specialization this is about to change.
This PR implements the following `grind_pattern` constraints:
```lean
grind_pattern fax => f x where
depth x < 2
grind_pattern fax => f x where
is_ground x
grind_pattern fax => f x where
size x < 5
grind_pattern fax => f x where
gen < 2
grind_pattern fax => f x where
max_insts < 4
grind_pattern gax => g as where
as =?= _ :: _
```
This PR adds support for difference operation for
`DHashMap`/`HashMap`/`HashSet` and proves several lemmas about it.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR implements new kinds of constraints for the `grind_pattern`
command. These constraints allow users to control theorem instantiation
in `grind`.
It requires a manual `update-stage0` because the change affects the
`.olean` format, and the PR fails without it.
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 fixes the compilation of structure projections with unboxed
arguments marked `extern`, adding missing `dec` instructions. It led to
leaking single allocations when such functions were used as closures or
in the interpreter.
This is the minimal working fix; `extern` should not replicate parts of
the compilation pipeline, which will be possible via #10291.
This PR is a followup of #11381 and enforces the invariants on ordering
of closed terms and constants required by the EmitC pass properly by
toposorting before saving the declarations into the Environment.
This PR adds `ofArray` to `DHashMap`/`HashMap`/`HashSet` and proves a
simp lemma allowing to rewrite `ofArray` to `ofList`.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR adds a release note draft for the next major release, where the
module system will cease being experimental.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR adds missing docstrings for constants that occur in the
reference manual.
---------
Co-authored-by: Johannes Tantow <44068763+jt0202@users.noreply.github.com>
This PR fixes a bug where the closed term extraction does not respect
the implicit invariant of the
c emitter to have closed term decls first, other decls second, within an
SCC. This bug has not yet
been triggered in the wild but was unearthed during work on upcoming
modifications of the
specializer.
This PR renames `String.Slice.Pos.ofSlice` to `String.Pos.ofToSlice` to
adhere with the (yet-to-be documented) naming convention for mapping
positions to positions. It then adds several new functions so that for
every way to construct a slice from a string and slice, there are now
functions for mapping positions forwards and backwards along this
construction.
This PR sets `@[macro_inline]` on the (trivial) `.ctorIdx` for inductive
types with one constructor, to reduce the number of symbols generated by
the compiler.
This PR aims to improve the performance of `String.contains`,
`String.find`, etc. when using patterns of type `Char` or `Char -> Bool`
by moving the needle out of the iterator state and thus working around
missing unboxing in the compiler.
This PR makes the library suggestions extension state available when
importing from `module` files.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds support for cleaning up denominators in `grind linarith`
when the type is a `Field`.
Examples:
```lean
open Std Lean.Grind
section
variable {α : Type} [Field α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α]
example (a b : α) (h : a < b / 2) : 2 * a < b := by grind
example (a b : α) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind
example (a b : α) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind
example (a b : α) (h : a = b * (3⁻¹)^2) : 9 * a ≤ b := by grind
example (a b : α) (h : a / 2 ≠ b / 9) : 9 * a < 2 * b ∨ 9 * a > 2 * b := by grind
example (a b : α) (h : a < b / (2^2 - 3/2 + -1 + 1/2)) : 2 * a < b := by grind
end
example (a b : Rat) (h : a < b / 2) : a + a < b := by grind
example (a b : Rat) (h : a < b / 2) : a + a ≤ b := by grind
example (a b : Rat) (h : a ≠ b * (3⁻¹)^2) : 9 * a < b ∨ 9 * a > b := by grind
example (a b : Rat) (h : a / 2 ≠ b / 9) : 9 * a < 2 * b ∨ 9 * a > 2 * b := by grind
```
This PR makes the `Std.Time.Format` import in
`Lean.Elab.Tactic.Grind.Annotated` private rather than public,
preventing the entire `Std.Time` infrastructure (including timezone
databases) from being re-exported through `import Lean`.
The `grindAnnotatedExt` extension is kept private, with a new public
accessor function `isGrindAnnotatedModule` exposed for use by
`LibrarySuggestions.Basic`.
This should address the +2.5% instruction increase on `import Lean`
observed after merging #11332.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR enables parallelism in `try?`. Currently, we replace the
`attempt_all` stages (there are two, one for builtin tactics including
`grind` and `simp_all`, and a second one for all user extensions) with
parallel versions. We do not (yet?) change the behaviour of `first`
based stages.
This PR moves the processing of options passed to the CLI from
`shell.cpp` to `Shell.lean`.
As with previous ports, this attempts to mirror as much of the original
behavior as possible, Benefits to be gained from the ported code can
come in later PRs. There should be no significant behavioral changes
from this port. Nonetheless, error reporting has changed some, hopefully
for the better. For instance, errors for improper argument
configurations has been made more consistent (e.g., Lean will now error
if numeric arguments fall outside the expected range for an option).
This PR accelerates termination of the ElimDeadBranches compiler pass.
The implementation addresses situations such as `choice [none, some
top]` which can be summarized to
`top` because `Option` has only two constructors and all constructor
arguments are `top`.
This PR implements a helper simproc for `grind`. It is part of the
infrastructure used to cleanup denominators in `grind linarith`.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR adds a focused error explanation aimed at the case where someone
tries to use Natural-Numbers-Game-style `induction` proofs directly in
Lean, where such proofs are not syntactically valid.
## Discussion
The natural numbers game uses a syntax that overlaps with Lean's
`induction` syntax despite having more structural similarity to
`induction'`. This means that fully correct proofs in the natural
numbers game, like this...
```lean4
import Mathlib
theorem zero_mul (m : ℕ) : 0 * m = 0 := by
induction m with n n_ih
rw [mul_zero]
rfl
rw [mul_succ]
rw [add_zero]
rw [n_ih]
rfl
```
...have completely baffling error messages from a newcomers'
perspective:
```
notNaturalNumbersGame.lean:3:20: error: unknown tactic
notNaturalNumbersGame.lean:3:2: error: Alternative `zero` has not been provided
notNaturalNumbersGame.lean:3:2: error: Alternative `succ` has not been provided
```
(the Mathlib import here only provides the `ℕ` syntax here; equivalently
`ℕ` could be renamed to `Nat` and the import could be removed, [like
this](https://live.lean-lang.org/#codez=C4Cwpg9gTmC2AEAvMUIH1YFcA28AUCAXPAHICGwAlPMQAzwBU8CAvPPYWwEYCeAUPHgBLAHYATTAGNgQiCObwA7kNDx5ItEJAD4URfADaWbGmSoAujqgAzbFf1GcaAM5TJlwXsNkxY0yggPXQcNLSCbbCA))
There are many problems with this proof from the perspective of "stock"
Lean, but the error messages in the `induction` case are particularly
unfriendly and provide no guidance from a NNG learner's perspective.
This PR provides more information about what is wrong:
```
notNaturalNumbersGame.lean:3:20: error: unknown tactic
notNaturalNumbersGame.lean:3:14: error(lean.inductionWithNoAlts): Invalid syntax for induction tactic: The `with` keyword must followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.
```
The error explanation it links to explicitly flags the transition of
NNG-style proofs to Lean as the likely culprit, and gives an example of
an effective translation.
This PR updates the `foldr`, `all`, `any` and `contains` functions on
`String` to be defined in terms of their `String.Slice` counterparts.
This is the last one in a long series of PRs. After this, all `String`
operations are polymorphic in the pattern, and no `String` operation
falls back to `String.Pos.Raw` internally (except those in the
`String.Pos.Raw` and `String.Substring.Raw` namespaces of course, which
still play a role in metaprogramming and will stay for the foreseeable
future).
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 changes the interface of the `ForIn`, `ForIn'`, and `ForM`
typeclasses to not take a `Monad m` parameter. This is a breaking change
for most downstream `instance`s, which will will now need to assume
`[Monad m]`.
The rationale is that if the provider of an instance requires `m` to be
a Monad, they should assume this up front. This makes it possible for
the instanve to assume `LawfulMonad m` or some other stronger
requirement, and also to provided a concrete instance for a particular
`m` without assuming a non-canonical `Monad` structure on it.
Zulip: [#lean4 > Monad assumptions in fields of other typeclasses @
💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Monad.20assumptions.20in.20fields.20of.20other.20typeclasses/near/537102158)
This PR activates the `grind_annotated` command in
`Init.Data.List.Lemmas` by removing the TODO comment and uncommenting
the command.
This PR depends on #11346 (implement `grind_annotated` command) and
should be merged after that PR (and after CI has done an
`update-stage0`.
This PR enables the syntax `use [ns Foo]` and `instantiate only [ns
Foo]` inside a `grind` tactic block, and has the effect of activating
all grind patterns scoped to that namespace. We can use this to
implement specialized tactics using `grind`, but only controlled subsets
of theorems.
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR upstreams the `with_weak_namespace` command from Mathlib:
`with_weak_namespace <id> <cmd>` changes the current namespace to `<id>`
for the duration of executing command `<cmd>`, without causing scoped
things to go out of scope. This is in preparation for upstreaming the
`scoped[Foo.Bar]` syntax from Mathlib, which will be useful now that we
are adding `grind` annotations in scopes.
This PR adds a `grind_annotated "YYYY-MM-DD"` command that marks files
as manually annotated for grind.
When LibrarySuggestions is called with `caller := "grind"` (as happens
with `grind +suggestions`), theorems from grind-annotated files are
filtered out from premise selection. The date argument validates using
Std.Time and is informational only for now, but could be used later to
detect files that need re-review.
There's no need for the library suggestions tools to suggest `grind`
theorems from files that have already been carefully annotated by hand.
This PR adds infrastructure for parallel execution across Lean's tactic
monads.
- Add IO.waitAny' to Init/System/IO.lean for waiting on task completion
- Add `Lean.Elab.Task` with `asTask` utilities for `CoreM`, `MetaM`,
`TermElabM`, `TacticM`
- Add `Lean.Elab.Parallel` with parallel execution strategies:
* `par`/`par'` - collect results in original order
* `parIter`/`parIterGreedy` - iterate over results (original or
completion order) (also variants with a cancellation token)
* `parFirst` - return first successful result
This does *not* attempt to be a monad-polymorphic framework for
parallelism. It's intentionally hard-coded to the Lean tactic monads
which I need to work with. If there's desire to make this polymorphic,
hopefully that can be done separately.
This PR renames `String.bytes` to `String.toByteArray`.
This is for two reasons: first, `toByteArray` is a better name, and
second, we have something else that wants to use the name `bytes`,
namely the function that returns in iterator over the string's bytes.
This PR documents that `backward.*` options are only temporary
migration aids and may disappear without further notice after 6 months
after their introduction. Users are kindly asked to report if they rely
on these options.
This PR adds a coercion from `String` to `String.Slice`.
In our envisioned future, most functions operating on strings will
accept `String.Slice` parameters by default (like `str` in Rust), and
this enables calling such functions with arguments of type `String`.
Closes#11298.
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 removes the `group` field from option descriptions. It is
unused, does not have a clear meaning and often matches the first
component of the option name.
Given its run time of >2hrs, the job is added as a secondary job for
nightly releases and a primary job for full releases. A new check level
for differentiating between nightlies and full releases is added for
this.
(Trying to) reactivate lsan will happen in a follow-up PR.
This PR fixes freeing memory accidentally retained for each document
version in the language server on certain elaboration workloads. The
issue must have existed since 4.18.0.
This PR adds an explicit normalization layer for ring constraints in the
`grind linarith` module. For example, it will be used to clean up
denominators when the ring is a field.
This PR renames the `cutsat` tactic to `lia` for better alignment with
standard terminology in the theorem proving community.
`cutsat` still works but now emits a deprecation warning and suggests
using `lia` instead via "Try this:". Both tactics have identical
behavior.
Co-authored-by: Claude <noreply@anthropic.com>
This PR cleans up the API around `String.find` and moves it uniformly to
the new position types `String.ValidPos` and `String.Slice.Pos`
Overview:
- To search for a character, character predicate, string or slice in a
string or slice `s`, use `s.find?` or `s.find`.
- To do the same, but starting at a position `p` of a string or slice,
use `p.find?` or `p.find`.
- To do the same but between two positions `p` and `q`, construct the
slice from `p` to `q` and then use `find?` or `find` on that.
- To search backwards, all of the above applies, except that the
function is called `revFind?`, there is no non-question-mark version
(use `getD` if there is a sane default return value in your specific
application), and that you can only search for characters and character
predicates, not strings or slices.
This PR ensures that users can provide `grind` proof parameters whose
types are not `forall`-quantified. Examples:
```lean
opaque f : Nat → Nat
axiom le_f (a : Nat) : a ≤ f a
example (a : Nat) : a ≤ f a := by
grind [le_f a]
example (a b : α) (h : ∀ x y : α, x = y) : a = b := by
grind [h a b]
```
This PR redefines `front` and `back` on `String` to go through
`String.Slice` and adds the new `String` functions `front?`, `back?`,
`positions`, `chars`, `revPositions`, `revChars`, `byteIterator`,
`revBytes`, `lines`.
This PR adds `CoreM.toIO'`, the analogue of `CoreM.toIO` dropping the
state from the return type, and similarly for `TermElabM.toIO'` and
`MetaM.toIO'`.
This PR introduces a new `grind` option, `funCC` (enabled by default),
which extends congruence closure to *function-valued* equalities. When
`funCC` is enabled, `grind` tracks equalities of **partially applied
functions**, allowing reasoning steps such as:
```lean
a : Nat → Nat
f : (Nat → Nat) → (Nat → Nat)
h : f a = a
⊢ (f a) m = a m
g : Nat → Nat
f : Nat → Nat → Nat
h : f a = g
⊢ f a b = g b
```
Given an application `f a₁ a₂ … aₙ`, when `funCC := true` and function
equality is enabled for `f`, `grind` generates and tracks equalities for
all partial applications:
* `f a₁`
* `f a₁ a₂`
* …
* `f a₁ a₂ … aₙ`
This allows equalities such as `f a₁ = g` to propagate through further
applications.
**When is function equality enabled for a symbol?**
Function equality is enabled for `f` in the following cases:
1. `f` is **not a constant** (e.g., a lambda, a local function, or a
function parameter).
2. `f` is a **structure field projection**, provided the structure is
**not a `class`**.
3. `f` is a constant marked with `@[grind funCC]`
Users can also enable function equality for specific constants in a
single call using:
```lean
grind [funCC f, funCC g]
```
**Examples:**
```lean
example (m : Nat) (a : Nat → Nat) (f : (Nat → Nat) → (Nat → Nat)) (h : f a = a) :
f a m = a m := by
grind
example (m : Nat) (a : Nat → Nat) (f : (Nat → Nat) → (Nat → Nat)) (h : f a = a) :
f a m = a m := by
fail_if_success grind -funCC -- fails if `funCC` is disabled
grind
```
```lean
example (a b : Nat) (g : Nat → Nat) (f : Nat → Nat → Nat) (h : f a = g) :
f a b = g b := by
grind
example (a b : Nat) (g : Nat → Nat) (f : Nat → Nat → Nat) (h : f a = g) :
f a b = g b := by
fail_if_success grind -funCC
grind
```
**Enabling per-symbol with parameters or attributes**
```lean
opaque f : Nat → Nat → Nat
opaque g : Nat → Nat
example (a b c : Nat) : f a = g → b = c → f a b = g c := by
grind [funCC f, funCC g]
attribute [grind funCC] f g
example (a b c : Nat) : f a = g → b = c → f a b = g c := by
grind
```
This feature substantially improves `grind`’s support for higher-order
and partially-applied function equalities, while preserving
compatibility with first-order SMT behavior when `funCC` is disabled.
Closes#11309
This PR significantly changes the signature of the `ToIterator` type
class. The obtained iterators' state is no longer dependently typed and
is an `outParam` instead of being bundled inside the class. Among other
benefits, `simp` can now rewrite inside of `Slice.toList` and
`Slice.toArray`. The downside is that we lose flexibility. For example,
the former combinator-based implementation of `Subarray`'s iterators is
no longer feasible because the states are dependently typed. Therefore,
this PR provides a hand-written iterator for `Subarray`, which does not
require a dependently typed state and is faster than the previous one.
Converting a family of dependently typed iterators into a simply typed
one using a `Sigma`-state iterator generates forbiddingly bad code, so
that we do provide such a combinator. This PR adds a benchmark for this
problem.
This PR improves the support for `Fin n` in `grind` when `n` is not a
numeral.
- `toInt (0 : Fin n) = 0` in `grind lia`.
- `Fin.mk`-applications are treated as interpreted terms in `grind lia`.
- `Fin.val` applications are suppressed from `grind lia`
counterexamples.
This PR fixes a breakage in Lake's TOML test caused by String API
changes. It also removes a JSON parser workaround that has since been
fixed, and it more generally polishes up the code.
This PR fixes an issue affecting `grind -revert`. In this mode, assigned
metavariables in hypotheses were not being instantiated. This issue was
affecting two files in Mathlib.
This PR fixes a local declaration internalization in `grind` that was
exposed when using `grind -revert`. This bug was affecting a `grind`
proof in Mathlib.
This PR makes the specializer (correctly) share more cache keys across
invocations, causing us to produce less code bloat.
We observed that in functions with lots of specialization, sometimes
cache keys are defeq but not BEq because one has unused let decls
(introduced by specialization) that the other doesn't. This PR resolves
this conflict by erasing unused let decls from specializer cache keys.
This PR improves the error message encountered in the case of a type
class instance resolution failure, and adds an error explanation that
discusses the common new-user case of binary operation overloading and
points to the `trace.Meta.synthInstance` option for advanced debugging.
## Example
```lean4
def f (x : String) := x + x
```
Before:
```
failed to synthesize
HAdd String String ?m.5
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
```
After:
```
failed to synthesize instance of type class
HAdd String String ?m.5
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
Error code: lean.failedToSynthesizeTypeclassInstance
[View explanation](https://lean-lang.org/doc/reference/latest/find/?domain=Manual.errorExplanation&name=lean.failedToSynthesizeTypeclassInstance)
```
The error message is changed in three important ways:
* Explains *what* failed to synthesize, using the "type class"
terminology that's more likely to be recognized than the "instance"
terminology
* Points to the `trace.Meta.synthInstance` option which is otherwise
nearly undiscoverable but is quite powerful (see also
leanprover/reference-manual#663 which is adding commentary on this
option)
* Gives an error explanation link (which won't actually work until the
next release after this is merged) which prioritizes the common-case
explanation of using the wrong binary operation
This PR removes all code that sets the `Option.Decl.group` field, which
is unused and has no clearly documented meaning.
The actual removal of the field would be #11305.
This PR renames the CTests tests to use filenames as test names. So
instead of
```
2080 - leanruntest_issue5767.lean (Failed)
```
we get
```
2080 - tests/lean/run/issue5767.lean (Failed)
```
which allows Ctrl-Click’ing on them in the VSCode terminal.
This PR renames congruence lemmas for union on
`DHashMap`/`HashMap`/`HashSet`/`DTreeMap`/`TreeMap`/`TreeSet` to fit the
convention of being in the `Equiv` namespace.
This PR fixes a bug in the propagation rules for `ite` and `dite` used
in `grind`. The bug prevented equalities from being propagated to the
satellite solvers. Here is an example affected by this issue.
```lean
example
[LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
[Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α]
(a b c : α) :
(if a - b ≤ -(a - b) then -(a - b) else a - b) ≤
((if a - c ≤ -(a - c) then -(a - c) else a - c) + if c - d ≤ -(c - d) then -(c - d) else c - d) +
if b - d ≤ -(b - d) then -(b - d) else b - d := by
grind
```
This PR adds support for decidable equality of empty lists and empty
arrays. Decidable equality for lists and arrays is suitably modified so
that all diamonds are definitionally equal.
Following #9302, the strong condition of definitionally equal under
`with_reducible_and_instances` is tested. This also moves some of the
comments added in #9302 out of docstrings.
---------
Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This PR renames `String.replaceStartEnd` to `String.slice`,
`String.replaceStart` to `String.sliceFrom`, and `String.replaceEnd` to
`String.sliceTo`, and similar for the corresponding functions on
`String.Slice`.
This PR adds several lemmas that relate
`getMin`/`getMin?`/`getMin!`/`getMinD` and insertion to the empty
(D)TreeMap/TreeSet and their extensional variants.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Global `attribute` commands on non-local declarations are impossible to
track granularly a priori and so should be preserved by `shake` by
default. A new `shake` option could be added to ignore these
dependencies for evaluation.
This PR adds `Std.Slice.Pattern` instances for `p : Char -> Prop` as
long as `DecidablePred p`, to allow things like `"hello".dropWhile (· =
'h')`.
To achieve this, we refactor `ForwardPattern` and friends to be
"non-uniform", i.e., the class is now `ForwardPattern pat`, not
`ForwardPattern ρ` (where `pat : ρ`).
This PR provides intersection operation for
`ExtDHashMap`/`ExtHashMap`/`ExtHashSet` and proves several lemmas about
it.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR provides intersection on `DTreeMap`/`TreeMap`/`TreeSet`and
provides several lemmas about it.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR adds a function `String.Slice.length`, with the following
deprecation string: There is no constant-time length function on slices.
Use `s.positions.count` instead, or `isEmpty` if you only need to know
whether the slice is empty.
This PR adds the alias `String.Slice.any` for `String.Slice.contains`.
It would probably be even better to only have one, but we don't have a
good mechanism for pointing people looking for one towards the other, so
an alias it is for now.
This PR splits the single grind_lint.lean test (50+ seconds) into 7
separate files that each run in under 7 seconds:
- grind_lint_list.lean (5.7s): List namespace with exceptions
- grind_lint_array.lean (4.6s): Array namespace
- grind_lint_bitvec.lean (3.9s): BitVec namespace with exceptions
- grind_lint_std_hashmap.lean (6.8s): Std hash map/set namespaces
- grind_lint_std_treemap.lean (~6s): Std tree map/set namespaces
- grind_lint_std_misc.lean (~5s): Std.Do, Std.Range, Std.Tactic
- grind_lint_misc.lean (5.5s): All other non-Lean namespaces
Each file maintains complete namespace coverage and preserves all
existing exceptions. The split enables better CI parallelization and
faster feedback.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude <noreply@anthropic.com>
This PR implements support for arbitrary `grind` parameters. The feature
is similar to the one available in `simp`, where a proof term is treated
as a local universe-polymorphic lemma. This feature relies on `grind
-revert` (see #11248). For example, users can now write:
```lean
def snd (p : α × β) : β := p.2
theorem snd_eq (a : α) (b : β) : snd (a, b) = b := rfl
/--
trace: [grind.ematch.instance] snd_eq (a + 1): snd (a + 1, Type) = Type
[grind.ematch.instance] snd_eq (a + 1): snd (a + 1, true) = true
-/
#guard_msgs (trace) in
set_option trace.grind.ematch.instance true in
example (a : Nat) : (snd (a + 1, true), snd (a + 1, Type), snd (2, 2)) = (true, Type, snd (2, 2)) := by
grind [snd_eq (a + 1)]
```
Note that in the example above, `snd_eq` is instantiated only twice, but
with different universe parameters.
As described in #11248, the new feature cannot be used with `grind
+revert`.
This PR marks the automatically generated `sizeOf` theorems as `grind`
theorems.
closes#11259
Note: Requested update stage0, we need it to be able to solve example in
the issue above.
```lean
example (a: Nat) (b: Nat): sizeOf a < sizeOf (a, b) := by
grind
```
This PR fixes several memory leaks in the new `String` API.
These leaks are mostly situations where we forgot to put borrowing
annotations. The single
exception is the new `String` constructor `ofByteArray`. It cannot take
the `ByteArray` as
a borrowed argument anymore and must thus free it on its own.
This PR continues the homogenization between matchers and splitters,
following up on #11256. In particular it removes the ambiguity whether
`numParams` includes the `discrEqns` or not.
This PR replaces `MatcherInfo.numAltParams` with a more detailed data
structure that allows us, in particular, to distinguish between an
alternative for a constructor with a `Unit` field and the alternative
for a nullary constructor, where an artificial `Unit` argument is
introduced.
This PR introduces a function `String.split` which is based on
`String.Slice.split` and therefore supports all pattern types and
returns a `Std.Iter String.Slice`.
This supersedes the functions `String.splitOn` and `String.splitToList`,
and we remove all all uses of these functions from core. They will be
deprecated in a future PR.
Migrating from `String.splitOn` and `String.splitToList` is easy: we
introduce functions `Iter.toStringList` and `Iter.toStringArray` that
can be used to conveniently go from `Std.Iter String.Slice` to `List
String` and `Array String`, so for example `s.splitOn "foo"` can be
replaced by `s.split "foo" |>.toStringList`.
This PR adds a `Unit` assumption to alternatives of the splitter that
would otherwise not have arguments. This fixes#11211.
In practice these argument-less alternatives did not cause wrong
behavior, as the motive when used with `split` is always a function
type. But it is better to be safe here (maybe someone uses splitters in
other ways), it may increase the effectiveness of #10184 and simplifies
#11220.
The perf impact is insignificant in the grand scheme of things on
stdlib, but the change is effective:
```
~/lean4 $ build/release/stage1/bin/lean tests/lean/run/matchSplitStats.lean
969 splitters found
455 splitters are const defs
~/lean4 $ build/release/stage2/bin/lean tests/lean/run/matchSplitStats.lean
969 splitters found
829 splitters are const defs
```
This PR implements the option `revert`, which is set to `false` by
default. To recover the old `grind` behavior, you should use `grind
+revert`. Previously, `grind` used the `RevSimpIntro` idiom, i.e., it
would revert all hypotheses and then re-introduce them while simplifying
and applying eager `cases`. This idiom created several problems:
* Users reported that `grind` would include unnecessary parameters. See
[here](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Grind.20aggressively.20includes.20local.20hypotheses.2E/near/554887715).
* Unnecessary section variables were also being introduced. See the new
test contributed by Sebastian Graf.
* Finally, it prevented us from supporting arbitrary parameters as we do
in `simp`. In `simp`, I implemented a mechanism that simulates local
universe-polymorphic theorems, but this approach could not be used in
`grind` because there is no mechanism for reverting (and re-introducing)
local universe-polymorphic theorems. Adding such a mechanism would
require substantial work: I would need to modify the local context
object. I considered maintaining a substitution from the original
variables to the new ones, but this is also tricky, because the mapping
would have to be stored in the `grind` goal objects, and it is not just
a simple mapping. After reverting everything, I would need to keep a
sequence of original variables that must be added to the mapping as we
re-introduce them, but eager case splits complicate this quite a bit.
The whole approach felt overly messy.
The new behavior `grind -revert` addresses all these issues. None of the
`grind` proofs in our test suite broke after we fixed the bugs exposed
by the new feature. That said, the traces and counterexamples produced
by `grind` are different. The new proof terms are also different.
This PR introduces a clarifying note to "undefined identifier" error
messages when the undefined identifier is in a syntactic position where
autobinding might generally apply, but where and autobinding is
disabled. A corresponding note is made in the `lean.unknownIdentifier`
error explanation.
The core intended audience for this error message change is "newcomer
who would otherwise be baffled why the thing that works in this Mathlib
project gets 'unknown identifier' errors in this non-Mathlib project."
## Modified behavior
### Example 1
```lean4
set_option autoImplicit true in
set_option relaxedAutoImplicit false in
def thisBreaks (x : α₂) (y : size₂) := ()
```
Before:
```
Unknown identifier `size₂`
```
After:
```
Unknown identifier `size₂`
Note: It is not possible to treat `size₂` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.
```
### Example 2
```lean4
set_option autoImplicit false in
def thisAlsoBreaks (x : α₃) (y : size₃) := ()
```
Before:
```
Unknown identifier `α₃`
Unknown identifier `size₃`
```
After:
```
Unknown identifier `α₃`
Note: It is not possible to treat `α₃` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
Unknown identifier `size₃`
Note: It is not possible to treat `size₃` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
```
## How this works
The elaboration process knows whether it is considering syntax where we
be able to auto-bind implicits thanks to information in the
`Lean.Elab.Term.Context`.
Before this PR, this contains:
* `autoBoundImplicit`, a boolean that is true when we are considering
syntax that might be able to auto-bind implicit AND when the
`autoImplicit` flag is set to true
* `autoBoundImplicits`, an array of `Expr` variables that we've
autobound
After this PR, this contains:
* `autoBoundImplicitCtx`, an option which is `some` **whenever** we are
considering syntax that might be able to auto-bind implicit, and carries
the array of exprs as well as a copy of the `autoImplicit` flag's value.
(The latter lets us re-implement the `autoBoundImplicit` flag for
backward compatibility.)
Therefore, rather than having access to "elaboration is in an
autobinding context && flag is enabled", it's possible to recover both
of those individual values, and give different information to the user
in cases where we didn't attempt autobinding but would have if different
options had been set.
## Rationale
The revised error message avoids offering much guidance — it doesn't
actively suggest setting the option to a different value or suggest
adding an implicit binding. Care needs to be taken here to make sure
advice is not misleading; as the accepted RFC in #6462 points out, a
substantial portion of autobinding failures are just going to be
misspellings.
I considered and then rejected a code action here to that would add a
local `set_option autoImplicit true`. This seems undesirable or
counterproductive — if a project like Mathlib has proactively disabled
`autoImplicit`, its odd to be pushing local exceptions.
A hint prompting the user to add an implicit binding would be more
proper, but only in certain circumstances — we want to be conservative
in suggesting specific code actions! In a situation like this one, we'd
want to _avoid_ giving the suggestion of adding a `{HasArr}` binding,
which I think either requires tricky heuristics or means we'd want the
elaboration to play through the consequences of auto-binding and make
sure it doesn't cause any follow-on errors before suggesting adding an
implicit binding.
```
set_option autoImplicit true
set_option relaxedAutoImplicit false
instance has_arr : HasArr Preorder := { Arr := Function }
```
Additionally, it seems like it would make the most sense to offer to
auto-bind _all_ the relevant unknown identifiers at once. To avoid being
misleading, this too would seem to require playing through the
consequences of autobinding before being able to safely suggest the
change. This is enough additional complexity that I'm leaving it for
future work.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This PR prevents symbol clashes between (non-`@[export]`) definitions
from different Lean packages.
Previously, if two modules define a function with the same name and were
transitively imported (even privately) by some downstream module,
linking would fail due to a symbol clash. Similarly, if a user defined a
symbol with the same name as one in the `Lean` library, Lean would use
the core symbol even if one did not import `Lean`.
This is solved by changing Lean's name mangling algorithm to include an
optional package identifier. This identifier is provided by Lake via
`--setup` when building a module. This information is weaved through the
elaborator, interpreter, and compiler via a persistent environment
extension that associates modules with their package identifier.
With a package identifier, standard symbols have the form
`lp_<pkg-id>_<mangled-def>`. Without one, the old scheme is used (i.e.,
`l_<mangled-def>`). Module initializers are also prefixed with package
identifier (if any). For example, the initializer for a module `Foo` in
a package `test` is now `initialize_test_Foo` (instead of
`initialize_Foo`). Lake's default for native library names has also been
adjusted accordingly, so that libraries can still, by default, be used
as plugins. Thus, the default library name of the `lean_lib Foo` in
`package test` will now be `libtest_Foo`.
When using Lake to build the Lean core (i.e., `bootstrap = true`), no
package identifier will be used. Thus, definitions in user packages can
never have symbol clashes with core.
Closes#222.
This PR adds a test that covers importing modules defined in multiple
packages.
Currently, will resolve the module to its first occurrence in the its
search order. However, this will soon change, so this test is designed
to analyze that behavior.
This PR redefines `String.take` and variants to operate on
`String.Slice`. While previously functions returning a substring of the
input sometimes returned `String` and sometimes returned
`Substring.Raw`, they now uniformly return `String.Slice`.
This is a BREAKING change, because many functions now have a different
return type. So for example, if `s` is a string and `f` is a function
accepting a string, `f (s.drop 1)` will no longer compile because
`s.drop 1` is a `String.Slice`. To fix this, insert a call to `copy` to
restore the old behavior: `f (s.drop 1).copy`.
Of course, in many cases, there will be more efficient options. For
example, don't write `f <| s.drop 1 |>.copy |>.dropEnd 1 |>.copy`, write
`f <| s.drop 1 |>.dropEnd 1 |>.copy` instead. Also, instead of `(s.drop
1).copy = "Hello"`, write `s.drop 1 == "Hello".toSlice` instead.
This PR adds `Std.Tricho r`, a typeclass for relations which identifies
them as trichotomous. This is preferred to `Std.Antisymm (¬ r · ·)` in
all cases (which it is equivalent to).
This PR is split from a future PR and adds the function
`String.Pos.next`, an alias (and soon to be correct name) of
`String.ValidPos.next`.
This is for boring bootstrapping reasons.
This PR extracts two modules from `Match.MatchEqs`, in preparation of
#11220
and to use the module system to draw clear boundaries between concerns
here.
This PR registers a node kind for `Lean.Parser.Term.elabToSyntax` in
order to support the `Lean.Elab.Term.elabToSyntax` functionality without
registering a dedicated parser for user-accessible syntax.
This PR adds intersection operation on `DHashMap`/`HashMap`/`HashSet`
and provides several lemmas about its behaviour.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR removes duplicated instance parameters in the standard library
and flips lemmas of the form `toList_eq_toListIter` into a form that is
suitable for `simp`.
This PR implements `elabToSyntax` for creating scoped syntax `s :
Syntax` for an arbitrary elaborator `el : Option Expr -> TermElabM Expr`
such that `elabTerm s = el`.
Roundtripping example implementing an elaborator imitating `let`:
```lean
elab "lett " decl:letDecl ";" e:term : term <= ty? => do
let elabE (ty? : Option Expr) : TermElabM Expr := do elabTerm e ty?
elabToSyntax elabE fun body => do
elabTerm (← `(let $decl:letDecl; $body)) ty?
#guard lett x := 42; (x + 1) = 43
```
This PR ensures that the `text` argument of `computeArtifact` is always
provided in Lake code, fixing a hashing bug with
`buildArtifactUnlessUpToDate` in the process.
Closes#11209
This PR avoids match splitter calculation from testing all quadratically
many pairs of alternatives for overlaps, by keeping track of possible
overlaps during matcher calculation, storing that information in the
`MatcherInfo`, and using that during matcher calculation.
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 provides a polymorphic `ForIn` instance for slices and an MPL
`spec` lemma for the iteration over slices using `for ... in`. It also
provides a version specialized to `Subarray`.
This PR fixes an error message in Lake which suggested incorrect
lakefile syntax.
The error message (which was very helpful by the way) looked like this:
```
error: TwoFX/batteries: package not found on Reservoir.
If the package is on GitHub, you can add a Git source. For example:
require ...
from git "https://github.com/TwoFX/batteries" @ git "main"
or, if using TOML:
[[require]]
git = "https://github.com/TwoFX/batteries"
rev = "main"
...
```
The suggested Lakefile syntax does not work. The correct syntax,
according to the reference manual and according to my tests, is
```
require ...
from git "https://github.com/TwoFX/batteries" @ "main"
```
without the second `git`.
This PR fixes a bug in the LCNF simplifier unearthed while working on
#11078. In some situations caused by `unsafeCast`, the simplifier would
record incorrect information about `cases`, leading to further bugs down
the line.
Suppose we have `v : NonScalar` due to an `unsafeCast` and we run
`cases` on it, expecting `Prod.mk fst snd`. The current code attempts to
record both the arguments from the constructor application in the case
arm `fst`, `snd` and the parameters for the type by inspecting the discr
`v`. However, `NonScalar` does of course not have any parameters,
causing the simplifier to record wrong information. This patch makes the
`cases` infrastructure more cautious when extracting information from
the type of `v`.
This PR changes how sparse case expressions represent the
none-of-the-above information. Instead of of many `x.ctorIdx ≠ i`
hypotheses, it introduces a single `Nat.hasNotBit mask x.ctorIdx`
hypothesis which compresses that information into a bitmask. This avoids
a quadratic overhead during splitter generation, where all n assumptions
would be refined through `.subst` and `.cases` constructions for all n
assumption of the splitter alternative.
The definition of `Nat.hasNotBit` uses `Nat.rightShift` which is fiddly
to get to reduce well, especially on open terms and with `Meta.whnf`.
Some experimentation was needed to find proof terms that work, these are
all put together in the `Lean.Meta.HasNotBit` module.
Fixes#11183
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR fixes the `reduceArity` compiler pass to consider
over-applications to functions that have their arity reduced.
Previously, this pass assumed that the amount of arguments to
applications was always the same as the number of parameters in the
signature. This is usually true, since the compiler eagerly introduces
parameters as long as the return type is a function type, resulting in a
function with a return type that isn't a function type. However, for
dependent types that sometimes are function types and sometimes not,
this assumption is broken, resulting in the additional parameters to be
dropped.
Closes#11131
This ensures that no `grind` annotated theorem, simply by being
instantiated, causes a chain of >20 further instantiations, with a small
list of documented exceptions.
This PR modifies the `try?` framework, so each subsidiary tactic runs
with a separate `maxHeartbeats` budget.
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR has `#grind_list check` produce a "Try this:" suggestion with
`#grind_list inspect` commands, as this is usually the next step in
dealing with problematic cases. We also fix the grind pattern for one
theorem, as part of testing the workflow. More to follow.
This PR fixes a few minor issues in the new `Action` framework used in
`grind`. The goal is to eventually delete the old `SearchM`
infrastructure. The main `solve` function used by `grind` is now based
on the `Action` framework. The PR also deletes dead code in `SearchM`.
Creates an inductive data type with 100 constructors, and a function
that does
matches on half of its constructors, with a catch-all for the other
half, and generates the splitter.
Related to #11183.
This PR renames `Substring` to `Substring.Raw`.
This is to signify its status as a second-class citizen (not deprecated,
but no real plans for verification, like `String.Pos.Raw`) and to free
up the name `Substring` for a possible future type `String.Substring :
String -> Type` so that `s.Substring` is the type of substrings of `s`.
The functions `String.toSubstring` and `String.toSubstring'` will remain
for now for bootstrapping reasons.
This PR implements `try?` using the new `finish?` infrastructure. It
also removes the old tracing infrastructure, which is now obsolete.
Example:
```lean
/--
info: Try these:
[apply] grind
[apply] grind only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
= HashMap.getElem_insert, #1bba]
[apply] grind only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
= HashMap.getElem_insert]
[apply] grind =>
instantiate only [findIdx, insert, = mem_indices_of_mem]
instantiate only [= getElem?_neg, = getElem?_pos]
cases #1bba
· instantiate only [findIdx]
· instantiate only
instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
-/
#guard_msgs in
example (m : IndexMap α β) (a : α) (b : β) :
(m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
try?
```
This PR modifies the error message that is returned when more than one
synthetic metavariable can't be resolved.
The two heuristics used for prioritization are:
- prefer typeclass problems associated with small ranges over typeclass
problems associated with large ranges (I'm pretty confident in this
heuristic)
- do not prefer typeclass problems over other kinds of errors (not as
confident in this heuristic)
This PR uses the new `grind_pattern` constraints to fix cases where an
unbounded number of theorem instantiations would be generated for
certain theorems in the standard library.
This PR implements `grind_pattern` constraints. They are useful for
controlling theorem instantiation in `grind`. As an example, consider
the following two theorems:
```lean
theorem extract_empty {start stop : Nat} :
(#[] : Array α).extract start stop = #[] := …
theorem extract_extract {as : Array α} {i j k l : Nat} :
(as.extract i j).extract k l = as.extract (i + k) (min (i + l) j) := …
```
If both are used for theorem instantiation, an unbounded number of
instances is generated as soon as we add the term `#[].extract i j` to
the `grind` context.
We can now prevent this by adding a `grind_pattern` constraint to
`extract_extract`:
```lean
grind_pattern extract_extract => (as.extract i j).extract k l where
as =/= #[]
```
With this constraint, only one instance is generated, as expected:
```lean
/-- trace: [grind.ematch.instance] extract_empty: #[].extract i j = #[] -/
#guard_msgs (drop error, trace) in
set_option trace.grind.ematch.instance true in
example (as : Array Nat) (h : #[].extract i j = as) : False := by
grind only [= extract_empty, usr extract_extract]
```
This PR changes all module build keys in Lake to be scoped by their
package. This enables building modules with the same name in different
packages (something previously only well-supported for executable
roots).
API-wise, the `BuildKey` definitions `module` and `moduleFacet` have
been deprecated and replaced with `packageModule` and
`packageModuleFacet`. The `moduleTargetIndicator` has also been removed
(with its purpose subsumed by `packageModule`).
This PR adds syntax for specifying `grind_pattern` constraints and
extends the `EMatchTheorem` object.
---
Note: We need a manual stage0 update because it affects the .olean
files.
This PR removes most cases where an error message explained that it was
"probably due to metavariables," giving more explanation and a hint.
## Example
```
def square x := x * x
```
Before:
```lean4
typeclass instance problem is stuck, it is often due to metavariables
HMul ?m.9 ?m.9 (?m.3 x)
```
After:
```
typeclass instance problem is stuck
HMul ?m.9 ?m.9 (?m.3 x)
Note: Lean will not try to resolve this typeclass instance problem because the
first and second type arguments to `HMul` are metavariables. These arguments
must be fully determined before Lean will try to resolve the typeclass.
Hint: Adding type annotations and supplying implicit arguments to functions
can give Lean more information for typeclass resolution. For example, if you
have a variable `x` that you intend to be a `Nat`, but Lean reports it as
having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get
typeclass resolution un-stuck.
```
In addition to providing beginner-and-intermediate-friendly explanation
about **why** typeclass instance problems are treated as "stuck" when
metavariables appear in output positions, this PR provides
potentially-valuable improvement even to expert users: it explains
**which of the typeclass arguments are inputs** and therefore need to be
fully specified before typeclass resolution will be attempted. This
information can be tricky to find otherwise.
## Next steps, but probably after this PR
* error explanation
* detecting when the syntactic source is a binop and giving a
special-cased explanation on the binary operators and their associated
typeclasses
* detecting when the syntactic source is a function call, inspecting the
function call's type somewhat, and replacing the generic "replace `x`
with `(x : Nat)` hint with a specialized "replace `foo` with `foo (tyArg
:= Nat)`" hint
This PR introduces slices of lists that are available via slice notation
(e.g., `xs[1...5]`).
* Moved the `take` combinator and the `List` iterator producer to
`Init`.
* Introduced a `toTake` combinator: `it.toTake` behaves like `it`, but
it has the same type as `it.take n`. There is a constant cost per
iteration compared to `it` itself.
* Introduced `List` slices. Their iterators are defined as
`suffixList.iter.take n` for upper-bounded slices and
`suffixList.iter.toTake` for unbounded ones.
Performance characteristics of using the slice `list[a...b]`:
* when creating it: `O(a)`
* every iterator step: `O(1)`
* `toList`: `O(b - a + 1)` (given that a <= b)
Because the slice only stores a suffix of `xs` internally, two slices
can be equal even though the underlying lists differ in an irrelevant
prefix. Because the `stop` field is allowed to be beyond the list's
upper bound, the slices `[1][0...1]` and `[1][0...2]` are not equal,
even though they effectively cover the same range of the same list.
Improving this would require us to call `List.length` when building the
slice, which would iterate through the whole list.
This PR replaces #11138, which just added a `@[csimp]` lemma for
`Int.pow`, this time actually replacing the definition. This means we
not only get fast runtime behaviour, but take advantage of the special
kernel support for `Nat.pow`.
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR adds tactic and term mode macros for `∎` (typed `\qed`) which
expand to `try?`. The term mode version captures any produced
suggestions and prepends `by`.
Co-authored-by: Claude <noreply@anthropic.com>
This PR removes `simp_all? +suggestions` from `try?` for now. It's
really slow out in Mathlib; too often the suggestions cause `simp` to
loop. Until we have the ability for `try?` to move past a timeing-out
tactic (or maybe even until we have parallelism), it needs to be
removed.
Alternatively, we could try modifying `simp` so that e.g. it won't use a
premise more than once. This might help avoid loops, but it would
produce less-reproducible proofs.
Co-authored-by: Claude <noreply@anthropic.com>
This PR ensures that tactics using library suggestions set the caller
field, so the premise selection engine has access to this. We'll later
use this to filter out some modules for grind, which we know have
already been fully annotated.
Co-authored-by: Claude <noreply@anthropic.com>
This PR implements support for `#grind_lint check in module <module>`.
Mathlib does not use namespaces, so we need to restrict the
`#grind_lint` search space using module (prefix) names. Example:
```lean
/--
info: instantiating `Array.filterMap_some` triggers more than 100 additional `grind` theorem instantiations
---
info: Array.filterMap_some
[thm] instances
[thm] Array.filterMap_filterMap ↦ 94
[thm] Array.size_filterMap_le ↦ 5
[thm] Array.filterMap_some ↦ 1
---
info: instantiating `Array.range_succ` triggers 22 additional `grind` theorem instantiations
-/
#guard_msgs in
#grind_lint check (min := 20) in module Init.Data.Array
```
This PR changes the default library suggestions (e.g. for `grind
+suggestions` or `simp_all? +suggestions) to include the theorems from
the current file in addition to the output of Sine Qua Non.
This PR implements the following improvements to the `#grind_lint`
command:
1. More informative messages when the number of instances exceeds the
minimum threshold.
2. A code action for `#grind_lint inspect` that inserts
`set_option trace.grind.ematch.instance true` whenever the number of
instances exceeds
the minimum threshold.
3. Displaying doc strings for `grind` configuration options in
`#grind_lint`.
4. Improve doc strings for `#grind_lint inspect` and `#grind_lint
check`.
Example:
```lean
/--
info: instantiating `Array.filterMap_some` triggers more than 100 additional `grind` theorem instantiations
---
info: Array.filterMap_some
[thm] instances
[thm] Array.filterMap_filterMap ↦ 94
[thm] Array.size_filterMap_le ↦ 5
[thm] Array.filterMap_some ↦ 1
---
info: Try this to display the actual theorem instances:
[apply] set_option trace.grind.ematch.instance true in
#grind_lint inspect Array.filterMap_some
-/
#guard_msgs in
#grind_lint inspect Array.filterMap_some
```
This PR renames `String.Iterator` to `String.Legacy.Iterator`.
From the docstring of `String.Legacy.Iterator`:
> This is a no-longer-supported legacy API that will be removed in a
future release. You should use
> `String.ValidPos` instead, which is similar, but safer. To iterate
over a string `s`, start with
> `p : s.startValidPos`, advance it using `p.next`, access the current
character using `p.get` and
> check if the position is at the end using `p = s.endValidPos` or
`p.IsAtEnd`.
This PR adds a test replicating Kim's diamond dependency example.
The top-level package, `D`, depends on two intermediate packages, `B`
and `C`, which each require semantically different versions of another
package, `A`. The portion of `A` that `B` and `C` publicly use is
unchanged across the versions, but they both privately make use of
changed API. Currently, this causes a version clash. This will be made
to work without error later this quarter.
This PR fixes some details in the Markdown renderings of Verso
docstrings, and adds tests to keep them correct. Also adds tests for
Verso docstring metadata.
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 adds a user-extension mechanism for the `try?` tactic. You can
either use the `@[try_suggestion]` attribute on a declaration with
signature ``MVarId -> Try.Info -> MetaM (Array (TSyntax `tactic))`` to
produce suggestions, or the `register_try?_tactic <stx>` command with a
fixed piece of syntax. User-extensions are only tried *after* the
built-in try strategies have been tried and failed.
I wanted to ensure that if the user provides a tactic that produces a
"Try this:" suggestion, we both emit the original tactic and the
suggested replacement (this is what we already do with `grind` and
`simp`). I have this working, but it is quite hacky: we grab the message
log and parse it. I fear this will break when the "Try this:" format is
inevitably changed in the future.
<!-- CURSOR_SUMMARY -->
---
> [!NOTE]
> Adds user-defined suggestion generators for `try?` via
`@[try_suggestion]` and `register_try?_tactic`, executed after built-ins
with priority and double-suggestion handling.
>
> - **Parser/Command**:
> - Add command syntax `register_try?_tactic (priority := n)?
<tacticSeq>` in `Lean.Parser.Command`.
> - **Suggestion registry**:
> - Introduce `@[try_suggestion (prio)]` attribute with a scoped env
extension to register generators (`MVarId → Try.Info → MetaM (Array
(TSyntax `tactic))`).
> - Priority ordering (higher first); supports local/global scope.
> - **Tactic engine (`try?`)**:
> - New unsafe pipeline to collect and run user generators after
built-in tactics; expands nested "Try this" outputs from user tactics.
> - `mkTryEvalSuggestStx` now takes `(goal, info)`; integrates user
tactics as fallback via `attempt_all`.
> - Suppress intermediate "Try this" messages during `evalAndSuggest` by
restoring the message log.
> - **Imports**:
> - Add `meta import Lean.Elab.Command` for command elaboration.
> - **Tests**:
> - `try_register_builtin.lean`: command availability and warning
without import.
> - `try_user_suggestions.lean`: basic, priority, built-in fallback,
double-suggestion, and command registration cases.
> - Update `versoDocMissing.lean.expected.out` to include
`register_try?_tactic` in expected commands.
>
> <sup>Written by [Cursor
Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit
302dc94544. This will update automatically
on new commits. Configure
[here](https://cursor.com/dashboard?tab=bugbot).</sup>
<!-- /CURSOR_SUMMARY -->
This PR replaces `Iter(M).size` with the `Iter(M).count`. While the
former used a special `IteratorSize` type class, the latter relies on
`IteratorLoop`. The `IteratorSize` class is deprecated. The PR also
renames lemmas about ranges be replacing `_Rcc` with `_rcc`, `_Rco` with
`_roo` (and so on) in names, in order to be more consistent with the
naming convention.
This PR adds a new, inactive and unused `doElem_elab` attribute that
will allow users to register custom elaborators for `doElem`s in the
form of the new type `DoElab`. The old `do` elaborator is active by
default but can be switched off by disabling the new option
`backward.do.legacy`.
This PR fixes a bug in #11125. Added a test this time ...
<!-- CURSOR_SUMMARY -->
---
> [!NOTE]
> Exclude deprecated declarations from library suggestions and add a
test verifying they are filtered out.
>
> - **Library Suggestions**:
> - Update `isDeniedPremise` in `src/Lean/LibrarySuggestions/Basic.lean`
to treat `Lean.Linter.isDeprecated` as denied (`true`), filtering
deprecated constants from suggestions.
> - **Tests**:
> - Add `tests/lean/run/library_suggestions_deprecated.lean` to verify
deprecated theorems (e.g., `deprecatedTheorem`) are not suggested by
`currentFile`, while non-deprecated ones are.
>
> <sup>Written by [Cursor
Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit
ef7e546dbc. This will update automatically
on new commits. Configure
[here](https://cursor.com/dashboard?tab=bugbot).</sup>
<!-- /CURSOR_SUMMARY -->
This PR adds iterators and slices for `DTreeMap`/`TreeMap`/`TreeSet`
based on zippers and provides basic lemmas about them.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR aims to bring the performance of `String.ValidPos` closer to
that of `String.Pos.Raw` by adding/correcting `extern` annotations as
needed.
This is in response to a regression observed after #11127. The changes
to the `String` `Parsec` module lead to different compiler behavior for
functions like `strCore` and `natCore`. The new IR *looks* better than
the old IR, but the
[numbers](1e438647ba)
are a bit mixed.
This PR removes all uses of `String.Iterator` from core, preferring
`String.ValidPos` instead.
In an upcoming PR, `String.Iterator` will be renamed to
`String.Legacy.Iterator`.
This PR adds support for `try?` to use induction; it will only perform
induction on inductive types defined in the current namespace and/or
module; so in particular for now it will not induct on built-in
inductives such as `Nat` or `List`.
This is stacked on top of #11132, and there are overlapping changes.
<!-- CURSOR_SUMMARY -->
---
> [!NOTE]
> Adds vanilla induction suggestions to `try?`, updates collection of
inductive candidates, and tests the new behavior on custom inductive
types.
>
> - **Try tactic pipeline**:
> - Add vanilla induction generators (`mkIndStx`, `mkAllIndStx`) that
try `induction <var> <;> …`, with fallback via `expose_names` when
needed.
> - Integrate induction into `mkTryEvalSuggestStx`, alongside existing
atomic, suggestions, and function-induction options.
> - **Collector updates (`Try/Collect.lean`)**:
> - Enhance `checkInductive` to `whnf` the type and use `getAppFn` to
detect inductive heads, populating `indCandidates`.
> - **Tests**:
> - New `tests/lean/run/try_induction.lean` covering suggestions for
`induction` on custom inductives, interaction with `grind`, and
coexistence with `fun_induction`.
>
> <sup>Written by [Cursor
Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit
b357990c97. This will update automatically
on new commits. Configure
[here](https://cursor.com/dashboard?tab=bugbot).</sup>
<!-- /CURSOR_SUMMARY -->
---------
Co-authored-by: Claude <noreply@anthropic.com>
This PR adds a `csimp` lemma for faster runtime evaluation of `Int.pow`
in terms of `Nat.pow`.
<!-- CURSOR_SUMMARY -->
---
> [!NOTE]
> Replaces `Int.pow` evaluation with a `@[csimp]` lemma using `Nat.pow`
and adds supporting lemmas (`pow_mul`, `neg_pow`, nonneg results).
>
> - **Performance/runtime**:
> - Introduce `powImp` and `@[csimp]` theorem `pow_eq_powImp` to
evaluate `Int.pow` via `Nat.pow` with sign handling.
> - **Math lemmas (supporting)**:
> - `Int.pow_mul`: `a ^ (n * m) = (a ^ n) ^ m`.
> - `Int.sq_nonnneg`: nonnegativity of `m ^ 2`.
> - `Int.pow_nonneg_of_even`: nonnegativity for even exponents.
> - `Int.neg_pow`: `(-m)^n = (-1)^(n % 2) * m^n`.
>
> <sup>Written by [Cursor
Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit
66ac236db7. This will update automatically
on new commits. Configure
[here](https://cursor.com/dashboard?tab=bugbot).</sup>
<!-- /CURSOR_SUMMARY -->
This PR adds support for `grind +suggestions` and `simp_all?
+suggestions` in `try?`. It outputs `grind only [X, Y, Z]` or `simp_all
only [X, Y, Z]` suggestions (rather than just `+suggestions`).
Co-authored-by: Claude <noreply@anthropic.com>
This PR fixes disequality propagation for constructor applications in
`grind`. The equivalence class representatives may be distinct
constructor applications, but we must ensure they have the same type.
Examples that were panic'ing before this PR:
```lean
example (a b : List Nat)
: a ≍ ([] : List Int) → b ≍ ([1] : List Int) → a = b ∨ p → p := by
grind
example (a b : List Nat)
: a = [] → a ≍ ([] : List Int) → b = [1] → a = b ∨ p → p := by
grind
example (a b : List Nat)
: a = [] → a ≍ ([] : List Int) → b = [1] → b ≍ [(1 : Int)] → a = b ∨ p → p := by
grind
example (a b : List Nat)
: a = [] → b = [1] → a = b ∨ p → p := by
grind
example (a b : List Nat)
: a = [] → a ≍ ([] : List Int) → b = [1] → a = b ∨ p → p := by
grind
```
Closes#11124
This PR fixes a typo in the doc string of `List.finIdxOf?`. The first
line of the doc string previously says the function returns the size of
the list if no element equal to `a`, but both the examples in the doc
string and real run-time behavior indicate it returns `none` in this
case.
Closes#11110
This PR fixes a problem for structures with diamond inheritance: rather
than copying doc-strings (which are not available unless `.server.olean`
is loaded), we link to them. Adds tests.
This PR adds `Job.sync` as a standard way of declaring a synchronous
job.
It makes some non-behavior changes to related Job APIs to improve
compilation.
This PR lets the match compilation procedure use sparse case analysis
when the patterns only match on some but not all constructors of an
inductive type. This way, less code is produce. Before, code handling
each of the other cases was then optimized and commoned-up by later
compilation pipeline, but that is wasteful to do.
In some cases this will prevent Lean from noticing that a match
statement is complete
because it performs less case-splitting for the unreachable case. In
this case, give explicit
patterns to perform the deeper split with `by contradiction` as the
right-hand side.
At least temporarily, there is also the option to disable this behaviour
with
```
set_option backwards.match.sparseCases false
```
This PR removes the `verifyEnum` functions from the bv_decide frontend.
These functions looked at the implementation of matchers to see if they
really do the matching that they claim to do. This breaks that
abstraction barrier, and should not be necessary, as only functions with
a `MatcherInfo` env entry are considered here, which should all play
nicely.
This PR adds `theorem Int.ediv_pow {a b : Int} {n : Nat} (hab : b ∣ a) :
(a / b) ^ n = a ^ n / b ^ n` and related lemmas.
---------
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
This PR adds “sparse casesOn” constructions. They are similar to
`.casesOn`, but have arms only for some constructors and a catch-all
(providing `t.ctorIdx ≠ 42` assumptions). The compiler has native
support for these constructors and now (because of the similarity) also
the per-constructor elimination principles.
This PR ensures that the `denote` functions used to implement
proof-by-reflection terms in `grind` are abbreviations. This change
eliminates the need for the `withAbstractAtoms` gadget.
This PR fixes a panic during equality propagation in the `grind ring`
module. If the maximum number of steps has been reached, the polynomials
may not be fully simplified.
Closes#11073
This PR adds union operations on DTreeMap/TreeMap/TreeSet and their raw
variants and provides lemmas about union operations.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR enables Lake users to require Reservoir dependencies by a
semantic version range. On a `lake update`, Lake will fetch the
package's version information from Reservoir and select the newest
version of the package that satisfies the range.
### Using Version Ranges
Version ranges can be specified through the `version` field of a TOML
`require` or the `@` clause of a Lean `require`. They are only
meaningful on Reservoir dependencies.
**lakefile.lean**
```lean-4
require "Seasawher" / "mdgen" @ "2.*"
```
**lakefile.toml**
```toml
[[require]]
name = "mdgen"
scope = "Seasawher"
version = "2.*"
```
The syntax for these versions ranges is a mix of
[Rust's](https://doc.rust-lang.org/stable/cargo/reference/specifying-dependencies.html?highlight=caret#version-requirement-syntax)
and
[Node's](https://github.com/npm/node-semver/tree/v7.7.3?tab=readme-ov-file#ranges)
with some Lean-friendly deviations.
### Comparators
The basic unit of semantic version ranges are version comparators. They
take a base version and a comparison operator and match versions which
compare positively with their base. Lake supports the following
comparison operators.
* `<`, `<=` / `≤`, `>`, `>=` / `≥`, `=`, `!=` / `≠`
Unlike Rust and Node, Lake supports Unicode alternatives for the
operators. It also adds the not-equal operator (`!=` / `≠`) to make
excluding broken versions easier.
Comparators can be combined into clauses via conjunction or disjunction:
* **AND clauses**: Rust-style `≥1.2.3, <1.8.0` or Node-style `1.2.3
<1.8.0`
* **OR clauses**: Node-style `1.2.7 || >=1.2.9, <2.0.0`
When the base version of a comparator has a `-` suffix (e.g.,
`>1.2.3-alpha.3`) it will match versions of the same core (`1.2.3`) with
suffixes that lexicographically compare (e.g., `1.2.3-alpha.7` or
`1.2.3-beta.2`) but will not match suffixed versions of different cores
(e.g., `3.4.5-rc5`). An empty `-` suffix can be used to disable this
behavior. For example, `<2.0.0-` will match `1.2.3-beta.2` and
`2.0.0-alpha.1`.
### Range Macros
In addition to the basic comparators, Lake also supports standard
shorthand for specifying more complex ranges. Namely, it supports the
caret (`^`) and tilde (`~`) operator along with wildcard ranges.
**Caret Ranges**
* `^1` => `≥1.0.0, <2.0.0-`
* `^1.2` => `≥1.2.0, <2.0.0-`
* `^1.2.3` => `≥1.2.3, <2.0.0-`
* `^1.2.3-beta.2` => `≥1.2.3-beta.2, <2.0.0-`
* `^0.2` => `≥0.0.0, <0.3.0-`
* `^0.2.3` => `≥0.2.3, <0.3.0-`
* `^0.0.3` => `≥0.0.3, <0.0.4-`
* `^0` => `≥0.0.0, <1.0.0-`
* `^0.0` => `≥0.0.0, <0.1.0-`
**Tilde Ranges**
* `~1` => `≥1.0.0, <2.0.0-`
* `~1.2` => `≥1.2.0, <1.3.0-`
* `~1.2.3` => `≥1.2.3, <1.3.0-`
* `~1.2.3-beta.2` => `≥1.2.3-beta.2, <1.3.0-`
* `^0` => `≥0.0.0, <1.0.0-`
* `^0.2.3` => `≥0.2.3, <0.3.0-`
* `^0.0.3` => `≥0.0.3, <0.0.4-`
* `~0` => `≥0.0.0, <1.0.0-`
* `~0.0` => `≥0.0.0, <0.1.0-`
* `~0.0.0` => `≥0.0.0, <0.1.0-`
**Wildcard Ranges**
* `*` => `≥0.0.0`
* `1.x` => `≥1.0.0, <2.0.0-`
* `1.*.x` => `≥1.0.0, <2.0.0-`
* `1.2.*` => `≥1.2.0, <1.3.0-`
These ranges closely follow Rust's and Node's syntax. Like Node but
unlike Rust, wildcard ranges support `x` and `X` as alternative syntax
for wildcards.
This PR implements `simp? +suggestions`, which uses the configured
library suggestion engine to add relevant theorems to the `simp` call.
`simp +suggestions` without the `?` prints a message requiring adding
the `?`.
This PR changes Lake's debug build type to use `-O0` instead of `-Og`
when compiling C code. `-Og` was found to be insufficient for debugging
compiled Lean code -- relevant code was stilled optimized out.
This PR changes `Nat.ble` by joining the two `Nat.ble Nat.zero _` cases
into one, allowing `decide (0 <= x) = true` and `decide (0 < succ x) =
true` to be solvable by `rfl`.
This PR fixes `ST.Ref.ptrEq` to act as described in the docs. This fixes
two bugs:
1. The recent `IO.RealWorld` elimination PR overlooked this function
(afaik this is the only one),
causing its return value to be generally wrong.
2. The implementation of `ptrEq` would previously always consider two
different cells with pointer
equivalent value to be pointer equal. However, the function is supposed
to check whether two
`Ref` are the same cell, not whether the contained elements are.
This PR implements equality propagation for `Nat` in `grind order`.
`grind order` supports offset equalities for rings, but it has an
adapter for `Nat`. Example:
```lean
example (a b : Nat) (f : Nat → Int) : a ≤ b + 1 → b + 1 ≤ a → f (1 + a) = f (1 + b + 1) := by
grind -offset -mbtc -lia -linarith (splits := 0)
```
This PR implements (nested term) equality propagation in `grind order`.
That is, it propagates implied equalities from `grind order` back to the
`grind` core. Examples:
```lean
open Lean Grind Std
example [LE α] [IsPartialOrder α] (a b : α) (f : α → Nat) : a ≤ b → b ≤ c → c ≤ a → f a = f b := by
grind (splits := 0)
example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrder α] [OrderedRing α]
(a b : α) (f : α → Int) : a ≤ b + 1 → b ≤ a - 1 → f a = f (2 + b - 1) := by
grind -mbtc -lia -linarith (splits := 0)
example (a b : Int) (f : Int → Int) : a ≤ b + 1 → b ≤ a - 1 → f a = f (2 + b - 1) := by
grind -mbtc -lia -linarith (splits := 0)
```
`prelude-injectivity.lean` was testing inj thm generation for all
inductives in core, including private ones, which could lead to name
clashes that should not be able to occur in actual files. Put it under
the module system to not load private decls in the first place.
This PR enforces users of the constant folder API to provide proofs of
their algebraic properties,
thus hopefully avoiding bugs such as #11042 and #11043 in the future.
This PR fixes a case of overeager constant folding on Nat where the
compiler would mistakenly assume `0 - x = x` (see also #11042 for the
same bug on UInts).
This PR adds a new suggestion to `finish?`. It now generates the `grind`
tactic script as before, and a `finish only` tactic. Example:
```lean
/--
info: Try these:
[apply] ⏎
instantiate only [findIdx, insert, = mem_indices_of_mem]
instantiate only [= getElem?_neg, = getElem?_pos]
cases #1bba
· instantiate only [findIdx]
· instantiate only
instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
[apply] finish only [findIdx, insert, = mem_indices_of_mem, = getElem?_neg, = getElem?_pos, = HashMap.mem_insert,
= HashMap.getElem_insert, #1bba]
-/
example (m : IndexMap α β) (a : α) (b : β) :
(m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
grind => finish?
```
This PR establishes `String.ofList` and `String.toList` as the preferred
method for converting between strings and lists of characters and
deprecates the alternatives `String.mk`, `List.asString` and
`String.data`.
This PR updates the `pr-title` CI check to enforce that the commit
message does not start with a capital letter followed by a non-capital
letter.
This should ensure that messages do not start with a capitalized word,
but allow messages that start with an acronym.
This PR adds a library suggestion engine for local theorems. To be
useful, I still need to write more combinators to re-rank and combine
suggestions from multiple engines.
This is stacked on top of #11029.
This PR changes the terminology used from "premise selection" to
"library suggestions". This will be more understandable to users (we
don't assume anyone is familiar with the premise selection literature),
and avoids a conflict with the existing use of "premise" in Lean
terminology (e.g. "major premise" in induction, as well as generally the
synonym for "hypothesis"/"argument").
This PR improves match compilation: Branch on variables in the order
suggested by the first remaining alternative, and do not branch when the
first remaining alternative does not require it. This fixes
https://github.com/leanprover/lean4/issues/10749. With `set_option
backwards.match.rowMajor false` the old behavior can be turned on.
(For now this is an experiment to get familiar with the code and the
whole
problem domain. It is likely overly naive.)
This PR renames theorems that use `sorted` in their name to instead use
`pairwise`.
Closes#10742.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This PR improves the detection of situations where we branch multiple
times on the same value in the
code generator. Previously this would only consider repeated branching
on function arguments, now on
arbitrary values.
Closes: #11018
When documenting smul : M → α → α, it is unintuitive and confusing to
use variables a:M and b:α. It is better to use m:M and a:α. I also
specified the types of all involved terms in the documentation text.
This PR improves join point finding in the compiler through two means:
1. We now handle situations where a function `f` can only become a join
point when a function `g`
becomes a join point as well correctly.
2. We introduce a second join point finding pass after specialisation
and before the following
simplification pass, as the specialiser might have introduced new join
point opportunities for
the simplifier to exploit.
Notably in the code from #10995 we now correctly detect the missing join
point which required both
of these changes to be made.
Closes: #10995
This PR extracts some refactorings from #10763, including dropping dead
code and not failing in `inaccessibleAsCtor`, which leadas to (slightly)
better error messages, and also on the grounds that the failing
alternative may actually be unreachable.
This PR makes the eager lambda lifting heuristic more predictable by
blocking it from lifting from
any kind of inlineable function, not just `@[inline]`. It also adapts
the doc-string to describe
what is actually going on.
This PR inlines several Decidable instances for performance reasons.
Unlike the previous #10934 it does not attempt to also simplify the
Decidable instance system as
that has proven to have non trivial performance impact.
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR fixes a memleak caused by the Lean based `IO.waitAny`
implementation by reverting it.
This the faulty Lean implementation:
```lean
def IO.waitAny (tasks : @& List (Task α)) (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) :
BaseIO α := do
have : Nonempty α := ⟨tasks[0].get⟩
let promise : IO.Promise α ← IO.Promise.new
tasks.forM <| fun t => BaseIO.chainTask (sync := true) t promise.resolve
return promise.result!.get
```
In a situation where we call this function repeatedly in a loop with a
pair of tasks `[t1, t2]`
where `t2` is a long lived task that we pass every time and `t1` is
fresh a short lived task, `t2` will
accumlate more and more children from `BaseIO.chainTask` that fill
memory over time. The old C++
implementation did not have this issue so we are reverting.
This PR defines `String.Slice.replace` and redefines `String.replace` to
use the `Slice` version.
The new implementation is generic in the pattern, so it supports things
like `"education".replace isVowel "☃!" = "☃!d☃!c☃!t☃!☃!n"`. Since it
uses the `ForwardSearcher` infrastructure, `String` patterns are
searched using KMP, unlike the previous implementation which had
quadratic runtime. As a side effect, the behavior when replacing an
empty string now matches that of most other programming languages,
namely `"abc".replace "" "k" = "kakbkck"`.
This PR fixes the KMP implementation, which did incorrect bookkeeping of
the backtracking process, leading to incorrect starting ranges of
matches.
The new implementation does not require `partial` anywhere.
This PR adds support for specifying anchors to restrict the search space
in `grind` when using `grind only`. Anchors can limit which case splits
are performed and which local lemmas are instantiated.
This PR adds the `set_config` tactic for setting `grind` configuration
options. It uses the same syntax used for setting configuration options
in the `grind` main tactic.
This PR tries to preserve names of pattern variables in match
alternatives in `decreasing_by`, by telescoping into the concrete
alternative rather than the type of the matcher's alt. Fixes#10976.
This PR ensures that searching for an empty string returns the expected
pattern of alternating size-zero matches and size-one rejects.
In particular, splitting by an empty string returns an array formed of
the empty string, all of the string's characters as singleton strings,
followed by another empty string. This matches the [Rust
behavior](https://doc.rust-lang.org/std/primitive.str.html#method.split),
for example.
This PR adds inline annotations to several `Decidable` instances.
Additionally, it removes the `Decidable` instance for `p → q` which is
made redundant by `forall_prop_decidable`.
This PR changes the closure allocator to use the general allocator
instead of the small object one.
This is because users may create closures with a gigantic amount of
closed variables which in turn
boost the size of the closure beyond the small object threshold.
This issue was uncovered by #10979. Detecting that the small object
threshold is at fault requires
building mimalloc in debug mode at which point it yields:
```
mimalloc: assertion failed: at "/home/henrik/lean4/build/debug/mimalloc/src/mimalloc/src/alloc.c":132, mi_heap_malloc_small_zero
assertion: "size <= MI_SMALL_SIZE_MAX"
```
The generated code at fault here looks as follows:
```c
LEAN_EXPORT lean_object* l_initExec___at___00res_spec__0(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_2 = lean_alloc_closure((void*)(l_initializer_ext___at___00initExec___at___00res_spec__0_spec__0___lam__0___boxed), 3, 0);
x_3 = l_initExec___redArg___closed__0;
x_4 = l_initExec___redArg___closed__1;
x_5 = l_instMonadLiftNonDetT___closed__0;
x_6 = l_initExec___redArg___closed__2;
x_7 = l_initExec___at___00res_spec__0___closed__0;
lean_inc_ref(x_2);
x_8 = lean_alloc_closure((void*)(l_initExec___at___00res_spec__0___lam__29___boxed), 213, 212);
lean_closure_set(x_8, 0, x_3);
lean_closure_set(x_8, 1, x_2);
lean_closure_set(x_8, 2, x_4);
lean_closure_set(x_8, 3, x_3);
lean_closure_set(x_8, 4, x_4);
lean_closure_set(x_8, 5, x_3);
lean_closure_set(x_8, 6, x_4);
lean_closure_set(x_8, 7, x_3);
lean_closure_set(x_8, 8, x_4);
lean_closure_set(x_8, 9, x_3);
lean_closure_set(x_8, 10, x_4);
lean_closure_set(x_8, 11, x_3);
lean_closure_set(x_8, 12, x_4);
lean_closure_set(x_8, 13, x_3);
lean_closure_set(x_8, 14, x_4);
lean_closure_set(x_8, 15, x_5);
lean_closure_set(x_8, 16, x_6);
lean_closure_set(x_8, 17, x_5);
lean_closure_set(x_8, 18, x_5);
lean_closure_set(x_8, 19, x_5);
lean_closure_set(x_8, 20, x_5);
lean_closure_set(x_8, 21, x_5);
lean_closure_set(x_8, 22, x_5);
...
```
With the crash happening in `lean_alloc_closure` where we
unconditionally invoke the small allocator
which cannot cope with closures this large. Hopefully changing this to
the general purpose allocator
doesn't have too much of an impact on performance.
Closes: #10979
This PR adds the basic infrastructure to perform termination proofs
about `String.ValidPos` and `String.Slice.Pos`.
We choose approach where the intended way to do termination arguments is
to argue about the position itself rather than some projection of it
like `remainingBytes`.
The types `String.ValidPos` and `String.Slice.Pos` are equipped with a
`WellFoundedRelation` instance given by the greater-than relation. This
means that if a function takes a position `p` and performs a recursive
call on `q`, then the decreasing obligation will be `p < q`. This works
well in the common case where `q` is `p.next h`, in which case the goal
`p < p.next h` is solved by the simplifier.
For stepping through a string backwards, we introduce a type synonym
with a `WellFoundedRelation` instance given by the less-than relation.
This means that if a function takes a position `p` and performs a
recursive call on `q` and specifies `termination_by p.down`, then the
decreasing obligation will be `q < p`. This works well in the case where
`q` is `p.prev h`, in which case the goal `p.prev h < p` is solved by
the simplifier.
For termination arguments invoving multiple strings, the lower-level
primitive `p.remainingBytes` (landing in `Nat`) is also available.
In a future PR, we will additionally provide the necessary typeclasses
instances to register `String.ValidPos` and `String.Slice.Pos` with
`grind` to make complex termination arguments more convenient in user
code.
This PR performs more widening in ElimDeadBranches in an attempt to
improve performance in situations with a lot of local precision.
While this is not enough to make the compilation instant it pushes
compilation time from 12s to 3s for the example in #10857 and barely
introduces regressions so it seems like a good first step in this
direction.
Closes: #10857
This PR implements the following `grind` improvements:
1. `set_option` can now be used to set `grind` configuration options in
the interactive mode.
2. Fixes a bug in the repeated theorem instantiation detection.
3. Adds the macro `use [...]` as a shorthand for `instantiate only
[...]`.
This PR adds the combinator ` · t_1 ... t_n` to the `grind` interactive
mode. The `finish?` tactic now generates scripts using this combinator
to conform to Mathlib coding standards. The new format is also more
compact. Example:
```lean
/--
info: Try this:
[apply] ⏎
instantiate only [= mem_indices_of_mem, insert, = getElem_def]
instantiate only [= getElem?_neg, = getElem?_pos]
cases #f590
· cases #ffdf
· instantiate only
instantiate only [= Array.getElem_set]
· instantiate only
instantiate only [size, = HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
· instantiate only [= mem_indices_of_mem, = getElem_def]
instantiate only [usr getElem_indices_lt]
instantiate only [size]
cases #ffdf
· instantiate only [=_ WF]
instantiate only [= getElem?_neg, = getElem?_pos, = Array.getElem_set]
instantiate only [WF']
· instantiate only
instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert, = Array.getElem_push]
-/
#guard_msgs in
example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
(m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
grind => finish?
```
This PR ensures that model-based theory combination in `grind cutsat`
considers nonlinear terms. Nonlinear multiplications such as `x * y` are
treated as uninterpreted symbols in `cutsat`.
Closes#10885
This PR adds support for scientific literals for `Rat` in `grind`.
`grind` does not yet add support for this kind of literal in arbitrary
fields.
closes#10489
This PR fixes a bug in the equality propagation procedure in
`grind.order`. Specifically, it affects the procedure that asserts
equalities in the `grind` core state that are implied by (ring)
inequalities in the `grind.order` module.
closes#10622
This is a guard against #10705; if a kernel error is raised when the
return value of this function is eventually checked, it is often
silenced downstream, making it hard to spot the failure.
If we panic here via `assert!`, then the diagnostic cannot be missed.
This PR adds the `mbtc` tactic to the `grind` interactive mode. It
implements model-based theory combination. It also ensures `finish?` is
capable of generating it.
This PR ensures that solver propagation steps are necessary in the
generated tactic script to close the goal.
It produces more compact proof scripts, but this is not just an
optimization, if we include an unnecessary step, we may fail to replay
the generated script when `cases` steps are pruned using
non-chronological backtracking (NCB). For example, when executing
`finish?`, we may have performed a `cases #<anchor>` step that enabled
`ring` to propagate a new fact. If this fact is not used in the final
proof, and the corresponding `cases #<anchor>` step is pruned by NCB,
the `ring` step will fail during replay.
This PR ensures that `finish?` produces partial tactic scripts
containing `sorry`s.
We may add an option to disable this feature in the future.
It is enabled by default because it provides a useful way to debug
`grind` failures.
This PR topologically sorts abstracted vars in
`Meta.Closure.mkValueTypeClosure` if MVars are being abstracted.
Fixes#10705
---------
Co-authored-by: Eric Wieser <efw@google.com>
This PR fixes a regression introduced by the `ST` redefinition by making
the definition of `ST` as
reducible as previously. The key issue here is that in the previous
state it would reduce to a
function at which point the monad lifting mechanisms don't kick in in
the same fashion anymore.
This PR fixes another instance of the “default parameter value in
constructor” footgun, which was affecting the `cases` tactic in the
`grind` interactive mode.
This PR adds a warning to `wf_preproces` that these lemmas can be used
to introduce hidden partiality.
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR uses hashmaps for the symbol lookups in the IR interpreter
instead of the existing rbmaps.
Thus reducing the constant overhead per function call.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR fixes name mangling to be unambiguous / injective by adding `00`
for disambiguation where necessary. Additionally, the inverse function,
`Lean.Name.unmangle` has been added which can be used to unmangle a
mangled identifier. This unmangler has been added to demonstrate the
injectivity but also to allow unmangling identifiers e.g. for debugging
purposes.
Closes#10724
This PR adds support for `grind +premises`, calling the currently
configured premise selection algorithm and including the results as
parameters to `grind`. (Recall that there is not currently a default
premise selector provided by Lean4: you need a downstream premise
selector to make use of this.)
This PR adds a test for depending on two packages which privately import
modules that define the same Lean definition. It verifies the current
behavior of a symbol clash. This behavior will be fixed later this
quarter.
This PR adds a `+lax` configuration option for `grind`, causing it to
ignore parameters referring to non-existent theorems, or to theorems for
which we can't generate a pattern. This allows throwing large sets of
theorems (e.g. from a premise selection enginre) into `grind` to see
what happens.
This PR implements the `have <ident>? : <prop>` tactic for the `grind`
interactive mode. The proposition is proved using the default `grind`
search strategy. This tactic is also useful for inspecting or querying
the current `grind` state.
This PR implements parameter optimization for the generated
`instantiate` tactics produced by `finish?`.
We use a simple parameter optimizer that takes two sets as input: the
lower and upper bounds.
The lower bound consists of the theorems actually used in the proof
term, while the upper bound includes all the theorems instantiated in a
particular theorem instantiation step.
The lower bound is often sufficient to replay the proof, but in some
cases, additional theorems must be included because a theorem
instantiation may contribute to the proof by providing terms and many
not be present in the final proof term.
This PR makes minor changes to the MePo premise selection algorithm.
I'm increasingly believing that MePo will not work well in Lean; I've
tried a few things without success. Alistair Geesing's thesis from 2023
had similar conclusions.
My intention is to reach the point we can properly benchmark premise
selection algorithms before doing any more work here.
This PR optimizes two `String` proofs and makes sure that
`MkIffOfInductiveProp` does not import `Lean.Elab.Tactic`, which
previously pushed it to the very end of the import graph.
This PR splits some low-hanging fruit out of `Init.Data.String.Basic`:
basic material about `String.Pos.Raw`, `String.Substrig`, and
`String.Iterator`.
More splitting required and the remaining material is quite unorganized,
but it's a start.
This PR implements zero cost `BaseIO` by erasing the `IO.RealWorld`
parameter from argument lists and structures. This is a **major breaking
change for FFI**.
Concretely:
- `BaseIO` is defined in terms of `ST IO.RealWorld`
- `EIO` (and thus `IO`) is defined in terms of `EST IO.RealWorld`
- The opaque `Void` type is introduced and the trivial structure
optimization updated to account for it. Furthermore, arguments of type
`Void s` are removed from the argument lists of the C functions.
- `ST` is redefined as `Void s -> ST.Out s a` where `ST.Out` is a pair
of `Void s` and `a`
This together has the following major effects on our generated code:
- Functions that return `BaseIO`/`ST`/`EIO`/`IO`/`EST` now do not take
the dummy world parameter anymore. To account for this FFI code needs to
delete the dummy world parameter from the argument lists.
- Functions that return `BaseIO`/`ST` now return their wrapped value
directly. In particular `BaseIO UInt32` now returns a `uint32_t` instead
of a `lean_object*`. To account for this FFI code might have to change
the return type and does not need to call `lean_io_result_mk_ok` anymore
but can instead just `return` values right away (same with extracting
values from `BaseIO` computations.
- Functions that return `EIO`/`IO`/`EST` now only return the equivalent
of an `Except` node which reduces the allocation size. The
`lean_io_result_mk_ok`/`lean_io_result_mk_error` functions were updated
to account for this already so no change is required.
Besides improving performance by dropping allocation (sizes) we can now
also do fun new things such as:
```lean
@[extern "malloc"]
opaque malloc (size : USize) : BaseIO USize
```
This PR renames the cast functions on `String.ValidPos` for `set` and
`modify` to adhere to the established naming convention.
It also fixes two typos and very slighly tweaks the import graph,
shortening the critical path by a negligible amount.
This PR fixes a bug with Lake's cache where revisions were stored at the
incorrect path. Revisions were stored at `<rev>/<pkg>.jsonl` rather than
the correct `<pkg>/<rev>.jsonl`.
This PR fixes a proof instability source in `grind`.
We say a proof is *unstable* if minor changes in the `.lean` file
containing the proof **affect** it.
This PR adds a missing move assignment operator, and deletes the copy
assignment operator.
C++ types should not implement move constructors without also
implementing move assignment. This also ensures that `m_fn` is correctly
emptied after a move, which is not guaranteed by the standard.
This change is also needed to allow `lean::optional` to be eventually
replaced by `std::optional`.
This PR improves the performance of `mvcgen` by an optimized
implementation for `try (mpure_intro; trivial)`. This tactic sequence is
used to eagerly discharge VCs and in the process instantiates schematic
variables.
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 fixes a bug in `String.Slice.takeWhile` which caused it to get
its bookkeeping wrong and panic. The new version only uses safe
operations on `String.Slice.Pos`.
This PR reduces the amount of symbols in our DLLs by cutting open a
linking cycle of the shape:
`Environment -> Compiler -> Meta -> Environment`
This is achieved by introducing a dynamic call to the compiler hidden
behind a `Ref` as previously
done in the pretty printer.
This PR adds a field `isDisplayableTerm` to `TermInfo` and all utility
functions which create `TermInfo` that can be set to force the language
server to render the term in hover popups.
This PR fixes `input_dir` tracking to also recurse through
subdirectories. The `filter` of an `input_dir` will be applied to each
file in the directory tree (the path names of directories will not be
checked).
Closes#10827.
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 lets match compilation use exfalso as soon as no alternatives
are left. This way, the compiler does not have to look at subsequent
case splits.
This PR shows that the iterators returned by `String.Slice.split` and
`String.Slice.splitInclusive` are finite as long as the forward matcher
iterator for the pattern is finite (which we already know for all of our
patterns).
At actually also completely redefines the iterators to avoid the inner
loop in `Internal.nextMatch` which generates inefficient code. Instead,
when encountering a mismach from the matcher, we `skip` the split
iterator.
This PR improves the `grind` tactic generated by the `instantiate`
action in tracing mode. It also updates the syntax for the `instantiate`
tactic, making it similar to `simp`. For example:
* `instantiate only [thm1, thm2]` instantiates only theorems `thm1` and
`thm2`.
* `instantiate [thm1, thm2]` instantiates theorems marked with the
`@[grind]` attribute **and** theorems `thm1` and `thm2`.
The action produces `instantiate only [...]` tactics. Example:
```lean
/--
info: Try this:
[apply] ⏎
instantiate only [= Array.getElem_set]
instantiate only [= Array.getElem_set]
-/
#guard_msgs in
example (as bs cs : Array α) (v₁ v₂ : α)
(i₁ i₂ j : Nat)
(h₁ : i₁ < as.size)
(h₂ : bs = as.set i₁ v₁)
(h₃ : i₂ < bs.size)
(h₄ : cs = bs.set i₂ v₂)
(h₅ : i₁ ≠ j ∧ i₂ ≠ j)
(h₆ : j < cs.size)
(h₇ : j < as.size) :
cs[j] = as[j] := by
grind => finish?
```
Recall that `finish?` replays generated tactics before suggesting them.
The `instantiate` action inspects the generated proof term to decide
which theorems to include as parameters in the `instantiate only [...]`
tactic. However, in some cases, a theorem contributes only by adding a
term to the state. In such cases, the generated tactic cannot be fully
replayed, and the action uses
`instantiate approx [<thms instantiated>]` to indicate which parts of
the tactic script are approximate. The `approx` is just a hint for
users.
This PR implements the `finish?` tactic for the `grind` interactive
mode. When it successfully closes the goal, it produces a code action
that allows the user to close the goal using explicit grind tactic
steps, i.e., without any search. It also makes explicit which solvers
have been used.
This is just the first version, we will add many "bells and whistles"
later. For example, `instantiate` steps will clearly show which theorems
have been instantiated.
Example:
```lean
/--
info: Try this:
[apply] ⏎
cases #b0f4
next => cases #50fc
next => cases #50fc <;> lia
-/
#guard_msgs in
example (p : Nat → Prop) (x y z w : Int) :
(x = 1 ∨ x = 2) →
(w = 1 ∨ w = 4) →
(y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
(z = 1 ∨ z = 0) → x + y ≤ 6 := by
grind => finish?
```
The anchors in the generated script are based on stable hash codes.
Moreover, users can hover over them to see the exact term used in the
case split. `grind?` will also be implemented using the new framework.
This PR implements support for `Action` in the `grind` solver extensions
(`SolverExtension`). It also provides the `Solvers.mkAction` function
that constructs an `Action` using all registered solvers. The generated
action is "fair," that is, a solver cannot prevent other solvers from
making progress.
This PR implements infrastructure for evaluating `grind` tactics in the
`GrindM` monad. We are going to use it to check whether auto-generated
tactics can effectively close the original goal.
This PR moves many operations involving `String.Pos.Raw` to a the
`String.Pos.Raw` namespace with the eventual aim of freeing up the
`String` namespace to contain operations using `String.ValidPos` (to be
renamed to `String.Pos`) instead.
This PR adds the `String.ValidPos.set` and `String.ValidPos.modify`
functions.
After this PR, `String.pos_lt_eq` is no longer a `simp` lemma. Add
`String.Pos.Raw.lt_iff` as a `simp` lemma if your proofs break.
This PR renames `String.split` to `String.splitToList`, because soon the
name `String.split` will be used by a new implementation which is
superior because it is polymorphic over the pattern kind and it returns
an iterator of slices instead of a list of strings.
This PR implements a compact notation for inspecting the `grind` state
in interactive mode. Within a `grind` tactic block, each tactic may
optionally have a suffix of the form `| filter?`.
Examples:
```lean
instantiate | gen > 0 -- Displays terms in the `grind` state after executing `instantiate` with generation greater than zero
```
```lean
instantiate | -- Displays the `grind` state after executing `instantiate`
```
Remark: If the user places the cursor one space before `|`, the state
*before* executing `instantiate` is displayed.
This PR removes the code that was silently displaying the `grind` state
after each tactic step, as it was too noisy.
It also updates the notation for the `first` combinator in the `grind`
tactic mode to avoid conflicts with the new syntax.
This PR changes match compilation to reject some pattern matches that
were previously accepted due to inaccessible patterns sometimes treated
like accessible ones. Fixes#10794.
This PR adds more selectors for TCP and Signals.
It also fixes a problem with `Selectors` that they cannot be closures
over a promise, otherwise it causes the waiter promise to never be
dropped.
This PR introduces the `backward.privateInPublic` option to aid in
porting projects to the module system by temporarily allowing access to
private declarations from the public scope, even across modules. A
warning will be generated by such accesses unless
`backward.privateInPublic.warn` is disabled.
This PR fixes `getHexNumSize` to consider underscores. Previously, only
the amount of bytes was counted, making it output 9 for `1234_abcd`
instead of the actual number of digits, which is 8.
the tested situation (kernel runs into deep recursion but elaborator is
happy) is not very stable and depends on, for example, stack size. This
test is not worth that hassle.
This PR adds adds union operation on `DHashMap`/`HashMap`/`HashSet` and
their raw variants and provides lemmas about union operations.
---------
Co-authored-by: Paul-Lez <paul.lezeau@gmail.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR adds `.vscode/settings.json` to our `.gitignore`, which allows
Lean 4 developers to set local workspace settings. We already use the
the workspace file for settings in core, so this shouldn't cause any
problems.
This PR fixes a bug in the unknown identifier code actions where the
identifiers wouldn't be correctly minimized in nested namespaces. It
also fixes a bug where identifiers would sometimes be minimized to
`[anonymous]`.
The first bug was introduced in #10619.
This PR adds a silent info message with the `grind` state in its
interactive mode. The message is shown only when there is exactly one
goal in the grind interactive mode. The condition is a workaround for
current limitations of our `InfoTree`.
This PR lets match compilation look only at the first remaining
alternative in `processLeaf`. At this point we have no further variables
we can split on, so if the first one isn’t applicable, match compilation
should fail.
This PR fixes a regression introduced by #10307, where hovering the name
of an inductive type or constructor in its own declaration didn't show
the docstring. In the process, a bug in docstring handling for
coinductive types was discovered and also fixed. Tests are added to
prevent the regression from repeating in the future.
This PR ensures that `grind` interactive mode is hygienic. It also adds
tactics for renaming inaccessible names: `rename_i h_1 ... h_n` and
`next h_1 ... h_n => ..`, and `expose_names` for automatically generated
tactic scripts. The PR also adds helper functions for implementing
case-split actions.
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.
This PR introduces a no-op version of `Shrink`, a type that should allow
shrinking small types into smaller universes given a proof that the type
is small enough, and uses it in the iterator library. Because this type
would require special compiler support, the current version is just a
wrapper around the inner type so that the wrapper is equivalent, but not
definitionally equivalent.
While `Shrink` is unable to shrink universes right now, but introducing
it now will allow us to generalize the universes in the iterator library
with fewer breaking changes as soon as an actual `Shrink` is possible.
This PR fixes a bug in combination with VS Code where Lean code that
looks like CSS color codes would display a color picker decoration.
VS Code displays this decoration by default for all languages, not just
CSS. Due to https://github.com/microsoft/vscode/issues/91533, this
setting cannot be disabled in the client on a per-language basis.
However, we can override the default behavior by providing a color
provider of our own. This PR implements an empty color provider to
override the VS Code one.
This PR adds support for interactivity to the combined "try this"
messages that were introduced in #9966. In doing so, it moves the link
to apply a suggestion to a separate `[apply]` button in front of the
suggestion. Hints with diffs remain unchanged, as they did not
previously support interacting with terms in the diff, either.
<img width="379" height="256" alt="Suggestion with interactive message"
src="https://github.com/user-attachments/assets/7838ebf6-0613-46e7-bc88-468a05acbf51"
/>
This PR restores the change in #8656, which removed `autoImplicit =
false` from the default lake template (per previous discussions linked
there). This was accidentally reverted in #8866.
This PR fixes a performance regression introduced in #10518. More
generally, it ensures both message log and info state are per-command,
which has been the case in practice ever since the asynchronous language
driver was introduced.
This PR fixes a bug where partially up-to-date files built with `--old`
could be stored in the cache as fully up-to-date. Such files are no
longer cached. In addition, builds without traces now only perform an
modification time check with `--old`. Otherwise, they are considered
out-of-date.
This PR changes the Lake's remote cache interface to scope cache outputs
by toolchain and/or platform were useful.
Packages that set `platformIndependent = true` will not be scoped by
platform and the core build (i.e., `bootstrap = true`) will not be
scoped by toolchain. Lake's detected platform and toolchain can be
overridden with the new `--platform` and `--toolchain` options to `cache
get` and `cache put`.
Lake no longer accepts the `--scope` option when using `cache get` with
Reservoir.. The `--repo` option must be used instead.
This PR follows upon #10606 and creates equational theorems uniformly
from the unfold theorem, there is only one handler registered in
`registerGetEqnsFn`.
For now we keep `registerGetEqnsFn`, because it’s used by mathlib’s
`irreducible_def`, but I’d like to get rid of it in the long term,
relying only on `registerGetUnfoldEqnFn` for constructions that should
unfold differently.
This PR improves the tactics `ac`, `linarith`, `lia`, `ring` tactics in
`grind` interactive mode. They now fail if no progress has been made.
They also generate an info message with counterexample/basis if the goal
was not closed.
This PR provides range support for the signed finite number types
`Int{8,16,32,64}` and `ISize`. The proof obligations are handled by
reducing all of them to proofs about an internal `UpwardEnumerable`
instance for `BitVec` interpreted as signed numbers.
This PR changes where errors are displayed when trying to use
`coinductive` keyword when targeting things that do not live in `Prop`.
Instead of displaying the error above the first element of the mutual
block, it is displayed above the erroneous definition.
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR removes support for reducible well-founded recursion, a Breaking
Change. Using `@[semireducible]` on a definition by well-founded
recursion prints a warning that this is no longer effective.
With the upcoming module system, proofs are often not available. With
this change, we remove a fringe use case hat may require proofs, and
that would not be supported under the module system anyways.
At least for now, direct use of `WellFounded.fix` is not affected.
This fixes: #5192
This PR re-enables semantic tokens for Verso docstrings, after a prior
change accidentally disabled them. It also adds a test to prevent this
from happening again.
In the process, it became clear that there was a bug. The highlighting
strategy led to overlapping but not identical tokens, but the code had
previously assumed that this couldn't happen at the delta-encoding step.
So this PR additionally replaces the removal of duplicate tokens with
priority-based handling of overlapping tokens.
---------
Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
This PR adds the following tactics to the `grind` interactive mode:
- `focus <grind_tac_seq>`
- `next => <grind_tac_seq>`
- `any_goals <grind_tac_seq>`
- `all_goals <grind_tac_seq>`
- `grind_tac <;> grind_tac`
- `cases <anchor>`
- `tactic => <tac_seq>`
Example:
```lean
def g (as : List Nat) :=
match as with
| [] => 1
| [_] => 2
| _::_::_ => 3
example : g bs = 1 → g as ≠ 0 := by
grind [g.eq_def] =>
instantiate
cases #ec88
next => instantiate
next => finish
tactic =>
rw [h_2] at h_1
simp [g] at h_1
```
This PR enforces rules around arithmetic of `String.Pos.Raw`.
Specifically, it adopts the following conventions:
- Byte indices ("ordinals") in strings should be represented using
`String.Pos.Raw`
- Amounts of bytes ("cardinals") in strings should be represented using
`Nat`.
For example, `String.Slice.utf8ByteSize` now returns `Nat` instead of
`String.Pos.Raw`, and there is a new function `String.Slice.rawEndPos`.
Finally, the `HAdd` and `HSub` instances for `String.Pos.Raw` are
reorganized. This is a **breaking change**.
The `HAdd/HSub String.Pos.Raw String.Pos.Raw String.Pos.Raw` instances
have been removed. For the use case of tracking positions relative to
some other position, we instead provide `offsetBy` and `unoffsetBy`
functions. For the use case of advancing/unadvancing a position by an
arbitrary number of bytes, we instead provide `increaseBy` and
`decreaseBy` functions. For
offsetting/unoffsetting/advancing/unadvancing a position `p` by the size
of a string `s` (resp. character `c`), use `s + p`/`p - s`/`p + s`/`p -
s` (resp. `c + p`/`p - c`/`p + c`/`p - c`).
This PR re-enables the "experimental" warning for `mvcgen` by changing
its default. The official release has been postponed to justify small
breaking changes in the semantic foundations in the near future.
This PR adds a new helper parser for implementing parsers that contain
hexadecimal numbers. We are going to use it to implement anchors in the
`grind` interactive mode.
2025-10-08 21:12:03 +00:00
4917 changed files with 134498 additions and 38493 deletions
To build Lean you should use `make -j -C build/release`.
To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
## New features
When asked to implement new features:
* begin by reviewing existing relevant code and tests
* write comprehensive tests first (expecting that these will initially fail)
* and then iterate on the implementation until the tests pass.
All new tests should go in `tests/lean/run/`. These tests don't have expected output; we just check there are no errors. You should use `#guard_msgs` to check for specific messages.
## Success Criteria
*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass.
## Build System Safety
**NEVER manually delete build directories** (build/, stage0/, stage1/, etc.) even when builds fail.
- ONLY use the project's documented build command: `make -j -C build/release`
- If a build is broken, ask the user before attempting any manual cleanup
## LSP and IDE Diagnostics
After rebuilding, LSP diagnostics may be stale until the user interacts with files. Trust command-line test results over IDE diagnostics.
## Update prompting when the user is frustrated
If the user expresses frustration with you, stop and ask them to help update this `.claude/CLAUDE.md` file with missing guidance.
## Creating pull requests
Follow the commit convention in `doc/dev/commit_convention.md`.
**Title format:**`<type>: <subject>` where type is one of: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf`.
Subject should use imperative present tense ("add" not "added"), no capitalization, no trailing period.
**Body format:** The first paragraph must start with "This PR". This paragraph is automatically incorporated into release notes. Use imperative present tense. Include motivation and contrast with previous behavior when relevant.
Example:
```
feat: add optional binder limit to `mkPatternFromTheorem`
This PR adds a `num?` parameter to `mkPatternFromTheorem` to control how many
leading quantifiers are stripped when creating a pattern.
```
## CI Log Retrieval
When CI jobs fail, investigate immediately - don't wait for other jobs to complete. Individual job logs are often available even while other jobs are still running. Try `gh run view <run-id> --log` or `gh run view <run-id> --log-failed`, or use `gh run view <run-id> --job=<job-id>` to target the specific failed job. Sleeping is fine when asked to monitor CI and no failures exist yet, but once any job fails, investigate that failure immediately.
For subsequent RCs (`-rc2`, etc.) and stable releases, just update the version number in the existing release notes file title.
See `doc/dev/release_checklist.md` section "Writing the release notes" for full details.
## Process
1. Run `script/release_checklist.py {version}` to check the current status
2. **CRITICAL: If preliminary lean4 checks fail, STOP immediately and alert the user**
- Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes file exists
- **IMPORTANT**: The release page is created AUTOMATICALLY by CI after pushing the tag - DO NOT create it manually
- **IMPORTANT**: For -rc1 releases, release notes must be created before proceeding
- Do NOT create any PRs or proceed with repository updates if these checks fail
3. Create a todo list tracking all repositories that need updates
4. **CRITICAL RULE: You can ONLY run `release_steps.py` for a repository if `release_checklist.py` explicitly says to do so**
- The checklist output will say "Run `script/release_steps.py {version} {repo_name}` to create it"
- If a repository shows "🟡 Dependencies not ready", you CANNOT create a PR for it yet
- You MUST rerun `release_checklist.py` before attempting to create PRs for any new repositories
5. For each repository that the checklist says needs updating:
- Run `script/release_steps.py {version} {repo_name}` to create the PR
- Mark it complete when the PR is created
6. After creating PRs, notify the user which PRs need review and merging
7. **MANDATORY: Rerun `release_checklist.py` to check current status**
- Do this after creating each batch of PRs
- Do this after the user reports PRs have been merged
- NEVER assume a repository is ready without checking the checklist output
8. As PRs are merged and tagged, dependent repositories will become ready
9. Continue the cycle: run checklist → create PRs for ready repos → wait for merges → repeat
10. Continue until all repositories are updated and the release is complete
## Important Notes
- **NEVER merge PRs autonomously** - always wait for the user to merge PRs themselves
- The `release_steps.py` script is idempotent - it's safe to rerun
- The `release_checklist.py` script is idempotent - it's safe to rerun
- Some repositories depend on others (e.g., mathlib4 depends on batteries, aesop, etc.)
- Wait for user to merge PRs before dependent repos can be updated
- Alert user if anything unusual or scary happens
- Use appropriate timeouts for long-running builds (verso can take 10+ minutes)
- ProofWidgets4 uses semantic versioning (v0.0.X) - it's okay to create and push the next sequential tag yourself when needed for a release
## PR Status Reporting
Every time you run `release_checklist.py`, you MUST:
1. Parse the output to identify ALL open PRs mentioned (lines with "✅ PR with title ... exists")
2. Provide a summary to the user listing ALL open PRs that need review
3. Group them by status:
- PRs for repositories that are blocked by dependencies (show these but note they're blocked)
- PRs for repositories that are ready to merge (highlight these)
4. Format the summary clearly with PR numbers and URLs
This summary should be provided EVERY time you run the checklist, not just after creating new PRs.
The user needs to see the complete picture of what's waiting for review.
## Nightly Infrastructure
The nightly build system uses branches and tags across two repositories:
- `leanprover/lean4` has **branches** `nightly` and `nightly-with-mathlib` tracking the latest nightly builds
- `leanprover/lean4-nightly` has **dated tags** like `nightly-2026-01-23`
When a nightly succeeds with mathlib, all three should point to the same commit. Don't confuse these: branches are in the main lean4 repo, dated tags are in lean4-nightly.
## Error Handling
**CRITICAL**: If something goes wrong or a command fails:
- **DO NOT** try to manually reproduce the failing steps yourself
- **DO NOT** try to fix things by running git commands or other manual operations
- Both scripts are idempotent and designed to handle partial completion gracefully
- If a script continues to fail after retrying, report the error to the user and wait for instructions
echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE=""
if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
else
echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
fi
else
echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now."
echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
fi
else
echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
@@ -72,6 +72,9 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
The github repository will automatically update stage0 on `master` once
`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
To trigger this, modify `stage0/src/stdlib_flags.h` (e.g., by adding or changing
a comment). When `update-stage0` runs, it will overwrite `stage0/src/stdlib_flags.h`
with the contents of `src/stdlib_flags.h`, bringing them back in sync.
NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.
NOTE: The current interface was designed for internal use in Lean and should be considered **unstable**.
It will be refined and extended in the future.
The Lean FFI documentation is now part of the [Lean language reference](https://lean-lang.org/doc/reference/latest/).
As Lean is written partially in Lean itself and partially in C++, it offers efficient interoperability between the two languages (or rather, between Lean and any language supporting C interfaces).
This support is however currently limited to transferring Lean data types; in particular, it is not possible yet to pass or return compound data structures such as C `struct`s by value from or to Lean.
There are two primary attributes for interoperating with other languages:
*`@[extern "sym"] constant leanSym : ...` binds a Lean declaration to the external symbol `sym`.
It can also be used with `def` to provide an internal definition, but ensuring consistency of both definitions is up to the user.
*`@[export sym] def leanSym : ...` exports `leanSym` under the unmangled symbol name `sym`.
For simple examples of how to call foreign code from Lean and vice versa, see <https://github.com/leanprover/lean4/blob/master/src/lake/examples/ffi> and <https://github.com/leanprover/lean4/blob/master/src/lake/examples/reverse-ffi>, respectively.
## The Lean ABI
The Lean Application Binary Interface (ABI) describes how the signature of a Lean declaration is encoded as a native calling convention.
It is based on the standard C ABI and calling convention of the target platform.
For a Lean declaration marked with either `@[extern "sym"]` or `@[export sym]` for some symbol name `sym`, let `α₁ → ... → αₙ → β` be the normalized declaration's type.
If `n` is 0, the corresponding C declaration is
```c
externssym;
```
where `s` is the C translation of `β` as specified in the next section.
In the case of an `@[extern]` definition, the symbol's value is guaranteed to be initialized only after calling the Lean module's initializer or that of an importing module; see [Initialization](#initialization).
If `n` is greater than 0, the corresponding C declaration is
```c
ssym(t₁,...,tₘ);
```
where the parameter types `tᵢ` are the C translation of the `αᵢ` as in the next section.
In the case of `@[extern]` all *irrelevant* types are removed first; see next section.
### Translating Types from Lean to C
* The integer types `UInt8`, ..., `UInt64`, `USize` are represented by the C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively
*`Char` is represented by `uint32_t`
*`Float` is represented by `double`
* An *enum* inductive type of at least 2 and at most 2^32 constructors, each of which with no parameters, is represented by the first type of `uint8_t`, `uint16_t`, `uint32_t` that is sufficient to represent all constructor indices.
For example, the type `Bool` is represented as `uint8_t` with values `0` for `false` and `1` for `true`.
*`Decidable α` is represented the same way as `Bool`
* An inductive type with a *trivial structure*, that is,
* it is none of the types described above
* it is not marked `unsafe`
* it has a single constructor with a single parameter of *relevant* type
is represented by the representation of that parameter's type.
For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`.
Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
* `Nat` and `Int` are represented by `lean_object *`.
Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
* Any other type is represented by `lean_object *`.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
Example: the runtime value of `u : Unit` is always `lean_box(0)`.
#### Inductive types
For inductive types which are in the fallback `lean_object *` case above and not trivial constructors, the type is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true. A `lean_ctor_object` stores the constructor index in the header, and the fields are stored in the `m_objs` portion of the object.
The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:
* Non-scalar fields stored as `lean_object *`
* Fields of type `USize`
* Other scalar fields, in decreasing order by size
Within each group the fields are ordered in declaration order. Trivial wrapper types count as their underlying wrapped type for this purpose.
* To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
* To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
* To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds.
For example, a structure such as
```lean
structure S where
ptr_1 : Array Nat
usize_1 : USize
sc64_1 : UInt64
sc64_2 : { x : UInt64 // x > 0 } -- wrappers of scalars count as scalars
sc64_3 : Float -- `Float` is 64 bit
sc8_1 : Bool
sc16_1 : UInt16
sc8_2 : UInt8
sc64_4 : UInt64
usize_2 : USize
sc32_1 : Char -- trivial wrapper around `UInt32`
sc32_2 : UInt32
sc16_2 : UInt16
```
would get re-sorted into the following memory order:
By default, all `lean_object *` parameters of an `@[extern]` function are considered *owned*, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via `lean_dec`.
To reduce reference counting overhead, parameters can be marked as *borrowed* by prefixing their type with `@&`.
Borrowed objects must only be passed to other non-consuming functions (arbitrarily often) or converted to owned values using `lean_inc`.
In `lean.h`, the `lean_object *` aliases `lean_obj_arg` and `b_lean_obj_arg` are used to mark this difference on the C side.
Return values and `@[export]` parameters are always owned at the moment.
## Initialization
When including Lean code as part of a larger program, modules must be *initialized* before accessing any of their declarations.
Module initialization entails
* initialization of all "constants" (nullary functions), including closed terms lifted out of other functions
* execution of all `[init]` functions
* execution of all `[builtin_init]` functions, if the `builtin` parameter of the module initializer has been set
The module initializer is automatically run with the `builtin` flag for executables compiled from Lean code and for "plugins" loaded with `lean --plugin`.
For all other modules imported by `lean`, the initializer is run without `builtin`.
Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtin_init]` functions are only run for native executable or plugins, regardless of whether their module is imported or not.
`lean` uses built-in initializers for e.g. registering basic parsers that should be available even without importing their module (which is necessary for bootstrapping).
The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
**Important for process-related functionality**: If your application needs to use process-related functions from libuv, such as `Std.Internal.IO.Process.getProcessTitle` and `Std.Internal.IO.Process.setProcessTitle`, you must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) **before** calling `lean_initialize()` or `lean_initialize_runtime_module()`. This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.
Together with initialization of the Lean runtime, you should execute code like the following exactly once before accessing any Lean declarations:
argv = lean_setup_args(argc, argv); // if using process-related functionality
lean_initialize_runtime_module();
//lean_initialize(); // necessary (and replaces `lean_initialize_runtime_module`) if you (indirectly) access the `Lean` package
lean_object * res;
// use same default as for Lean executables
uint8_t builtin = 1;
res = initialize_A_B(builtin, lean_io_mk_world());
if (lean_io_result_is_ok(res)) {
lean_dec_ref(res);
} else {
lean_io_result_show_error(res);
lean_dec(res);
return ...; // do not access Lean declarations if initialization failed
}
res = initialize_C(builtin, lean_io_mk_world());
if (lean_io_result_is_ok(res)) {
...
//lean_init_task_manager(); // necessary if you (indirectly) use `Task`
lean_io_mark_end_initialization();
```
In addition, any other thread not spawned by the Lean runtime itself must be initialized for Lean use by calling
```c
void lean_initialize_thread();
```
and should be finalized in order to free all thread-local resources by calling
```c
void lean_finalize_thread();
```
## `@[extern]` in the Interpreter
The interpreter can run Lean declarations for which symbols are available in loaded shared libraries, which includes `@[extern]` declarations.
Thus to e.g. run `#eval` on such a declaration, you need to
1. compile (at least) the module containing the declaration and its dependencies into a shared library, and then
1. pass this library to `lean --load-dynlib=` to run code `import`ing this module.
Note that it is not sufficient to load the foreign library containing the external symbol because the interpreter depends on code that is emitted for each `@[extern]` declaration.
Thus it is not possible to interpret an `@[extern]` declaration in the same file.
See [`tests/compiler/foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) for an example.
.text"The Lean standard library contains a fully-featured string library, centered around the types `String` and `String.Slice`.",
.text"`String` is defined as the subtype of `ByteArray` of valid UTF-8 strings. A `String.Slice` is a `String` together with a start and end position.",
.text"`String` is equivalent to `List Char`, but it has a more efficient runtime representation. While the logical model based on `ByteArray` is overwritten in the runtime, the runtime implementation is very similar to the logical model, with the main difference being that the length of a string in Unicode code points is cached in the runtime implementation.",
.text"We are considering removing this feature in the future (i.e., deprecating `String.length`), as the number of UTF-8 codepoints in a string is not particularly useful, and if needed it can be computed in linear time using `s.positions.count`."
.text"The Lean standard library contains a number of functions that take one or more strings and slices and return a string or a slice.",
.text"If possible, these functions should avoid allocating a new string, and return a slice of their input(s) instead.",
.text"Usually, for every operation `f`, there will be functions `String.f` and `String.Slice.f`, where `String.f s` is defined as `String.Slice.f s.toSlice`.",
.text"In particular, functions that transform strings and slices should live in the `String` and `String.Slice` namespaces even if they involve a `String.Pos`/`String.Slice.Pos` (like `String.sliceTo`), for reasons that will become clear shortly.",
.h3"Transforming positions",
.text"Since positions on strings and slices are dependent on the string or slice, whenever users transform a string/slice, they will be interested in interpreting positions on the original string/slice as positions on the result, or vice versa.",
.text"Consequently, every operation that transforms a string or slice should come with a corresponding set of transformations between positions, usually in both directions, possibly with one of the directions being conditional.",
.text"For example, given a string `s` and a position `p` on `s`, we have the slice `s.sliceFrom p`, which is the slice from `p` to the end of `s`. A position on `s.sliceFrom p` can always be interpreted as a position on `s`. This is the \"backwards\" transformation. Conversely, a position `q` on `s` can be interpreted as a position on `s.sliceFrom p` as long as `p ≤ q`. This is the conditional forwards direction.",
.text"The convention for naming these transformations is that the forwards transformation should have the same name as the transformation on strings/slices, but it should be located in the `String.Pos` or `String.Slice.Pos` namespace, depending on the type of the starting position (so that dot notation is possible for the forward direction). The backwards transformation should have the same name as the operation on strings/slices, but with an `of` prefix, and live in the same namespace as the forwards transformation (so in general dot notation will not be available).",
.text"So, in the `sliceFrom` example, the forward direction would be called `String.Pos.sliceFrom`, while the backwards direction should be called `String.Pos.ofSliceFrom` (not `String.Slice.Pos.ofSliceFrom`).",
.text"If one of the directions is conditional, it should have a corresponding panicking operation that does not require a proof; in our example this would be `String.Pos.sliceFrom!`.",
.text"Sometimes there is a name clash for the panicking operations if the operation on strings is already panicking. For example, there are both `String.slice` and `String.slice!`. If the original operation is already panicking, we only provide panicking transformation operations. But now `String.Pos.slice!` could refer both to the panicking forwards transformation associated with `String.slice`, and also to the (only) forwards transformation associated with `String.slice!`. In this situation, we use an `orPanic` suffix to disambiguate. So the panicking forwards operation associated with `String.slice` is called `String.Pos.sliceOrPanic`, and the forwards operation associated with `String.slice!` is called `String.Pos.slice!`."
This release introduces the Lean module system, which allows files to
control the visibility of their contents for other files. In previous
releases, this feature was available as a preview when the option
`experimental.module` was set to `true`; it is now a fully supported
feature of Lean.
# Benefits
Because modules reduce the amount of information exposed to other
code, they speed up rebuilds because irrelevant changes can be
ignored, they make it possible to be deliberate about API evolution by
hiding details that may change from clients, they help proofs be
checked faster by avoiding accidentally unfolding definitions, and
they lead to smaller executable files through improved dead code
elimination.
# Visibility
A source file is a module if it begins with the `module` keyword. By
default, declarations in a module are private; the `public` modifier
exports them. Proofs of theorems and bodies of definitions are private
by default even when their signatures are public; the bodies of
definitions can be made public by adding the `@[expose]`
attribute. Theorems and opaque constants never expose their bodies.
`public section` and `@[expose] section` change the default visibility
of declarations in the section.
# Imports
Modules may only import other modules. By default, `import` adds the
public information of the imported module to the private scope of the
current module. Adding the `public` modifier to an import places the
imported modules's public information in the public scope of the
current module, exposing it in turn to the current module's clients.
Within a package, `import all` can be used to import another module's
private scope into the current module; this can be used to separate
lemmas or tests from definition modules without exposing details to
downstream clients.
# Meta Code
Code used in metaprograms must be marked `meta`. This ensures that the
code is compiled and available for execution when it is needed during
elaboration. Meta code may only reference other meta code. A whole
module can be made available in the meta phase using `meta import`;
this allows code to be shared across phases by importing the module in
each phase. Code that is reachable from public metaprograms must be
imported via `public meta import`, while local metaprograms can use
plain `meta import` for their dependencies.
The module system is described in detail in [the Lean language reference](https://lean-reference-manual-review.netlify.app/find/?domain=Verso.Genre.Manual.section&name=files).
parser=argparse.ArgumentParser(description="Check release status of Lean4 repositories")
parser.add_argument("toolchain",help="The toolchain version to check (e.g., v4.6.0)")
@@ -404,30 +696,78 @@ def main():
print(f" ❌ Short commit hash {commit_hash[:SHORT_HASH_LENGTH]} is numeric and starts with 0, causing issues for version parsing. Try regenerating the last commit to get a new hash.")
set(LEAN_EXTRA_LINKER_FLAGS${LEAN_EXTRA_LINKER_FLAGS_DEFAULT}CACHESTRING"Additional flags used by the linker")
set(LEAN_EXTRA_CXX_FLAGS""CACHESTRING"Additional flags used by the C++ compiler")
set(LEAN_EXTRA_CXX_FLAGS""CACHESTRING"Additional flags used by the C++ compiler. Unlike `CMAKE_CXX_FLAGS`, these will not be used to build e.g. cadical.")
set(LEAN_TEST_VARS"LEAN_CC=${CMAKE_C_COMPILER}"CACHESTRING"Additional environment variables used when running tests")
@@ -281,7 +280,7 @@ Checks whether any of the elements in a subarray satisfy a Boolean predicate.
The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that satisfies the predicate is found.
-/
@[inline]
@[inline,suggest_forSubarray.some]
defany{α:Typeu}(p:α→Bool)(as:Subarrayα):Bool:=
Id.run<|as.anyM(pure<|p·)
@@ -291,7 +290,7 @@ Checks whether all of the elements in a subarray satisfy a Boolean predicate.
The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that does not satisfy the predicate is found.
-/
@[inline]
@[inline,suggest_forSubarray.every]
defall{α:Typeu}(p:α→Bool)(as:Subarrayα):Bool:=
Id.run<|as.allM(pure<|p·)
Some files were not shown because too many files have changed in this diff
Show More
Reference in New Issue
Block a user
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.