chore: bump for lean4#3159 #7
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
github-merge-queue bot
pushed a commit
to leanprover/lean4
that referenced
this pull request
Jan 22, 2024
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 <sebasti@nullri.ch>
|
Thanks Marc! I incorporated this PR into 5ae885f. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR bumps alloy for the changes in leanprover/lean4#3159. It should be merged when the v4.6.0 RC is released. Before merging, the toolchain needs to be adjusted.