Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
39bffb6fda
This PR fixes a performance issue where the Lean language server would walk the full project file tree every time a file was saved, blocking the processing of all other requests and notifications and significantly increasing overall language server latency after saving. This issue was originally reported at https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Compiling.20too.20slow/near/484386515 and uncovered in a lengthy investigation. The performance bug that causes the Lean language server to walk the full project file tree when the file watcher for .ilean files is triggered was introduced when the .ileans were first introduced, whereas the specific issue of file saving also triggering the walk was introduced by #3247 in 4.8.0 and the use of the file watcher for .lean files, which would then also trigger the directory walk. Combining this with VS Code's auto-save feature causes the language server to walk the full project file tree on every change of the document. It somehow hasn't really been much of an issue until now, but we still do way too much work in the watchdog main loop. I'll look into resolving that more general issue in the future. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| debug.log | ||
| 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).