feat: lake: require dependencies by semver range

[tydeu]

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

require "Seasawher" / "mdgen" @ "2.*"

lakefile.toml

[[require]]
name = "mdgen"
scope = "Seasawher"
version = "2.*"

The syntax for these versions ranges is a mix of Rust's and Node's 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.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-26 01:24:27)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-31 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-02 02:16:58)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-10959 has successfully built against this PR. (2025-10-26 02:39:58) View Log
• ✅ Mathlib branch lean-pr-testing-10959 has successfully built against this PR. (2025-11-02 03:21:08) View Log
• ✅ Mathlib branch lean-pr-testing-10959 has successfully built against this PR. (2025-11-03 02:56:13) View Log
• ✅ Mathlib branch lean-pr-testing-10959 has successfully built against this PR. (2025-11-03 05:20:19) View Log