Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
e9f69d1068
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> |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| default.nix | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| lean.code-workspace | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
| shell.nix | ||
This is the repository for Lean 4.
We provide nightly releases and have just begun regular stable point releases.
About
- Quickstart
- Walkthrough installation video
- Quick tour video
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean
- Manual
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
- FAQ
Installation
See Setting Up Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.