feat: lake: reservoir require

[tydeu]

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:

require <scope> / <pkg-name> [@ "git#<rev>"] -- e.g., require "leanprover" / "doc-gen4"

Or in 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 and Source Replacement will come in the future.

Updated and split from #3174.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-4495 build against this PR was cancelled. (2024-06-19 01:12:01) View Log
• ✅ Mathlib branch lean-pr-testing-4495 has successfully built against this PR. (2024-06-19 02:04:54) View Log
• ✅ Mathlib branch lean-pr-testing-4495 has successfully built against this PR. (2024-06-20 18:19:43) View Log
• 🟡 Mathlib branch lean-pr-testing-4495 build against this PR was cancelled. (2024-06-28 22:50:16) View Log
• ✅ Mathlib branch lean-pr-testing-4495 has successfully built against this PR. (2024-06-28 23:43:04) View Log
• ✅ Mathlib branch lean-pr-testing-4495 has successfully built against this PR. (2024-06-29 01:13:54) View Log