Makes `MessageData.ofConstName` available without needing to import the
pretty printer. Any code making use of `MessageData` can write `m!" ...
{.ofConstName n} ... "` to have the name print with hover information.
More error messages now have hover information.
* Now `.ofConstName` also has a boolean flag to make names print fully
qualified. Default: false.
* Now `.ofConstName` will sanitize names that aren't constants. It is OK
to use it in `"unknown constant '{.ofConstName constName}'"` errors.
Usability note: it is more user-friendly to have "has already been
declared" errors report the fully qualified name. For this, write
`m!"{.ofConstName n true} has already been declared"`.
Gives more control over pretty printing metavariables.
- When `pp.mvars.levels` is false, then universe level metavariables
pretty print as `_` rather than `?u.22`
- When `pp.mvars.anonymous` is false, then anonymous metavariables
pretty print as `?_` rather than `?m.22`. Named metavariables still
pretty print with their names. When this is false, it also sets
`pp.mvars.levels` to false, since every level metavariable is anonymous.
- When `pp.mvars` is false, then all metavariables pretty print as `?_`
or `_`.
Modifies TryThis to use `pp.mvars.anonymous` rather than doing a
post-delaboration modification. This incidentally improves TryThis since
it now prints universe level metavariables as `_` rather than `?u.22`.
This PR enables the use of incrementality for completion in tactic
blocks. Consider the following example:
```lean
example : True := by
have : True := T
sleep 10000
```
Before this PR, in order to respond to a completion request after `T`,
`sleep 10000` has to complete first since the command must be fully
elaborated. After this PR, the completion request is responded to
immediately.
Updates the user widget manual to account for more recent changes. One
issue is that the samples no longer work on https://live.lean-lang.org/
because it uses an outdated version of the `@leanprover/infoview` NPM
package. They work on https://lean.math.hhu.de/ and in recent versions
of the VSCode extension.
After each tactic step, we save the info tree created by it together
with an appropriate info tree context that makes it stand-alone (which
we already did before to some degree, see `Info.updateContext?`). Then,
in the adjusted request handlers, we first search for a snapshot task
containing the required position, if so wait on it, and if it yielded an
info tree, use it to answer the request, or else continue searching and
waiting, falling back to the full info tree, which should be unchanged
by this PR.
The definition header does *not* report info trees early as in general
it is not stand-alone in the tactic sense but may contain e.g.
metavariables solved by the body in which case we do want to show the
ultimate state as before. This could be refined in the future in case
there are no unsolved mvars.
The adjusted request handlers are exactly the ones waited on together by
the info view, so they all have to be adjusted to have any effect on the
UX. Further request handlers may be adjusted in the future.
No new tests as "replies early" is not something we can test with our
current framework but the existing test suite did help in uncovering
functional regressions.
I noticed that a change to `Lean.PrettyPrinter.Delaborator.Builtins`
rebuilt more modules than I expected, so I moved a definition and
reduced some dependcies.
More reduction would be possible to move const-delaboration out of the
big `Lean.PrettyPrinter`, and import from `Lean.PrettyPrinter`
selectively.
Before, `pp.instantiateMVars` generally had no effect because most call
sites for the pretty printer instantiated metavariables first, but now
this functionality is entrusted upon the `pp.instantiateMVars` option.
This also has an effect in hovers, where metavariables can be unfolded
one assignment at a time. However, the goal state still sees all
metavariables instantiated due to the fact that the algorithm relies on
expression equality post-instantiation (see
`Lean.Widget.goalToInteractive`).
Closes#4406
Allows embedding user widgets in structured messages. Companion PR is
leanprover/vscode-lean4#449.
Some technical choices:
- The `MessageData.ofWidget` constructor might not be strictly necessary
as we already have `MessageData.ofFormatWithInfos`, and there is
`Info.ofUserWidget`. However, `.ofUserWidget` also requires a `Syntax`
object (as it is normally produced when widgets are saved at a piece of
syntax during elaboration) which we do not have in this case. More
generally, it continues to be a bit cursed that `Elab.Info` nodes are
used both for elaboration and delaboration (pretty-printing), so
entrenching that approach seems wrong. The better approach would be to
have a separate notion of pretty-printer annotation; but such a refactor
would not be clearly beneficial right now.
- To support non-JS-based environments such as
https://github.com/Julian/lean.nvim, `.ofWidget` requires also providing
another message which approximates the widget in a textual form.
However, in practice these environments might still want to support a
few specific user widgets such as "Try this".
---
Closes#2064.
luckily the necessary functionality already exists in the form of
`addPPExplicitToExposeDiff`. But it is not cheap, and we should not run
this code
when the error message isn’t shown, so we should do this lazily.
We already had `MessageData.ofPPFormat` to assemble the error message
lazily, but it
was restricted to returning `FormatWithInfo`, a data type that doesn’t
admit a nice
API to compose more complex messages (like `Format` or `MessageData`
has; an attempt to
fix that is in #3926).
Therefore we split the functionality of `.ofPPFormat` into
`.ofFormatWithInfo` and `.ofLazy`,
and use `.ofLazy` to compute the more complex error message of `apply`.
Fixes#3232.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Reusing the best profiling UI out there
Usage:
```
lean -Dtrace.profiler=true -Dtrace.profiler.output=profile.json foo.lean ...
```
then open `profile.json` in https://profiler.firefox.com/.
See also `script/collideProfiles.lean` for minimizing and merging
profiles.
* Setting `pp.mvars` to false causes metavariables to pretty print as
`?_`.
* Setting `pp.mvars.withType` to true causes metavariables to pretty
print with type ascriptions.
Motivation: when making tests, it is inconvenient using `#guard_msgs`
when there are metavariables, since the unique numbering is subject to
change.
This feature does not use `⋯` omissions since a metavariable is already
in a sense an omitted term. If repeated metavariables do not appear in
an expression, there is a chance that a term pretty printed with
`pp.mvars` set to false can still elaborate to the correct term, unlike
for other omissions.
(In the future we could consider an option that pretty prints uniquely
numbered metavariables as `?m✝`, `?m✝¹`, `?m✝²`, etc. to be able to tell
them apart, at least in the same pretty printed expression. It would
take care to make sure that these names are stable across different
hovers.)
Closes#3781
This coercion caused difficult-to-diagnose bugs sometimes. Because there
are some situations where converting a string to a name should be done
by parsing the string, and others where it should not, an explicit
choice seems better here.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Sends a diagnostic informing the user to run Restart File when a file
dependency is saved.
Based on #3014 because this feature was easier to implement with the new
architecture.
ToDo:
- [x] Adjust vscode-lean4 to display a notification when this diagnostic
appears in a non-annoying way
(https://github.com/leanprover/vscode-lean4/pull/393)
- [x] Use a file watcher to identify changes to files not tracked by VS
Code
- [x] Rebase onto master when #3014 is merged
Incrementally unveil trace children for excessively large nodes to
improve infoview rendering time, adjust particularly chatty
`simp.ground` trace to make use of it.
By having the `pp.proofs` feature use `⋯` when omitting proofs, when
users copy/paste terms from the InfoView the elaborator can give an
error message explaining why the term cannot be elaborated.
Also adds `pp.proofs.threshold` option to allow users to pretty print
shallow proof terms. By default, only atomic proof terms are pretty
printed.
This adjustment was suggested in PR #3201, which added `⋯` and the
related `pp.deepTerms` option.
This PR facilitates augmenting the context of an `InfoTree` with
*partial* contexts while elaborating a command. Using partial contexts,
this PR also adds support for tracking the parent declaration name of a
term in the `InfoTree`. The parent declaration name is needed to compute
the call hierarchy in #3082.
Specifically, the `Lean.Elab.InfoTree.context` constructor is refactored
to take a value of the new type `Lean.Elab.PartialContextInfo` instead
of a `Lean.Elab.ContextInfo`, which now refers to a full `InfoTree`
context. The `PartialContextInfo` is then merged into a `ContextInfo`
while traversing the tree using
`Lean.Elab.PartialContextInfo.mergeIntoOuter?`. The partial context
after executing `liftTermElabM` is stored in values of a new type
`Lean.Elab.CommandContextInfo`.
As a result of this, `Lean.Elab.ContextInfo.save` moves to
`Lean.Elab.CommandContextInfo.save`.
For obtaining the parent declaration for a term, a new typeclass
`MonadParentDecl` is introduced to save the parent declaration in
`Lean.Elab.withSaveParentDeclInfoContext`. `Lean.Elab.Term.withDeclName
x` now calls `withSaveParentDeclInfoContext x` to save the declaration
name.
### Migration
**The changes to the `InfoTree.context` constructor break backwards
compatibility with all downstream users that traverse the `InfoTree`
manually instead of going through the functions in `InfoUtils.lean`.**
To fix this, you can merge the outer `ContextInfo` in a traversal with
the `PartialContextInfo` of an `InfoTree.context` node using
`PartialContextInfo.mergeIntoOuter?`. See e.g.
`Lean.Elab.InfoTree.foldInfo` for an example:
```lean
partial def InfoTree.foldInfo (f : ContextInfo → Info → α → α) (init : α) : InfoTree → α :=
go none init
where go ctx? a
| context ctx t => go (ctx.mergeIntoOuter? ctx?) a t
| node i ts =>
let a := match ctx? with
| none => a
| some ctx => f ctx i a
ts.foldl (init := a) (go <| i.updateContext? ctx?)
| _ => a
```
Downstream users that manually save `InfoTree`s may need to adjust calls
to `ContextInfo.save` to use `CommandContextInfo.save` instead and
potentially wrap their `CommandContextInfo` in a
`PartialContextInfo.commandCtx` constructor when storing it in an
`InfoTree` or `ContextInfo.mk` when creating a full context.
### Motivation
As of now, `ContextInfo`s are always *full* contexts, constructed as if
they were always created in `liftTermElabM` after running the
`TermElabM` action. This is not strictly true; we already create
`ContextInfo`s in several places other than `liftTermElabM` and work
around the limitation that `ContextInfo`s are always full contexts in
certain places (e.g. `Info.updateContext?` is a crux that we need
because we can't always create partial contexts at the term-level), but
it has mostly worked out so far. Note that one must be very careful when
saving a `ContextInfo` in places other than `liftTermElabM` because the
context may not be as complete as we would like (e.g. it may lack
meta-variable assignments, potentially leading to a language server
panic).
Unfortunately, the parent declaration of a term is another example of a
context that cannot be provided in `liftTermElabM`: The parent
declaration is usually set via `withDeclName`, which itself lives in
`TermElabM`. So by the time we are trying to save the full
`ContextInfo`, the declaration name is already gone. There is no easy
fix for this like in the other cases where we would really just like to
augment the context with an extra field.
The refactor that we decided on to resolve the issue is to refactor the
`InfoTree` to take a `PartialContextInfo` instead of a `ContextInfo` and
have code that traverses the `InfoTree` merge inner contexts with outer
contexts to produce a full `ContextInfo` value.
### Bumps for downstream projects
- `lean-pr-testing-3159` branch at Std, not yet opened as a PR
- `lean-pr-testing-3159` branch at Mathlib, not yet opened as a PR
- https://github.com/leanprover/LeanInk/pull/57
- https://github.com/hargoniX/LeanInk/pull/1
- https://github.com/tydeu/lean4-alloy/pull/7
- https://github.com/leanprover-community/repl/pull/29
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
To handle delaborating notations that are functions that can be applied
to arguments, extracts the core function application delaborator as a
separate function that accepts the number of arguments to process and a
delaborator to apply to the "head" of the expression.
Defines `withOverApp`, which has the same interface as the combinator of
the same name from std4, but it uses this core function application
delaborator.
Uses `withOverApp` to improve a number of application delaborators,
notably projections. This means Mathlib can stop using `pp_dot` for
structure fields that have function types.
Incidentally fixes `getParamKinds` to specialize default values to use
supplied arguments, which impacts how default arguments are delaborated.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
I initially expected `Name`s to always faithfully represent internal data, in particular that a name with macro scopes would have a form such as ```foo._@.Module._hyg.1``, and that tombstones would only appear in types that represent pretty-printed output such as as `String` or `Format`. However, that is not what happens. We have `sanitizeNames` which rewrites the `userName` field of local hypotheses to be `Name.str .anonymous "blah✝"`.
Then in the server code, we put these into `names : Array Name`e. This works fine for displaying in the infoview, but if we try to deserialize an `InteractiveHypothesisBundle` inside an RPC method for widget purposes, the `FromJson Name` instance blows up in `String.toName`.
I think my preferred solution is to, rather than 'fix' `String.toName` to accept these names with tombstones, stop pretending that they are actual `Name`s and re-type `InteractiveHypothesisBundle.names : Array String`. This should be a backwards-compatible change w.r.t. infoview code as the JSON representation is a string in either case. It is not backwards compatible w.r.t. meta code that uses this field.
Added recursion cases to the diff algorithm for projections and mdata.
Previously, these would be rendered as the entire expression being different but we can do better
by checking if the recursion args are the same.
With mdata, these are entirely ignored by the diff algorithm.
