Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
528c0dd2e4
This PR enables Lake users to require Reservoir dependencies by a semantic version range. On a `lake update`, Lake will fetch the package's version information from Reservoir and select the newest version of the package that satisfies the range. ### Using Version Ranges Version ranges can be specified through the `version` field of a TOML `require` or the `@` clause of a Lean `require`. They are only meaningful on Reservoir dependencies. **lakefile.lean** ```lean-4 require "Seasawher" / "mdgen" @ "2.*" ``` **lakefile.toml** ```toml [[require]] name = "mdgen" scope = "Seasawher" version = "2.*" ``` The syntax for these versions ranges is a mix of [Rust's](https://doc.rust-lang.org/stable/cargo/reference/specifying-dependencies.html?highlight=caret#version-requirement-syntax) and [Node's](https://github.com/npm/node-semver/tree/v7.7.3?tab=readme-ov-file#ranges) with some Lean-friendly deviations. ### Comparators The basic unit of semantic version ranges are version comparators. They take a base version and a comparison operator and match versions which compare positively with their base. Lake supports the following comparison operators. * `<`, `<=` / `≤`, `>`, `>=` / `≥`, `=`, `!=` / `≠` Unlike Rust and Node, Lake supports Unicode alternatives for the operators. It also adds the not-equal operator (`!=` / `≠`) to make excluding broken versions easier. Comparators can be combined into clauses via conjunction or disjunction: * **AND clauses**: Rust-style `≥1.2.3, <1.8.0` or Node-style `1.2.3 <1.8.0` * **OR clauses**: Node-style `1.2.7 || >=1.2.9, <2.0.0` When the base version of a comparator has a `-` suffix (e.g., `>1.2.3-alpha.3`) it will match versions of the same core (`1.2.3`) with suffixes that lexicographically compare (e.g., `1.2.3-alpha.7` or `1.2.3-beta.2`) but will not match suffixed versions of different cores (e.g., `3.4.5-rc5`). An empty `-` suffix can be used to disable this behavior. For example, `<2.0.0-` will match `1.2.3-beta.2` and `2.0.0-alpha.1`. ### Range Macros In addition to the basic comparators, Lake also supports standard shorthand for specifying more complex ranges. Namely, it supports the caret (`^`) and tilde (`~`) operator along with wildcard ranges. **Caret Ranges** * `^1` => `≥1.0.0, <2.0.0-` * `^1.2` => `≥1.2.0, <2.0.0-` * `^1.2.3` => `≥1.2.3, <2.0.0-` * `^1.2.3-beta.2` => `≥1.2.3-beta.2, <2.0.0-` * `^0.2` => `≥0.0.0, <0.3.0-` * `^0.2.3` => `≥0.2.3, <0.3.0-` * `^0.0.3` => `≥0.0.3, <0.0.4-` * `^0` => `≥0.0.0, <1.0.0-` * `^0.0` => `≥0.0.0, <0.1.0-` **Tilde Ranges** * `~1` => `≥1.0.0, <2.0.0-` * `~1.2` => `≥1.2.0, <1.3.0-` * `~1.2.3` => `≥1.2.3, <1.3.0-` * `~1.2.3-beta.2` => `≥1.2.3-beta.2, <1.3.0-` * `^0` => `≥0.0.0, <1.0.0-` * `^0.2.3` => `≥0.2.3, <0.3.0-` * `^0.0.3` => `≥0.0.3, <0.0.4-` * `~0` => `≥0.0.0, <1.0.0-` * `~0.0` => `≥0.0.0, <0.1.0-` * `~0.0.0` => `≥0.0.0, <0.1.0-` **Wildcard Ranges** * `*` => `≥0.0.0` * `1.x` => `≥1.0.0, <2.0.0-` * `1.*.x` => `≥1.0.0, <2.0.0-` * `1.2.*` => `≥1.2.0, <1.3.0-` These ranges closely follow Rust's and Node's syntax. Like Node but unlike Rust, wildcard ranges support `x` and `X` as alternative syntax for wildcards. |
||
|---|---|---|
| .claude/commands | ||
| .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 Install Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean.