Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
7c9519e60c
This PR modifies `all_goals` so that in recovery mode it commits changes to the state only for those goals for which the tactic succeeds (while preserving the new message log state). Before, we were trusting that failing tactics left things in a reasonable state, but now we roll back and admit the goal. The changes also fixes a bug where we were rolling back only the metacontext state and not the tactic state, leading to an inconsistent state (a goal list with metavariables not in the metacontext). Closes #7883 Alternatively we could stop on the first error, however it is helpful to see what the tactic did to each goal while interactively writing a tactic script. There is some non-monotonicity here though since tactics can solve for metavariables that appear in successive goals, and conceivably a later goal succeeds only if a previous one does. Given that the non-monotonicity is limited to recovery mode (which is for example the RHS and not the LHS of the `<;>` combinator), we think this is acceptable. Another justification for the change to roll back the state on each failure is that we need to admit goals in the failing cases. When a tactic throws an error, we cannot assume the goal list is meaningful. Rolling back lets us admit just the goal the tactic started with, without needing to try to work out which new metavariables should be admitted in the error state, allowing the tactic to continue trying the tactic on the next goal. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| 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).