Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
848832dd61
This PR makes `saveModuleData` throw an IO.Error instead of panicking, if given something that cannot be serialized. This doesn't really matter for saving modules, but is handy when writing tools to save auxiliary date in olean files via Batteries' `pickle`. The caller of this C++ function already is guarded in a `try`/`catch` that promotes from a `lean::exception` to an `IO.userError`. A simple test of this in the web editor is ``` import Batteries #eval pickle "/tmp/foo.txt" fun x : Nat => x ``` which crashes before this change. --------- Co-authored-by: Laurent Sartran <lsartran@google.com> |
||
|---|---|---|
| .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 Setting Up Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.