Add Lean Programming Language ecosystem

[eric-wieser]

Reservoir here refers to https://reservoir.lean-lang.org/

Let's check with @tydeu, the maintainer thereof, that the verbiage is correct here.

[tydeu]

Looks reasonable to me. Perhaps it would be wise to clarify whether the full name of the Reservoir package is desired (i.e., @leanprover-community/mathlib vs just mathlib)?

[eric-wieser]

@tydeu, would you argue for the inclusion or exclusion of the @ character (given that it does not appear in lakefiles)?

[tydeu]

@eric-wieser I think the @ is a useful marker for disambiguation. But, if the context is unambiguous, it is fine to drop it. As it is not a proper part of the package's name, it should probably not be included in the name here.

[eric-wieser]

So leanprover-community/mathlib would be your preferred format for name? Or @leanprover-community/mathlib to disamguate from the github repo name (which is of course different!)

[tydeu]

@eric-wieser Since the name is already contextually constrained by the ecosystem (Lean), the bare name seems fine. If you wanted to allow either the repository name or the package name as the name, then using the @ as a disambiguator would be reasonable. With the current draft, though, this is unnecessary.

[jess-lowe]

Heya, couple of quick questions:

1. Do you also want to reserve a prefix?
2. Can you please run the script in https://github.com/ossf/osv-schema/blob/main/scripts/update-ecosystems-lists.py to update some of the other related docs.

Thanks :)