feat: add call hierarchy support #3082

mhuisi · 2023-12-16T19:35:22Z

This PR adds support for the "call hierarchy" feature of LSP that allows quickly navigating both inbound and outbound call sites of functions. In this PR, "call" is taken to mean "usage", so inbound and outbound references of all kinds of identifiers (e.g. functions or types) can be navigated. To implement the call hierarchy feature, this PR implements the LSP requests textDocument/prepareCallHierarchy, callHierarchy/incomingCalls and callHierarchy/outgoingCalls.

Showing the call hierarchy (click to show image)

Incoming calls (click to show image)

Outgoing calls (click to show image)

It is based on #3159, which should be merged before this PR.

To route the parent declaration name through to the language server, the .ilean format is adjusted, breaking backwards compatibility with version 1 of the ILean format and yielding version 2.

This PR also makes the following more minor adjustments:

Lean.Server.findModuleRefs now also combines the identifiers of constants and FVars and prefers constant over FVars for the combined identifier. This is necessary because e.g. declarations declared using where yield both a constant (for usage outside of the function) and an FVar (for usage inside of the function) with the same range, whereas we would typically like all references to refer to the former. This also fixes a bug introduced in feat: rename request handler #2462 where renaming a declaration declared using where would not rename usages outside of the function, as well as a bug in the unused variable linter where where declarations would be reported as unused even if they were being used outside of the function.
The function converting Lean.Server.RefInfo to Lean.Lsp.RefInfo now also computes the Lean.DeclarationRanges for parent declaration names via MetaM and must hence be in IO now.
Add a utility function Array.groupByKey to HashMap.lean.
Stylistic refactoring of Watchdog.lean and LanguageFeatures.lean.

leanprover-community-mathlib4-bot · 2023-12-16T19:59:01Z

💥 Mathlib branch lean-pr-testing-3082 build failed against this PR. (2023-12-16 19:59:00) View Log
💥 Mathlib branch lean-pr-testing-3082 build failed against this PR. (2023-12-16 20:21:12) View Log
❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-19 16:27:26)
💥 Mathlib branch lean-pr-testing-3082 build failed against this PR. (2023-12-20 14:12:59) View Log
💥 Mathlib branch lean-pr-testing-3082 build failed against this PR. (2024-01-10 13:34:07) View Log
❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. (2024-01-23 09:28:02)
✅ Mathlib branch lean-pr-testing-3082 has successfully built against this PR. (2024-01-24 17:52:01) View Log
✅ Mathlib branch lean-pr-testing-3082 has successfully built against this PR. (2024-01-24 18:31:45) View Log
✅ Mathlib branch lean-pr-testing-3082 has successfully built against this PR. (2024-01-25 12:36:11) View Log

mhuisi · 2023-12-19T16:27:39Z

The previous version of this PR adjusted withDeclName to also save the InfoContext. This was incorrect because this saved InfoContext was not fully complete (e.g. it lacked assignments for metavariables).

The core issue is that we want to save some kind of context while elaborating a term, but cannot meaningfully do so until we are fully done with elaborating the term, lest parts of the saved context may be missing. We already work around this limitation in several other places, e.g. using Info.updateContext?, and the parent declaration name is just one more situation where this comes up.

To solve this issue, the previous commit introduces a notion of PartialContextInfo that replaces the ContextInfo in InfoTree.context. The underlying idea is that while constructing the InfoTree, we augment it with PartialContextInfos where it makes sense, and then when traversing over the tree, we merge outer ContextInfos with inner PartialContextInfos (with fields from inner contexts shadowing those of outer context) into ContextInfos to provide all the context that is available up to this point.

The old ContextInfo that was added by liftTermElabM has been renamed to CommandContextInfo.

Another adjustment made in the previous commit is to remove the incorrect unused variable linter tests checking for unused where declarations. where declarations are accessible from outside of a definition and should hence not be marked as unused, something that is also fixed by this PR.

mhuisi · 2023-12-19T16:38:35Z

(CI is red because LeanInk manually traverses the InfoTree, but the tests are green. PRs for fixing downstream repos tbd)

src/Lean/Server/References.lean

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 - leanprover/LeanInk#57 - hargoniX/LeanInk#1 - tydeu/lean4-alloy#7 - leanprover-community/repl#29 --------- Co-authored-by: Sebastian Ullrich <[email protected]>

src/Lean/Server/References.lean

In v4.6.0, there was a significant regression in initial server startup performance because the .ilean files got bigger in #3082 and we load the information stored in all .ilean files synchronously when the server starts up. This PR makes this loading asynchronous. The trade-off is that requests that are issued right after the initial server start when the references are not fully loaded yet may yield incomplete results. Benchmark for this in a separate PR soon after this one. --------- Co-authored-by: Sebastian Ullrich <[email protected]>

mhuisi added the server Affects the Lean server code label Dec 16, 2023

mhuisi requested review from Vtec234, kim-em, leodemoura and Kha as code owners December 16, 2023 19:35

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 16, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 16, 2023

Update lean-toolchain for testing leanprover/lean4#3082

8afce7a

leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Dec 16, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 16, 2023

Trigger CI for leanprover/lean4#3082

699a838

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 20, 2023

Trigger CI for leanprover/lean4#3082

cd59f1d

mhuisi force-pushed the mhuisi/call-hierarchy branch from 59f4035 to 0aba0a0 Compare January 10, 2024 13:09

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 10, 2024

Trigger CI for leanprover/lean4#3082

3af4fac

mhuisi mentioned this pull request Jan 10, 2024

feat: partial context info #3159

Merged

mhuisi force-pushed the mhuisi/call-hierarchy branch 2 times, most recently from df4a8b7 to 8a8acfc Compare January 11, 2024 12:31

digama0 reviewed Jan 17, 2024

View reviewed changes

src/Lean/Server/References.lean Show resolved Hide resolved

mhuisi force-pushed the mhuisi/call-hierarchy branch 2 times, most recently from 97994ca to 6cd7dcd Compare January 24, 2024 16:14

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 24, 2024

Update lean-toolchain for testing leanprover/lean4#3082

cf9e510

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 24, 2024

Trigger CI for leanprover/lean4#3082

54afcd2

Kha reviewed Jan 24, 2024

View reviewed changes

src/Lean/Server/References.lean Outdated Show resolved Hide resolved

leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jan 24, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 24, 2024

Trigger CI for leanprover/lean4#3082

8f1c710

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 24, 2024

Trigger CI for leanprover/lean4#3082

17326d8

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 25, 2024

Trigger CI for leanprover/lean4#3082

2e1bca0

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 25, 2024

Trigger CI for leanprover/lean4#3082

c965488

mhuisi added 4 commits January 25, 2024 13:33

refactor: enforce column limit in watchdog

e1a72b3

refactor: LanguageFeatures alignment

e7932d3

feat: add call hierarchy support

f3f2a0f

doc: add a couple of missing docstrings

9d8564f

mhuisi force-pushed the mhuisi/call-hierarchy branch from 7d59981 to 9d8564f Compare January 25, 2024 12:33

doc: adjust RELEASES.md

06d5525

mhuisi enabled auto-merge January 25, 2024 14:30

mhuisi added this pull request to the merge queue Jan 25, 2024

Merged via the queue into leanprover:master with commit f9e5f1f Jan 25, 2024
8 checks passed

nomeata mentioned this pull request Jan 30, 2024

refactor: forallAltTelescope to take altNumParams #3230

Merged

mhuisi mentioned this pull request Mar 1, 2024

fix: load references asynchronously #3552

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add call hierarchy support #3082

feat: add call hierarchy support #3082

mhuisi commented Dec 16, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Dec 16, 2023 •

edited

Loading

mhuisi commented Dec 19, 2023

mhuisi commented Dec 19, 2023

feat: add call hierarchy support #3082

feat: add call hierarchy support #3082

Conversation

mhuisi commented Dec 16, 2023 • edited Loading

leanprover-community-mathlib4-bot commented Dec 16, 2023 • edited Loading

mhuisi commented Dec 19, 2023

mhuisi commented Dec 19, 2023

mhuisi commented Dec 16, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Dec 16, 2023 •

edited

Loading