93c9ae7c20
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. |
||
|---|---|---|
| .. | ||
| app.manifest | ||
| CMakeLists.txt | ||
| lean.cpp | ||
| lean_js.cpp | ||
| manifest.rc | ||
| mk_lean_sh.sh | ||