This PR implements a number of refinements for the auto-implicit inlay
hints implemented in #6768.
Specifically:
- In #6768, there was a bug where the inlay hint edit delay could
accumulate on successive edits, which meant that it could sometimes take
much longer for inlay hints to show up. This PR implements the basic
infrastructure for request cancellation and implements request
cancellation for semantic tokens and inlay hints to resolve the issue.
With this edit delay bug fixed, it made more sense to increase the edit
delay slightly from 2000ms to 3000ms.
- In #6768, we applied the edit delay to every single inlay hint request
in order to reduce the amount of inlay hint flickering. This meant that
the edit delay also had a significant effect on how far inlay hints
would lag behind the file progress bar. This PR adjusts the edit delay
logic so that it only affects requests sent directly after a
corresponding `didChange` notification. Once the edit delay is used up,
all further semantic token requests are responded to without delay, so
that the only latency that affects how far the inlay hints lag behind
the progress bar is how often we emit refresh requests and how long VS
Code takes to respond to them.
- For inlay hints, refresh requests are now emitted 500ms after a
response to an inlay hint request, not 2000ms, which means that after
the edit delay, inlay hints should only lag behind the progress bar by
about up to 500ms. This is justifiable for inlay hints because the
response should be much smaller than e.g. is the case for semantic
tokens.
- In #6768, 'Restart File' did not prompt a refresh, but it does now.
- VS Code does not immediately remove old inlay hints from the document
when they are applied. In #6768, this meant that inlay hints would
linger around for a bit once applied. To mitigate this issue, this PR
adjusts the inlay hint edit delay logic to identify edits sent from the
client as being inlay hint applications, and sets the edit delay to 0ms
for the inlay hint requests following it. This means that inlay hints
are now applied immediately.
- In #6768, hovering over single-letter auto-implicit inlay hints was a
bit finicky because VS Code uses the regular cursor icon on inlay hints,
not the thin text cursor icon, which means that it is easy to put the
cursor in the wrong spot. We now add the separation character (` ` or
`{`) preceding an auto-implicit to the hover range as well, which makes
hovering over inlay hints much smoother.
As per dicussion with team colleages, the feature shouldn’t be called
“auto attach” but rather “well-founded recursion preprocessing” to avoid
(imprecise) jargon.
This PR adds the `binderNameHint` gadget. It can be used in rewrite and
simp rules to preserve a user-provided name where possible.
The expression `binderNameHint v binder e` defined to be `e`.
If it is used on the right-hand side of an equation that is applied by a
tactic like `rw` or `simp`,
and `v` is a local variable, and `binder` is an expression that (after
beta-reduction) is a binder
(so `fun w => …` or `∀ w, …`), then it will rename `v` to the name used
in the binder, and remove
the `binderNameHint`.
A typical use of this gadget would be as follows; the gadget ensures
that after rewriting, the local
variable is still `name`, and not `x`:
```
theorem all_eq_not_any_not (l : List α) (p : α → Bool) :
l.all p = !l.any fun x => binderNameHint x p (!p x) := sorry
example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by
rw [all_eq_not_any_not]
-- ⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true
```
This gadget is supported by `simp`, `dsimp` and `rw` in the
right-hand-side of an equation, but not
in hypotheses or by other tactics.
This PR ensures `try?` can suggest tactics that need to reference
inaccessible local names.
Example:
```lean
/--
info: Try these:
• · expose_names; induction as, bs_1 using app.induct <;> grind [= app]
• · expose_names; induction as, bs_1 using app.induct <;> grind only [app]
-/
#guard_msgs (info) in
example : app (app as bs) cs = app as (app bs cs) := by
have bs := 20 -- shadows `bs` in the target
try?
```
This PR adds a convenience command `#info_trees in`, which prints the
info trees generated by the following command. It is useful for
debugging or learning about `InfoTree`.
This PR adds support for changing the binder annotations of existing
variables to and from strict-implicit and instance-implicit using the
`variable` command.
This PR requires a stage0 update to fully take effect.
Closes#6078
This PR starts on the process of cleaning up variable names across
List/Array/Vector. For now, we just rename "numerical index" variables
in one file. This is driven by a custom linter.
This PR adds error messages for `inductive` declarations with
conflicting constructor names and `mutual` declarations with conflicting
names.
Closes#6694.
This PR adds support for plugins to the frontend and server.
Implementation-wise, this adds a `plugins` argument to `runFrontend`,
`processHeader`, amd `importModules`, a `plugins` field to
`SetupImportsResult` and `FileSetupResult`. and a `pluginsPath` field to
`LeanPaths`, and then threads the value through these.
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 modifies `rewrite`/`rw` to abort rewriting if the elaborated
lemma has any immediate elaboration errors (detected by presence of
synthetic sorries). Rewriting still proceeds if there are elaboration
issues arising from pending synthetic metavariables, like instance
synthesis failures. The purpose of the change is to avoid obscure
"tactic 'rewrite' failed, equality or iff proof expected ?m.5" errors
when for example a lemma does not exist.
This helps error reporting for the natural number game.
https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Why.20doesn't.20add_left_comm.20work.20here.3F/near/497060022
This PR fixes the `#discr_tree_simp_key` command, because it displays
the keys for just `lhs` in `lhs ≠ rhs`, but it should be `lhs = rhs`,
since that is what simp indexes.
This PR changes the name generation of specialized LCNF decls so they
don't strip macro scopes. This avoids name collisions for
specializations created in distinct macro scopes. Since the normal
Name.append function checks for the presence of macro scopes, we need to
use appendCore.
This PR adds the tactic `expose_names`. It creates a new goal whose
local context has been "exposed" so that every local declaration has a
clear, accessible name. If no local declarations require renaming, the
original goal is returned unchanged.
This tactic will be used to improve `try?`.
This PR implements two rules for bv_decide's preprocessor, lowering
`|||` to `&&&` in order to enable more term sharing + application of
rules about `&&&` as well as rewrites of the form `(a &&& b == -1#w) =
(a == -1#w && b == -1#w)` in order to preserve rewriting behavior that
already existed before this lowering.
This PR enables code generation to proceed in parallel to further
elaboration.
It does not aim to make further refinements such as generating code for
different declarations in parallel or removing the dependency on kernel
checking.
previously we did not include the “old” IH in the local context, so that
creating a MVar would not pick it up. But this always felt like a hack,
and prevented us from inferring types. So lets's try keeping them in the
context and using `withErasedFVars` only when creating metavariables.
This PR adds a `recommended_spelling` command, which can be used for
recording the recommended spelling of a notation (for example, that the
recommended spelling of `∧` in identifiers is `and`). This information
is then appended to the relevant docstrings for easy lookup.
The function `Lean.Elab.Term.Doc.allRecommendedSpellings` may be used to
obtain a list of all recommended spellings, for example to create a
table that is part of a style guide. In the future, it might be
desirable to be able to partition such a table into smaller tables by
category. This can be added in a future PR.
The implementation is heavily inspired by #4490.
This PR changes how the unfold theorems for well-founded recursion are
created. They are created eagerly (anticipating that the behaivor may be
affected by simp sets soon), and without the detour of going through
equational theorems.
This PR adds a builtin tactic and a builtin attribute that are required
for the tree map. The tactic, `as_aux_lemma`, can generally be used to
wrap the proof term generated by a tactic sequence into a separate
auxiliary lemma in order to keep the proof term small. This can, in rare
cases, be necessary if the proof term will appear multiple times in the
encompassing term. The new attribute, `Std.Internal.tree_tac`, is
internal and should not be used outside of `Std`.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR changes how app unexpanders are invoked. Before the ref was
`.missing`, but now the ref is the head constant's delaborated syntax.
This way, when `pp.tagAppFns` is true, then tokens in app unexpanders
are annotated with the head constant. The consequence is that in docgen,
tokens will be linkified. This new behavior is consistent with how
`notation` defines app unexpanders.
In a followup PR we can slightly simplify the `notation` unexpander
macro to not set the ref.
This PR makes the pretty printer for `.coeFun`-tagged functions respect
`pp.tagAppFns`. The effect is that in docgen, when an expression pretty
prints as `f x y z` with `f` a coerced function, then if `f` is a
constant it will be linkified.
This PR modifies the delaborator so that in `pp.tagAppFns` mode,
generalized field notation is tagged with the head constant. The effect
is that docgen documentation will linkify dot notation. Internal change:
now formatted `rawIdent` can be tagged.
This PR adds the `try?` tactic. This is the first draft, but it can
already solve examples such as:
```lean
example (e : Expr) : e.simplify.eval σ = e.eval σ := by
try?
```
in `grind_constProp.lean`. In the example above, it suggests:
```lean
induction e using Expr.simplify.induct <;> grind?
```
In the same test file, we have
```lean
example (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
try?
```
and the following suggestion is produced
```lean
induction σ₁, σ₂ using State.join.induct <;> grind?
```
This PR adds the `grind` configuration option `verbose`. For example,
`grind -verbose` disables all diagnostics. We are going to use this flag
to implement `try?`.
This PR changes the `simpMatch` function, used inside the equation
generator for WF-rec functions, to not do eta-expansion.
This makes the process a bit more robust and disciplined, and avoids
removing match-statements (and introduce projections and dependencies)
that we'd rather split instead.
Also adds more tracing to the equational theorem generator.
Extracted from #6898.
This PR adds the new attributes `[grind =>]` and `[grind <=]` for
controlling pattern selection and minimizing the number of places where
we have to use verbose `grind_pattern` command. It also fixes a bug in
the new pattern selection procedure, and improves the automatic pattern
selection for local lemmas.
The tests `grind_constProp.lean` and `no_grind_constProp.lean` are the
same use case with and without `grind`.
This PR fixes a few `grind` issues exposed by the `grind_constProp.lean`
test.
- Support for equational theorem hypotheses created before invoking
`grind`. Example: applying an induction principle.s
- Support of `Unit`-like types.
- Missing recursion depth checks.
This PR fixes a bug in the pattern selection heuristic used in `grind`.
It was unfolding definitions/abstractions that were not supposed to be
unfolded. See `grind_constProp.lean` for examples affected by this bug.
This PR allows environment extensions to opt into access modes that do
not block on the entire environment up to this point as a necessary
prerequisite for parallel proof elaboration.
This PR adds Float32 to the LCNF builtinRuntimeTypes list. This was
missed during the initial Float32 implementation, but this omission has
the side effect of lowering Float32 to obj in the IR.
