feat: partial context info

[mhuisi]

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

[leanprover-community-mathlib4-bot]

• 💥 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]

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?