This PR adds two benchmarks (sieve of Eratosthenes, removing duplicates
from the list) and one test (a function with sublinear complexity
defined via well-founded recursion evaluated on large naturals with up
to `60` digits).
The tests have been suggested by @b-mehta.
This PR changes the semantics of `inline` annotations in the compiler.
The behavior of the original `@[inline]` attribute remains the same but
the function `inline` now comes with a restriction that it can only use
declarations that are local to the current module. This comes as a
preparation to pulling the compiler out into a separate process.
Closes: #12334
This PR changes the handling of over-applied cases expressions in
`ToLCNF` to avoid generating function declarations that are called
immediately. For example, `ToLCNF` previously produced this:
```lean-4
set_option trace.Compiler.init true
/--
trace: [Compiler.init] size: 4
def test x y : Bool :=
fun _y.1 _y.2 : Bool :=
cases x : Bool
| PUnit.unit =>
fun _f.3 a : Bool :=
return a;
let _x.4 := _f.3 _y.2;
return _x.4;
let _x.5 := _y.1 y;
return _x.5
-/
#guard_msgs in
def test (x : Unit) (y : Bool) : Bool :=
x.casesOn (fun a => a) y
```
which is now simplified to
```lean-4
set_option trace.Compiler.init true
/--
trace: [Compiler.init] size: 3
def test x y : Bool :=
cases x : Bool
| PUnit.unit =>
let a := y;
return a
-/
#guard_msgs in
def test (x : Unit) (y : Bool) : Bool :=
x.casesOn (fun a => a) y
```
This is especially relevant for #8309 because there `dite` is defined as
an over-applied `Bool.casesOn`.
This PR adds the option `doc.verso.module`. If set, it controls whether
module docstrings use Verso syntax. If not set, it defaults to the value
of the `doc.verso` option.
Closes#12070.
This PR fixes an issue on new NeoVim versions that would cause the
language server to display an error when using certain code actions.
(For some reason, NeoVim recently decided to diverge from VS Code in
terms of when it emits code action resolution requests, which means that
not setting the `data?` field won't preclude NeoVim from emitting a
request anymore, which in turn means that the server can't resolve the
code action.)
This PR implements preparatory work for #12179. It implements a new
feature in `isDefEq` to ensure it does not increase the transparency
level to `.default` when checking definitionally equality of implicit
arguments. This transparency level bump was introduced in Lean 3, but it
is not a performance issue and is affecting Mathlib. This PR adds the
new feature, but it is disabled by default.
This PR adds a default `Inhabited` instance to `Theorem` type.
The need to do so came up in #12296 , as `Theorem` is one of the entries
of the structure which is the key entry of `SimpleScopedEnvExtension`.
This PR fixes the PR release workflow which was failing due to the
deprecated `MATHLIB4_COMMENT_BOT` PAT being invalid.
**Error:** `jq: error (at <stdin>:4): Cannot index string with string
"name"` when fetching labels - the API returned an error response
instead of labels array because the PAT credentials were bad.
**Changes:**
- Generate a token from the `mathlib-lean-pr-testing` GitHub App (ID:
2785182) for posting comments to Lean PRs about mathlib compatibility
- Use `GITHUB_TOKEN` for read-only label fetching (no special identity
needed)
- Update the bot username check from `leanprover-community-bot` to
`mathlib-lean-pr-testing[bot]`
**Secrets added:** `MATHLIB_LEAN_PR_TESTING_APP_ID` and
`MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY` have been added to the repository.
Fixes the CI failure at
https://github.com/leanprover/lean4/actions/runs/21705647318/job/62595966115🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR adds `String.Slice.Subslice`, which is an unbundled version of
`String.Slice`.
This type is of interest because it is the correct type for string
searching and splitting operations to land in.
This PR just adds the type with minimal API. Additional API and
subsequent refactoring of the searching and splitting API is left for
future PRs.
This PR reverses the relationship between the `ForwardPattern` and
`ToForwardSearcher` classes.
Previously, it was possible to derive `ForwardPattern` (i.e.,
`dropPrefix?`) from `ToForwardSearcher` (i.e., get an iterator of
`SearchStep (s)`). Now, we give the default instance in the other
direction: it is now possible to derive `ToForwardSearcher` from
`ForwardPattern`. Since it is usually much easier to provide
`ForwardPattern` than `ToForwardSearcher`, this means more shared code,
which pays off double since we will give a correctness proof for the
default implementation in an upcoming PR.
This PR also adds some string lemmas.
This PR adds theorems that directly state that div and mod form an
injective pair: if `a / n = b / n` and `a % n = b % n` then `a = b`.
These complement existing div/mod lemmas and are useful for extension
arguments.
Upstreaming from
https://github.com/leanprover-community/mathlib4/pull/34201🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
This PR fixes the PR release workflow which is failing to create
`lean-pr-testing` branches due to the deprecated `MATHLIB4_BOT` PAT (see
https://github.com/leanprover/lean4/actions/runs/21698772126/job/62574742680).
The fix uses `actions/create-github-app-token@v2` to generate a token
from the `mathlib-nightly-testing` GitHub App (ID: 2784211) instead,
which has write access to both `leanprover-community/batteries` and
`leanprover-community/mathlib4-nightly-testing`.
Requires adding `MATHLIB_NIGHTLY_TESTING_APP_ID` and
`MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY` secrets to leanprover/lean4
(done).
🤖 Prepared with Claude Code
This PR ensures `simp` does not "simplify" instances by default. The old
behavior can be retrieved by using `simp +instances`. This PR is similar
to #12195, but for `dsimp`.
The backward compatibility flag for `dsimp` also deactivates this new
feature.
```
set_option backward.dsimp.instances true
```
Applying `simp` (and `dsimp`) to instances creates non-standard
instances, and this creates all sorts of problems in Mathlib.
---------
Co-authored-by: Henrik Böving <hargonix@gmail.com>
Co-authored-by: Sebastian Graf <sgraf1337@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR leverages the fact that expressions are type correct in `grind`
and the conclusion of extensionality theorems is of the form `?a = ?b`.
This PR is relevant for #12179 because it enables us to use a weaker
`isDefEq` that does not bump the transparency level when processing
implicit arguments.
This adds a `maxSuggestions : Option Nat := none` field to both
`Simp.Config` and `Grind.Config`. When `suggestions` is enabled, this
field controls the maximum number of library suggestions to use. If
`none`, the default limit is used.
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
This adds `set_option debug.byAsSorry true` and `decreasing_by sorry` to
various files to allow bootstrapping with Config structure changes. These
changes will be restored after the bootstrap dance is complete.
This PR adds and updates docstrings for syntax (and one for ranges).
The reference manual's section on syntax operators is gaining more
content, so the resulting docstrings were reviewed and the missing ones
added.
This PR adds an experimental `cbv` tactic that can be invoked from
`conv` mode. The tactic is not suitable for production use and an
appropriate warning is displayed.
This PR introduces the functions `(String|Slice).posGE` and
`(String|Slice).posGT` will full verification and deprecates
`Slice.findNextPos` in favor of `Slice.posGT`.
The KMP implementation is adapted to use these two new functions.
Various useful string and order lemmas are added along the way.
Also add a `simp` attribute to `Std.le_refl` and fix the resulting
fallout (yes, this would have been better as a separate PR).
