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>
