feat: partial context info by mhuisi · Pull Request #3159 · leanprover/lean4

mhuisi · 2024-01-10T15:04:28Z

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:

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 InfoTrees 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, ContextInfos 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 ContextInfos in several places other than liftTermElabM and work around the limitation that ContextInfos 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
chore: bump for lean4#3159 LeanInk#57
chore: bump for lean4#3159 hargoniX/LeanInk#1
chore: bump for lean4#3159 tydeu/lean4-alloy#7
chore: bump for lean4#3159 leanprover-community/repl#29

ghost · 2024-01-10T15:35:28Z

💥 Mathlib branch lean-pr-testing-3159 build failed against this PR. (2024-01-10 15:35:26) View Log
💥 Mathlib branch lean-pr-testing-3159 build failed against this PR. (2024-01-10 15:55:32) View Log
💥 Mathlib branch lean-pr-testing-3159 build failed against this PR. (2024-01-10 16:36:01) View Log
🟡 Mathlib branch lean-pr-testing-3159 build this PR didn't complete normally. (2024-01-11 13:18:10) View Log
🟡 Mathlib branch lean-pr-testing-3159 build this PR didn't complete normally. (2024-01-11 16:08:02) View Log
✅ Mathlib branch lean-pr-testing-3159 has successfully built against this PR. (2024-01-12 11:07:08) View Log
✅ Mathlib branch lean-pr-testing-3159 has successfully built against this PR. (2024-01-12 12:18:24) View Log
🟡 Mathlib branch lean-pr-testing-3159 build against this PR was cancelled. (2024-01-19 12:42:25) View Log
✅ Mathlib branch lean-pr-testing-3159 has successfully built against this PR. (2024-01-19 13:56:14) View Log
✅ Mathlib branch lean-pr-testing-3159 has successfully built against this PR. (2024-01-19 15:56:48) View Log

kim-em · 2024-01-11T04:52:56Z

I've added full-ci, as we're going to need to update ProofWidgets4 to get this tested.

Next steps when that is ready:

update lean-pr-testing-3159 at ProofWidgets (which I've created, but not updated)
push a v0.0.26-pre tag to ProofWidgets4 from the lean-pr-testing-3159 branch
change the Mathlib lean-pr-testing-3159 branch to use ProofWidgets @ v0.0.26-pre
see what else breaks?

src/Lean/Elab/InfoTree/Types.lean

src/Lean/Elab/Tactic/Basic.lean

…pt for leanprover/lean4#3159

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`. <details> <summary>Showing the call hierarchy (click to show image)</summary> ![show_call_hierarchy](https://github.com/leanprover/lean4/assets/10852073/add13943-013c-4d0a-a2d4-a7c57ad2ae26) </details> <details> <summary>Incoming calls (click to show image)</summary> ![incoming_calls](https://github.com/leanprover/lean4/assets/10852073/9a803cb4-6690-42b4-9c5c-f301f76367a7) </details> <details> <summary>Outgoing calls (click to show image)</summary> ![outgoing_calls](https://github.com/leanprover/lean4/assets/10852073/a7c4f193-51ab-4365-9473-0309319b1cfe) </details> 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 #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`.

* feat: hover info for `rcases h : ...` (#486) * feat: hover info for `rcases h : ...` * fix * chore: adaptations for leanprover/lean4#3123 (#502) * chore: adaptations for leanprover/lean4#3123 * update toolchain * chore: remove unnecessary `have` (#516) After leanprover/lean4#3132 the linter will complain about this. * chore: simproc PR changes (#496) See leanprover/lean4#3124 Co-authored-by: Scott Morrison <scott.morrison@gmail.com> * chore: adaptions for nightly-2023-01-11 (#524) * advance toolchain to nightly-2024-01-12, no updates required * chore: updates to DiscrTree for changes in nightly (#536) * doc: extend docstrings for `ext` and `ext1` (#525) Makes sure to mention that the patterns are processed using `rintro`, and makes sure `ext` mentions `ext1`. * docs(Data/List): typo (#529) * feat: Eq.rec lemma (#385) * chore: Add empty collection instance to BinomialHeap (#532) * Incremental Library Search (#421) This ports library_search from Mathlib to Std. It preserves the ability to do caching, but is designed to support a cacheless mode. The exact and apply tactics are named `std_exact?` and `std_apply?`, but will eventually be renamed. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> * fix termination_by clauses in LazyDiscrTree fix LibrarySearch * bump toolchain --------- Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz> Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Joe Hendrix <joe@lean-fro.org> * feat: adaptations for leanprover/lean4#3159 (#557) * merge origin/main * chore: fixes for `simp` refactor (#571) * move to v4.6.0-rc1 * fix proofs --------- Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Leonardo de Moura <leonardo@microsoft.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz> Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Joe Hendrix <joe@lean-fro.org>

) * feat: hover info for `rcases h : ...` (leanprover-community#486) * feat: hover info for `rcases h : ...` * fix * chore: adaptations for leanprover/lean4#3123 (leanprover-community#502) * chore: adaptations for leanprover/lean4#3123 * update toolchain * chore: remove unnecessary `have` (leanprover-community#516) After leanprover/lean4#3132 the linter will complain about this. * chore: simproc PR changes (leanprover-community#496) See leanprover/lean4#3124 Co-authored-by: Scott Morrison <scott.morrison@gmail.com> * chore: adaptions for nightly-2023-01-11 (leanprover-community#524) * advance toolchain to nightly-2024-01-12, no updates required * chore: updates to DiscrTree for changes in nightly (leanprover-community#536) * doc: extend docstrings for `ext` and `ext1` (leanprover-community#525) Makes sure to mention that the patterns are processed using `rintro`, and makes sure `ext` mentions `ext1`. * docs(Data/List): typo (leanprover-community#529) * feat: Eq.rec lemma (leanprover-community#385) * chore: Add empty collection instance to BinomialHeap (leanprover-community#532) * Incremental Library Search (leanprover-community#421) This ports library_search from Mathlib to Std. It preserves the ability to do caching, but is designed to support a cacheless mode. The exact and apply tactics are named `std_exact?` and `std_apply?`, but will eventually be renamed. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> * fix termination_by clauses in LazyDiscrTree fix LibrarySearch * bump toolchain --------- Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz> Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Joe Hendrix <joe@lean-fro.org> * feat: adaptations for leanprover/lean4#3159 (leanprover-community#557) * merge origin/main * chore: fixes for `simp` refactor (leanprover-community#571) * move to v4.6.0-rc1 * fix proofs --------- Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Leonardo de Moura <leonardo@microsoft.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz> Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Joe Hendrix <joe@lean-fro.org>

feat: partial context info

b8a5a20

mhuisi requested review from Kha, Vtec234, kim-em and leodemoura as code owners January 10, 2024 15:04

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

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

Update lean-toolchain for testing leanprover/lean4#3159

108f24e

ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 10, 2024

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

Trigger CI for leanprover/lean4#3159

3773c08

doc: adjust RELEASES.md

3d4ec21

mhuisi mentioned this pull request Jan 10, 2024

feat: add call hierarchy support #3082

Merged

kim-em added the full-ci label Jan 11, 2024

kim-em added a commit to leanprover-community/ProofWidgets4 that referenced this pull request Jan 11, 2024

update for leanprover/lean4#3159

051935f

mhuisi mentioned this pull request Jan 11, 2024

chore: bump for lean4#3159 leanprover/LeanInk#57

Merged

chore: temporarily revert RELEASES.md so that CI can run

b3c45ba

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 11, 2024

Trigger CI for leanprover/lean4#3159

d273a09

mhuisi mentioned this pull request Jan 12, 2024

chore: bump for lean4#3159 tydeu/lean4-alloy#7

Closed

ghost 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 12, 2024

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 12, 2024

Trigger CI for leanprover/lean4#3159

51a2f6a

chore: update LeanInk

778edc5

Kha requested changes Jan 19, 2024

View reviewed changes

src/Lean/Elab/InfoTree/Types.lean Show resolved Hide resolved

src/Lean/Elab/Tactic/Basic.lean Outdated Show resolved Hide resolved

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 19, 2024

Trigger CI for leanprover/lean4#3159

b5bdd6d

chore: update LeanInk further

2f6d2be

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 19, 2024

Trigger CI for leanprover/lean4#3159

a16e64f

refactor: doc comment and remove redundant instance

7946ee3

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 19, 2024

Trigger CI for leanprover/lean4#3159

f52c118

mhuisi requested a review from Kha January 22, 2024 08:56

Kha approved these changes Jan 22, 2024

View reviewed changes

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

Merged via the queue into leanprover:master with commit e9f69d1 Jan 22, 2024

mhuisi added a commit to mhuisi/lean4 that referenced this pull request Jan 22, 2024

doc: update RELEASES.md for leanprover#3159

e580a21

github-merge-queue bot pushed a commit that referenced this pull request Jan 22, 2024

doc: update RELEASES.md for #3159 (#3205)

4f41ccf

kim-em added a commit to leanprover-community/batteries that referenced this pull request Jan 23, 2024

feat: adaptations for leanprover/lean4#3159

b191117

kim-em mentioned this pull request Jan 23, 2024

feat: adaptations for leanprover/lean4#3159 leanprover-community/batteries#557

Merged

kim-em added a commit to leanprover-community/batteries that referenced this pull request Jan 23, 2024

feat: adaptations for leanprover/lean4#3159 (#557)

65705c6

antonkov added a commit to Paper-Proof/paperproof that referenced this pull request Jan 25, 2024

Move parser to use InfoTree.visitM instead of manual traversal to ada…

5a564bf

…pt for leanprover/lean4#3159

kim-em mentioned this pull request Jan 30, 2024

feat: adaptations for leanprover/lean4#3159 leanprover-community/ProofWidgets4#39

Merged

yangky11 mentioned this pull request Feb 3, 2024

Handle the Breaking Changes to InfoTree in v4.6.0-rc1 lean-dojo/LeanDojo#132

Closed

digama0 mentioned this pull request Feb 3, 2024

Incorrect environment in command snaps for code action #3250

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: partial context info#3159

feat: partial context info#3159
mhuisi merged 6 commits intoleanprover:masterfrom
mhuisi:mhuisi/partial-context-info

mhuisi commented Jan 10, 2024 •

edited

Loading

Uh oh!

ghost commented Jan 10, 2024 •

edited by ghost

Loading

Uh oh!

kim-em commented Jan 11, 2024 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

mhuisi commented Jan 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Migration

Motivation

Bumps for downstream projects

Uh oh!

ghost commented Jan 10, 2024 • edited by ghost Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kim-em commented Jan 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mhuisi commented Jan 10, 2024 •

edited

Loading

ghost commented Jan 10, 2024 •

edited by ghost

Loading

kim-em commented Jan 11, 2024 •

edited

Loading