Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
22d1d04059
This PR fixes a bug where the goal state selection would sometimes select incomplete incremental snapshots on whitespace, leading to an incorrect "no goals" response. Fixes #6594, a regression that was originally introduced in 4.11.0 by #4727. The fundamental cause of #6594 was that the snapshot selection would always select the first snapshot with a range that contains the cursor position. For tactics, whitespace had to be included in this range. However, in the test case of #6594, this meant that the snapshot selection would also sometimes pick a snapshot before the cursor that still contains the cursor in its whitespace, but which also does not necessarily contain all the information needed to produce a correct goal state. Specifically, at the `InfoTree`-level, when the cursor is in whitespace, we distinguish competing goal states by their level of indentation. The snapshot selection did not have access to this information, so it necessarily had to do the wrong thing in some cases. This PR fixes the issue by adjusting the snapshot selection for goals to explicitly account for whitespace and indentation, and refactoring the language processor architecture to thread enough information through to the snapshot selection so that it can decide which snapshots to use without having to force too many tasks, which would destroy incrementality in goal state requests. Specifically, this PR makes the following adjustments: - Refactor `SnapshotTask` to contain both a `Syntax` and a `Range`. Before, `SnapshotTask`s had a single range that was used both for displaying file progress information and for selecting snapshots in server requests. For most snapshots, this range did not include whitespace, though for tactics it did. Now, the `reportingRange` field of `SnapshotTask` is intended exclusively for reporting file progress information, and the `Syntax` is used for selecting snapshots in server requests. Importantly, the `Syntax` contains the full range information of the snapshot, i.e. its regular range and its range including whitespace. - Adjust all call-sites of `SnapshotTask` to produce a reasonable `Syntax`. - Adjust the goal snapshot selection to account for whitespace and indentation, as the `InfoTree` goal selection does. - Fix a bug in the snapshot tree tracing that would cause it to render the `Info` of a snapshot at the wrong location when `trace.Elab.info` was also set. This PR is based on #6329. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases | ||
| 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
- 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).