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