Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
7b0b1909f1
This PR adds the ability to override package entries in a Lake manifest via a separate JSON file. This file can be specified on the command line with `--packages` or applied persistently by placing it at `.lake/package-overrides.json`. The overrides file is a subset of `lake-manifest.json` with just a version and a `packages` field. The entries in the package share the syntax of the manifest file and take precedence over the entries there. Lake loads the entries from the manifest, then overrides them with those in `.lake/package-overrides.json` (if any) and then those in any file passed to `--packages`. |
||
|---|---|---|
| .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).