feat: lake: require overhaul
#3174
Draft
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 13, 2024
62ee6c4 to
36512d7
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 13, 2024
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 13, 2024
|
Mathlib CI status (docs):
|
36512d7 to
199aaa9
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 16, 2024
199aaa9 to
d3abba5
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 16, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 17, 2024
c94e8c7 to
a892c70
Compare
0c0e55b to
3b1bc72
Compare
b531bf4 to
88fd601
Compare
This was referenced May 6, 2024
github-merge-queue bot
pushed a commit
that referenced
this pull request
May 24, 2024
Switches the manifest format to use `major.minor.patch` semantic versions. Major version increments indicate breaking changes (e.g., new required fields and semantic changes to existing fields). Minor version increments (after `0.x`) indicate backwards-compatible extensions (e.g., adding optional fields, removing fields). This change is backwards compatible. Lake will still successfully read old manifest with numeric versions. It will treat the numeric version `N` as semantic version `0.N.0`. Lake will also accept manifest versions with `-` suffixes (e.g., `x.y.z-foo`) and then ignore the suffix. This change also includes the general cleanup/refactoring of the manifest code and data structures that was part of #3174.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Jun 29, 2024
Adds a new type of `require` which fetches package metadata from a registry API endpoint (i.e., Reservoir) and then clones a Git package using the information provided. To require such a dependency, the new syntax is: ```lean require <scope> / <pkg-name> [@ "git#<rev>"] -- e.g., require "leanprover" / "doc-gen4" ``` Or in TOML: ```toml [[require]] name = "<pkg-name>" scope = "<scope>" rev = "<rev>" ``` Unlike with Git dependencies, Lake can make use of the richer information provided by the registry to determine the default branch of the package. This means for repositories of packages like `doc-gen4` which have a default branch that is not `master`, Lake will now use said default branch (e.g., in `doc-gen4`'s case, `main`). Lake also supports configuring the registry endpoint via an environment variable: `RESERVIOR_API_URL`. Thus, any server providing a similar interface to Reservoir can be used as the registry. Further configuration options paralleling those of Cargo's [Alternative Registries](https://doc.rust-lang.org/cargo/reference/registries.html) and [Source Replacement](https://doc.rust-lang.org/cargo/reference/source-replacement.html) will come in the future. Updated and split from #3174.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR contains major changes to
requireDSL, the Lake manifest format, types of dependencies, and the how packages and targets are named. These changes overlap in significant ways, hence why there were all done as part of one PR. However, due to its complexity, it may be worthwhile to break significant parts of it up into smaller PRs. What follows is a summary of the major components of the current PR.This PR depends on leanprover/reservoir#18 being merged (and its tests will need to be update once it is).
requireDocstringsLake now supports docstrings on
requirecommands:Closes #2898.
require ... if ...& Locked Conditional DependenciesTo specify conditional dependencies, the previous approach of, e.g.:
has been replaced with:
This replacement is backwards-compatible. Lake will intelligently expand
meta if .. require ...torequire ... if ..with a deprecation warning asking the user to update their configuration file accordingly.The advantage of this change is that require statements are no longer conditionally elaborated. Instead, conditional dependencies are always part of a package's configuration. They just have settings indicating whether they are conditional and whether the dependency is enabled in a given configuration.
Lake makes use of the information to ensure the manifest always contains a complete record of all possible package dependencies locked to a specific version. That is,
lake updatewill materialize and lock all dependencies -- even those not enabled. Other commands (e.g.,lake build) will just materialize / use the packages enabled with the set configuration. This helps ensure reproducible builds across different configurations.GitHub Dependency Source
Packages which are required from GitHub can now state this explicitly via new
requiresyntax and a new source type rather than reusing the standardgitsource. For example,While Lake could deduce this from some URLs, making this explicit avoids heuristic errors and allows Lake to better provide GitHub-specific features. For instance, Lake now respects a
LAKE_GITHUB_URLenvironment variable to point Lake to a different URL (other thanhttps://github.com) from which to clone GitHub packages. This should help enable, for example, GitHub mirrors in restricted internet contexts and compatibility with Enterprise editions of GitHub.Reservoir Registry Dependency
Adds a new
registrypackage source which fetches package metadata from a API endpoint (e.g., Reservoir's) and clones a Git package using the information provided. To require such a dependency, the new syntax is:require <scope> / <pkg-name> [@ <rev>] -- e.g., require "leanprover" / "doc-gen4"Unlike with Git dependencies, Lake can make use of the richer information provided by the registry to determine the default branch of the package. This means for repositories of packages like
stdwhich have a default branch that is notmaster, Lake will now use said default branch (e.g., in std's case,main).Also, as with GitHub dependencies, Lake supports configuring the registry endpoint via an environment variable:
LAKE_RESERVIOR_URL. Thus, any server providing a similar interface to Reservoir can be used as the registry. Further configuration options paralleling those of Cargo's Alternative Registries and Source Replacement will come in future PRs.Simple Package & Target Names
To implement Reservoir dependencies, an important detail was to have the package names specified in the
requirestatement match those of the package being required. Previously, a mismatch was just warning, but experience has shown this should be a error (as things break otherwise). Reservoir gets its package names from thelake-manifest.jsonof the indexed package, thus it is important the name listed there matches and is easily machine-readable.Before this PR, this name was naively produced via a
toJSONon the package'sname : Namefield. However, this can produce names with escapes that are hard for non-Lean machines to read. These escapes can be removed via settingescape := falseinName.toString, but this makes the name not round-trip if it contains multiple components. To avoid this, Packages are now forced to have simple names (i.e., aNamewith a single string component). For consistency's sake, this PR also changes targets (e.g.,lean_lib,lean_exe, andtarget) to have simple names as well.It is important note that this is a major API refactor with potential for breakage in complex configuration files. I have tried to minimized the places were breakage could occur, but they still exist. For instance, targets identified to by a multipart name literal will no longer exist and produce an error. Unfortunately, the simple FFI example in Lake used such a target:
It needed to be changed to:
There are several such cases in the larger Lean ecosystem as well (e.g., loogle). This is likely because they followed the naming pattern of the example.