Lean4 package/code discovery

Stream: lean4

[Andrew Kent]

How do people (plan to?) answer the question "is X already implemented by someone in Lean4"? (I know I may be asking this a bit prematurely, but figured why the hell not =)

In my particular case, I'm tempted to start building a package for declarative command line argument parsing (perhaps like Rust's clap or Haskell's optparse-applicative)... but it would be nice to know if someone else has started down this path already just in case =)

[Sebastian Ullrich]

It's probably a bit early to invest time in building a leanpkg index or anything similarly fancy :) , but it would be great to have something like https://leanprover-community.github.io/lean_projects.html for Lean 4 projects!

[Bryan Gin-ge Chen]

If everyone tags their Lean 4 repos with lean4 on GitHub, we would get a crude directory here: https://github.com/topics/lean4

[Anders Christiansen Sørby]

Could we add a separate stream for discussing the growing lean4 package ecosystem? #lean4-packages for example. Would be nice to have a place to coordinate and discuss and ask for contributions.

[Henrik Böving]

Since this is not at all a priority in Lean 4 development right now the efforts regarding this will most likely be only by a few individuals so it'll probably fit just nicely in here.

[Anders Christiansen Sørby]

Sure. I just didn't want to spam the lean4 stream more than necessary.