leanprover / reservoir

Package registry for Lean/Lake.
https://reservoir.lean-lang.org
Apache License 2.0
16 stars 1 forks source link

Reservoir dependents for git dependencies #49

Open kim-em opened 2 weeks ago

kim-em commented 2 weeks ago

Reservoir doesn't report most of the dependents of Mathlib, even though it reports these projects as dependents of Batteries and Aesop (and this dependency is only acquired via the transitive dependency through Mathlib).

Presumably this is because Mathlib uses a Reservoir require for Batteries and Aesop, but very few projects use a Reservoir require for Mathlib as yet.

This looks pretty bad, and is not restricted to Mathlib.

Proposed fix: when Reservoir looks at a package, if it sees a old style git repository, it matches it against the known git urls of Reservoir packages, and does dependency analysis using this information.