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 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 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 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.
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 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 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 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 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 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 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.
