Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Reservoir dependents for git dependencies #49

Closed
kim-em opened this issue Sep 17, 2024 · 0 comments · Fixed by #54
Closed

Reservoir dependents for git dependencies #49

kim-em opened this issue Sep 17, 2024 · 0 comments · Fixed by #54
Assignees
Labels
A-package Area: Package data. Issue seeks more package info. C-enhancement Category: Issue requires a new feature. P-high Priority: High. We will work on this issue.

Comments

@kim-em
Copy link

kim-em commented Sep 17, 2024

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.

@tydeu tydeu transferred this issue from leanprover/lean4 Sep 17, 2024
@tydeu tydeu added C-enhancement Category: Issue requires a new feature. A-package Area: Package data. Issue seeks more package info. labels Sep 17, 2024
@tydeu tydeu changed the title Reservoir dependency reporting bug. Reservoir dependents for git dependencies Sep 17, 2024
@tydeu tydeu added the P-high Priority: High. We will work on this issue. label Sep 23, 2024
@tydeu tydeu closed this as completed in #54 Oct 5, 2024
@tydeu tydeu closed this as completed in f61224d Oct 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-package Area: Package data. Issue seeks more package info. C-enhancement Category: Issue requires a new feature. P-high Priority: High. We will work on this issue.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants