Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
c9c3366521
This PR adds support for plugins to Lake. Precompiled modules are now loaded as plugins rather than via `--load-dynlib`. Additional plugins can be added through an experimental `plugins` configuration option. The syntax for specifying this is not yet convenient, and will be improved in future changes. A parallel `dynlibs` configuration option has been added for specifying additional dynamic libraries to build and pass to `--load-dynlib`. This PR also changes the default directory for `.olean`, `.ilean`, and module dynamic libraries (i.e., `leanLibDir`) to `lib/lean` instead of the previous default of `lib`. This avoids potential name clashes between single module shared libraries and the shared libraries of a full `lean_lib`. On non-Windows systems, module dynamic libraries are no longer linked to their imports or external symbols. Symbols from those libraries are left unresolved until load time. This avoids nesting these dependencies within the shared library and means Lake no longer needs to augment the shared library path to allow Lean to resolve such nested dependencies on load. |
||
|---|---|---|
| .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).