Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
af0b563099
After each tactic step, we save the info tree created by it together with an appropriate info tree context that makes it stand-alone (which we already did before to some degree, see `Info.updateContext?`). Then, in the adjusted request handlers, we first search for a snapshot task containing the required position, if so wait on it, and if it yielded an info tree, use it to answer the request, or else continue searching and waiting, falling back to the full info tree, which should be unchanged by this PR. The definition header does *not* report info trees early as in general it is not stand-alone in the tactic sense but may contain e.g. metavariables solved by the body in which case we do want to show the ultimate state as before. This could be refined in the future in case there are no unsolved mvars. The adjusted request handlers are exactly the ones waited on together by the info view, so they all have to be adjusted to have any effect on the UX. Further request handlers may be adjusted in the future. No new tests as "replies early" is not something we can test with our current framework but the existing test suite did help in uncovering functional regressions. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| lean.code-workspace | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
This is the repository for Lean 4.
About
- Quickstart
- 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 (documentation source: doc/make/index.md).