This PR fixes an `Elab.async` regression where elaboration tasks are
cancelled on document edit even though their result may be reused in the
new document version, reporting an incomplete result.
While this PR fixes the functional regression, it does so as an
over-approximation by never cancelling such tasks. A follow-up PR will
implement the correct behavior of only cancelling the tasks that are not
reused.
This PR moves away from using `List.get` / `List.get?` / `List.get!` and
`Array.get!`, in favour of using the `GetElem` mediated getters. In
particular it deprecates `List.get?`, `List.get!` and `Array.get?`. Also
adds `Array.back`, taking a proof, matching `List.getLast`.
This PR enables the language server to present multiple disjoint line
ranges as being worked on. Even before parallelism lands, we make use of
this feature to show post-elaboration tasks such as kernel checking on
the first line of a declaration to distinguish them from the final
tactic step.
This PR adds preliminary support for inlay hints, as well as support for
inlay hints that denote the auto-implicits of a function. Hovering over
an auto-implicit displays its type and double-clicking the auto-implicit
inserts it into the text document.
This PR is an extension of #3910.
### Known issues
- In VS Code, when inserting an inlay hint, the inlay hint may linger
for a couple of seconds before it disappears. This is a defect of the VS
Code implementation of inlay hints and cannot adequately be resolved by
us.
- When making a change to the document, it may take a couple of seconds
until the inlay hints respond to the change. This is deliberate and
intended to reduce the amount of inlay hint flickering while typing. VS
Code has a mechanism of its own for this, but in my experience it is
still far too sensitive without additional latency.
- Inserting an auto-implicit inlay hint that depends on an auto-implicit
meta-variable causes a "failed to infer binder type" error. We can't
display these meta-variables in the inlay hint because they don't have a
user-displayable name, so it is not clear how to resolve this problem.
- Inlay hints are currently always resolved eagerly, i.e. we do not
support the `textDocument/inlayHint/resolve` request yet. Implementing
support for this request is future work.
### Other changes
- Axioms did not support auto-implicits due to an oversight in the
implementation. This PR ensures they do.
- In order to reduce the amount of inlay hint flickering when making a
change to the document, the language server serves old inlay hints for
parts of the file that have not been processed yet. This requires LSP
request handler state (that sometimes must be invalidated on
`textDocument/didChange`), so this PR introduces the notion of a
stateful LSP request handler.
- The partial response mechanism that we use for semantic tokens, where
we simulate incremental LSP responses by periodically emitting refresh
requests to the client, is generalized to accommodate both inlay hints
and semantic tokens. Additionally, it is made more robust to ensure that
we never emit refresh requests while a corresponding request is in
flight, which causes VS Code to discard the respond of the request, as
well as to ensure that we keep prompting VS Code to send another request
if it spuriously decides not to respond to one of our refresh requests.
- The synthetic identifier of an `example` had the full declaration as
its (non-canonical synthetic) range. Since we need a reasonable position
for the identifier to insert an inlay hint for the auto-implicits of an
`example`, we change the (canonical synthetic) range of the synthetic
identifier to that of the `example` keyword.
- The semantic highlighting request handling is moved to a separate
file.
### Breaking changes
- The semantic highlighting request handler is not a pure request
handler anymore, but a stateful one. Notably, this means that clients
that extend the semantic highlighting of the Lean language server with
the `chainLspRequestHandler` function must now use the
`chainStatefulLspRequestHandler` function instead.
This PR makes the signatures of `find` functions across
`List`/`Array`/`Vector` consistent. Verification lemmas will follow in
subsequent PRs.
We were previously quite inconsistent about the signature of
`indexOf`/`findIdx` functions across `List` and `Array`. Moreover, there
are still quite large gaps in the verification lemma coverage for these
even at the `List` level.
My intention is to make the signatures consistent by providing:
`findIdx` / `findIdx?` / `findFinIdx?` (these all take a predicate, and
return respectively a `Nat`, `Option Nat`, `Option (Fin l.length)`) and
similarly `idxOf` / `idxOf?` / `finIdxOf?` (which look for an element)
for each of List/Array/Vector. I've seen enough examples by now where
each variant is genuinely the most convenient at the call-site, so I'm
going to accept the cost of having many closely related functions.
*Hopefully* for the verification lemmas we can simp all of these into
"projections" of the `Option (Fin l.length)` versions, and then only
have to specify that.
However, I will not plan on immediately either filling in the missing
verification lemmas (or even deciding what the simp normal forms
relating these operations are), and just reach parity amongst
List/Array/Vector for what is already there.
This PR implements support for offset constraints in the `grind` tactic.
Several features are still missing, such as constraint propagation and
support for offset equalities, but `grind` can already solve examples
like the following:
```lean
example (a b c : Nat) : a ≤ b → b + 2 ≤ c → a + 1 ≤ c := by
grind
example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by
grind
example (a b c : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 2 ≤ c := by
grind
example (a b c : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 1 ≤ c := by
grind
example (a b c : Nat) : a + 1 ≤ b → b ≤ c + 2 → a ≤ c + 1 := by
grind
example (a b c : Nat) : a + 2 ≤ b → b ≤ c + 2 → a ≤ c := by
grind
```
---------
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
This PR splits a definition out of `Lean.Lsp.Basic`, with the effect
that material about JSON is not needed for `Lean.Meta.Sorry` and its
dependencies.
This PR ensures that the configuration in `Simp.Config` is used when
reducing terms and checking definitional equality in `simp`.
closes#5455
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR makes it harder to create "fake" theorems about definitions that
are stubbed-out with `sorry` by ensuring that each `sorry` is not
definitionally equal to any other. For example, this now fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails
```
However, this still succeeds, since the `sorry` is a single
indeterminate `Nat`:
```lean
def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds
```
One can be more careful by putting parameters to the right of the colon:
```lean
def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails
```
Most sources of synthetic sorries (recall: a sorry that originates from
the elaborator) are now unique, except for elaboration errors, since
making these unique tends to cause a confusing cascade of errors. In
general, however, such sorries are labeled. This enables "go to
definition" on `sorry` in the Infoview, which brings you to its origin.
The option `set_option pp.sorrySource true` causes the pretty printer to
show source position information on sorries.
**Details:**
* Adds `Lean.Meta.mkLabeledSorry`, which creates a sorry that is labeled
with its source position. For example, `(sorry : Nat)` might elaborate
to
```
sorryAx (Lean.Name → Nat) false
`lean.foo.12.8.12.13.8.13._sorry._@.lean.foo._hyg.153
```
It can either be made unique (like the above) or merely labeled. Labeled
sorries use an encoding that does not impact defeq:
```
sorryAx (Unit → Nat) false (Function.const Lean.Name ()
`lean.foo.14.7.13.7.13.69._sorry._@.lean.foo._hyg.174)
```
* Makes the `sorry` term, the `sorry` tactic, and every elaboration
failure create labeled sorries. Most are unique sorries, but some
elaboration errors are labeled sorries.
* Renames `OmissionInfo` to `DelabTermInfo` and adds configuration
options to control LSP interactions. One field is a source position to
use for "go to definition". This is used to implement "go to definition"
on labeled sorries.
* Makes hovering over a labeled `sorry` show something friendlier than
that full `sorryAx` expression. Instead, the first hover shows the
simplified ``sorry `«lean.foo:48:11»``. Hovering over that hover shows
the full `sorryAx`. Setting `set_option pp.sorrySource true` makes
`sorry` always start with printing with this source position
information.
* Removes `Lean.Meta.mkSyntheticSorry` in favor of `Lean.Meta.mkSorry`
and `Lean.Meta.mkLabeledSorry`.
* Changes `sorryAx` so that the `synthetic` argument is no longer
optional.
* Gives `addPPExplicitToExposeDiff` awareness of labeled sorries. It can
set `pp.sorrySource` when source positions differ.
* Modifies the delaborator framework so that delaborators can set Info
themselves without it being overwritten.
Incidentally closes#4972.
Inspired by [this Zulip
thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Is.20a.20.60definition_wanted.60.20keyword.20possible.3F/near/477260277).
This PR removes unnecessary parameters from the funcion induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.
Part 2, adjusting after stage0 update.
Closes#6320
This PR modifies the signature of the functions `Nat.fold`,
`Nat.foldRev`, `Nat.any`, `Nat.all`, so that the function is passed the
upper bound. This allows us to change runtime array bounds checks to
compile time checks in many places.
This PR replaces `Array.feraseIdx` and `Array.insertAt` with
`Array.eraseIdx` and `Array.insertIdx`, both of which take a `Nat`
argument and a tactic-provided proof that it is in bounds. We also have
`eraseIdxIfInBounds` and `insertIdxIfInBounds` which are noops if the
index is out of bounds. We also provide a `Fin` valued version of
`Array.findIdx?`. Together, these quite ergonomically improve the array
indexing safety at a number of places in the compiler/elaborator.
This PR introduces date and time functionality to the Lean 4 Std.
Breaking Changes:
- `Lean.Data.Rat` is now `Std.Internal.Rat` because it's used by the
DateTime library.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
This PR adds the Lean.RArray data structure.
This data structure is equivalent to `Fin n → α` or `Array α`, but
optimized for a fast kernel-reduction `get` operation.
It is not suitable as a general-purpose data structure. The primary
intended use case is the “denote” function of a typical proof by
reflection proof, where only the `get` operation is necessary, and where
using `List.get` unnecessarily slows down proofs with more than a
hand-full of atomic expressions.
There is no well-formedness invariant attached to this data structure,
to keep it concise; it's semantics is given through `RArray.get`. In
that way one can also view an `RArray` as a decision tree implementing
`Nat → α`.
In #6068 this data structure is used in `simp_arith`.
This PR changes the signature of `Array.get` to take a Nat and a proof,
rather than a `Fin`, for consistency with the rest of the (planned)
Array API. Note that because of bootstrapping issues we can't provide
`get_elem_tactic` as an autoparameter for the proof. As users will
mostly use the `xs[i]` notation provided by `GetElem`, this hopefully
isn't a problem.
We may restore `Fin` based versions, either here or downstream, as
needed, but they won't be the "main" functions.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This PR changes the signature of `Array.set` to take a `Nat`, and a
tactic-provided bound, rather than a `Fin`.
Corresponding changes (but without the auto-param) for `Array.get` will
arrive shortly, after which I'll go more pervasively through the Array
API.
Simplifies the definition of `MapDeclarationExtension` so that it only
contains a `NameMap` without an additional `List (Name × α)`. Uses the
`NameMap`'s natural ordering during export rather than sorting.
This fixes issues from inserting into a `MapDeclarationExtension`
multiple times with the same key. Inside a module it appears that each
insertion overwrites the data, since those queries access the `NameMap`.
But across modules, only the first insertion is accessible, since each
insertion was actually pushed to the front of a `List`.
Mathlib needs this for a documentation extension feature, and [they are
considering a PR with a
workaround](https://github.com/leanprover-community/mathlib4/pull/17043)
that digs into the `MapDeclarationExtension` data structures.
I'd previously added an instance from `ForIn'` to `ForIn`, but this then
caused some non-defeq duplication. It seems fine to just remove the
concrete `ForIn` instances in cases where the `ForIn'` instance exists
too. We can even remove a number of type-specific lemmas in favour of
the general ones.
I made a few choices so far that can probably be discussed:
- got rid of `modn` on `UInt`, nobody seems to use it apart from the
definition of `shift` which can use normal `mod`
- removed the previous defeq optimized definition of `USize.size` in
favor for a normal one. The motivation was to allow `OfNat` to work
which doesn't seem to be necessary anymore afaict.
- Minimized uses of `.val`, should we maybe mark it deprecated?
- Mostly got rid of `.val` in basically all theorems as the proper next
level of API would now be `.toBitVec`. We could probably re-prove them
but it would be more annoying given the change of definition.
- Did not yet redefine `log2` in terms of `BitVec` as this would require
a `log2` in `BitVec` as well, do we want this?
- I added a couple of theorems around the relation of `<` on `UInt` and
`Nat`. These were previously not needed because defeq was used all over
the place to save us. I did not yet generalize these to all types as I
wasn't sure if they are the appropriate lemma that we want to have.
This PR ensures that deprecated declarations are displayed with a
strikethrough markup in the completion popup of VS Code and that the
docstring of a completion item denotes the meta-data of the deprecation.
Resolve cases when the `To/FromJSON` type classes are used with `Empty`,
e.g. in the following motivating example.
```
import Lean
structure Foo (α : Type) where
y : Option α
deriving Lean.ToJson
#eval Lean.toJson (⟨none⟩ : Foo Empty) -- fails
```
This is a follow-up to this PR
https://github.com/leanprover/lean4/pull/5415, as suggested by
@eric-wieser. It expands on the original suggestion by also handling
`FromJSON`.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
From the new doc-string:
```quote
In early versions of Lean, the typeclasses provided by `/` and `%`
were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
However we decided it was better to use `ediv` and `emod`,
as they are consistent with the conventions used in SMTLib, Mathlib,
and often mathematical reasoning is easier with these conventions.
At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
In September 2024, we decided to do this rename (with deprecations in place),
and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
ever need to use these functions and their associated lemmas.
```
1. Remove the need to allocate an intermediate `String` for literally
every character in a JSON `String`.
2. Use a single `String` buffer in the entire `Json.compress` machinery.
3. Use `toListAppend`
Number 1 is doing most of the lifting in the perf diff, the rest are
some minor but measurable improvements.
This doesn't completely resolve the danger (only relevant in `prelude`
files) of importing `Init.Data.List.Basic` but not `Init.Data.List.Impl`
and thereby not having `@[csimp]` lemmas installed for some list
operations.
I'm going to address this better while working on `Array`.
This PR roughly halves the time needed to load the .ilean files by
optimizing the JSON parser and the conversion from JSON to Lean data
structures.
The code is optimized roughly as follows:
- String operations are inlined more aggressively
- Parsers are changed to use new `String.Iterator` functions `curr'` and
`next'` that receive a proof and hence do not need to perform an
additional check
- The `RefIdent` of .ilean files now uses a `String` instead of a `Name`
to avoid the expensive parse step from `String` to `Name` (despite the
fact that we only very rarely actually need a `Name` in downstream code)
- Instead of `List`s and `Subarray`s, the JSON to Lean conversion now
directly passes around arrays and array indices to avoid redundant
boxing
- Parsec's `peek?` sometimes generates redundant `Option` wrappers
because the generation of basic blocks interferes with the ctor-match
optimization, so it is changed to use an `isEof` check where possible
- Early returns and inline-do-blocks cause the code generator to
generate new functions, which then interfere with optimizations, so they
are now avoided
- Mutual defs are used instead of unspecialized passing of higher-order
functions to generate faster code
- The object parser is made tail-recursive
This PR also fixes a stack overflow in `Lean.Json.compress` that would
occur with long lists and adds a benchmark for the .ilean roundtrip
(compressed pretty-printing -> parsing).
I'm experimenting with changing the signature of `Ord.arrayOrd`; rather
than make a local synonym here, let's make a local instance so it
doesn't interact with the experiments.
This restores all of the imports of `Lean.Data.HashMap` and
`Lean.Data.HashSet` so that users actually see the deprecation warnings
instead of a "declaration not found" error.
For experimentation by @the-sofi-uwu.
I also have an efficient number parser in LeanSAT that I am planning to
upstream after we have sufficiently bikeshed this change.
