Library/package searching

Stream: general

[Greg Shuflin]

Are there any attempts yet to make a lean package repository system, maybe along the lines of crates.io or hackage?

[James Sully]

yep!
https://reservoir.lean-lang.org/

[Greg Shuflin]

James Sully said:

yep!
https://reservoir.lean-lang.org/

Awesome. It would be great if this could be mentioned on one of the official lean4 documentation pages.

[James Sully]

I think it's still in the early stages. Eg. it currently just gets them from github

[Greg Shuflin]

It would definitely be good if Reservoir didn't assume that GitHub was the only place someone might host an open-source project's git repository :smile:

[James Sully]

I'm sure it's just a stopgap

[James Sully]

I think lake allows you to specify any git repo as a dependency