lake: could not materialize package

[jcommelin]

While working on mathlib branch bump/nightly-2024-09-11 (see leanprover-community/mathlib4#16716) we used the new Reservoir dependency syntax, but received the error message:

$ lake update LeanSearchClient
error: leanprover-community/LeanSearchClient: could not materialize package: dependency has no explicit source and was not found on Reservoir

This error is both going to be reasonably common (whenever someone doesn't understand how reservoir works), and is not actionable.

Could we please add:
"

• To see why it is not on Reservoir, visit https://...
• If you did not intend to use Reservoir, and the dependency is available on GitHub, please replace your require line with

require foo from git "https://github.com/org/repo" @ hash

• or otherwise with the https URL for the git repository of this package.
  "

If the first bullet point is complicated to implement, we should implement the 2nd and 3rd bullet points in the meantime.

We could do even more here:

• explain why it is not on reservoir?
• check if it is on github and then be more specific in the help

[kim-em]

@jcommelin, I took the liberty of rewriting. :-)

[tydeu]

As an aside, in regards to this particular error, note that a package can use both an explicit source (i.e., from git) and still provide a Reservoir require. For example:

require "leanprover-community" / "LeanSearchClient" 
  from git "https://github.com/leanprover-community/LeanSearchClient.git" @ "main"