Package registry for Lean 4

Stream: lean4

[Xubai Wang]

The number of Lean 4 package continues growing. Now it's a good time to have a package registry for Lean 4, and that's what I'm working on. The registry is hosted on the GitHub Pages https://xubaiw.github.io/reservoir-index/, with the index repo and source code. The style of user interface follows that of lean4 homepage and doc-gen.

The functionality is quite incomplete now, and it's barely nothing more than a list, but I cannot wait to put it here to see if people have some nice ideas about package registry and even help write some part of the code. So this zulip topic may also be used for feature discussion.

I also wonder if there is possibility to transfer these repos to leanprover to make them the "official" registry after implementing some basic features.

[Xubai Wang]

The registry will try to call github search api periodically to update itself (through pull request), but users can manually add their package information to the index repo.

[Yakov Pechersky]

In browser dark mode, I can't read anything:
image.png

[Xubai Wang]

It works well with my Dark Reader dynamic mode. But yeah, surely, dark mode support will be added to my to-do list.

[Xubai Wang]

I also plans to add documentation rendering to it, using doc-gen4, so it will also play the role of docs.rs.

And then a version picking facility is very important, as we no longer have "version" in lake, and have to rely on the git commit message. People will be able to search through the commit messages easily to find the hash they want.

[Xubai Wang]

The navigation input on top of the page for now does filtering only, but in my idea it should be more flexible and have more diverse functionality.