Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
e2353689f2
This PR fixes the `floatLetIn` pass to not move variables in case it could break linearity (owned variables being passed with RC 1). This mostly improves the situation in the parser which previously had many functions that were supposed to be linear in terms of `ParserState` but the compiler made them non-linear. For an example of how this affected parsers: ```lean-4 def optionalFn (p : ParserFn) : ParserFn := fun c s => let iniSz := s.stackSize let iniPos := s.pos let s := p c s let s := if s.hasError && s.pos == iniPos then s.restore iniSz iniPos else s s.mkNode nullKind iniSz ``` previously moved the `let iniSz := ...` declaration into the `hasError` branch. However, this means that at the point of calling the inner parser (`p c s`), the original state `s` needs to have RC>1 because it is used later in the `hasError` branch, breaking linearity. This fix prevents such moves, keeping `iniSz` before the `p c s` call. |
||
|---|---|---|
| .claude | ||
| .github | ||
| doc | ||
| images | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .gitpod.Dockerfile | ||
| .gitpod.yml | ||
| .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
- Documentation Overview
- Language Reference
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
Installation
See Install Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.