lean package manager

Stream: general

[kapil verma]

is there a package manager for lean? like npm, pip etc? And an equivalent ecosystem where people publish theorems for other people to use

[Eric Wieser]

is there a package manager for lean? like npm, pip etc?

Lean uses leanpkg.toml, which justs uses git urls for package management. leanpkg knows how to fetch the dependencies from this specification.

And an equivalent ecosystem where people publish theorems for other people to use

Right now that ecosystem is primarily the monorepo, mathlib

[Eric Rodriguez]

lean 4 will have something called lake, as far as I know

[Yury G. Kudryashov]

It's hard to have an ecosystem when the main math library changes definitions on a regular basis.

[Arthur Paulino]

That wouldn't be a problem for Lean 4 though, whose scope goes beyond mathematics. It would be reasonable to have an ecosystem of smaller and more stable packages

[Yury G. Kudryashov]

There were some discussions about this. I don't remember what's the current plan.