Reservoir status display

Stream: lean4

[Mac Malone]

@Utensil Song / @Patrick Massot A quick update: Reservoir now displays a dark gold checmark for packages that failed to build on the latest toolchain but successfully build on a older version (and this is noted in the checkmark's tooltip). What do you think of this as a solution to leanprover/reservoir#2?

[Mario Carneiro]

I see mathlib4 also has a green checkmark, did something change there?

[Mac Malone]

@Mario Carneiro Yep, it is now included in the daily testbed.

[Mac Malone]

(which only took 35 minutes to build all 229 packages on their package-specified toolchain today. :grinning_face_with_smiling_eyes: )

[Eric Wieser]

Is this leveraging the mathlib cache, or does that number also include building all of mathlib?

[Mac Malone]

@Eric Wieser It's making use of cache.

[Utensil Song]

Looks nice! Why it is gold instead of green is clear once hovered on the check mark.

Just a nitpick, maybe a blue checkmark is more neutral than a dark gold one, but a dark gold one is certainly more neutral than a red or yellow one.

[Utensil Song]

An interesting case is LeanInfer, it builds on the latest Lean v4.4.0-rc1 but not the last stable v4.3.0 because the code is kept up-to-date with v4.4.0-rc1 . Should this case be shown differently? Like in gray. But red cross is also fine, I guess.

image.png

[Mario Carneiro]

I think a cross is fine, assuming there is not a 4.3.0 branch and the existing code does not compile on 4.3.0

[Utensil Song]

Currently, Reservoir builds against the main branch, no assumption is made about version specific branches or tags. But this could be a convention for projects and a feature of Reservoir.

[Utensil Song]

Another case is abel_ruffini_lean which has leanprover/lean4:v4.3.0 in its toolchain file, but fails for both v4.3.0 and v4.4.0-rc1. Checking the code it actually should fail for both, but in the case of v4.3.0, it failed twice, once of missing a file (the right reason), once after lake update and due to leanOption in v4.4.0-rc1, is this expected?

[Mario Carneiro]

even std fails on 4.3.0 because of the leanOption thing

[Patrick Massot]

I still feels very unfair that many projects have only red cross while they do build on the toolchain that announce. For instance https://github.com/leanprover-community/lean4-metaprogramming-book builds on GitHub CI.

[Eric Wieser]

I think this is only true for projects which are on a version of lean that predates reservoir

[Patrick Massot]

Hence that's an issue with reservoir.

[Patrick Massot]

And I still don't understand why the reservoir landing page shows any red cross at all. It should simply filter them out (but still show them in search results of course).

[Mac Malone]

Patrick Massot said:

I still feels very unfair that many projects have only red cross while they do build on the toolchain that announce. For instance https://github.com/leanprover-community/lean4-metaprogramming-book builds on GitHub CI.

Reservoir does regulary build packages on the the toolcahin they specify! :big_smile: leanprover-community/lean4-metaprogramming-book has a red cross because it does not build on its own toolchain with a simple lake build. It is also not clear to me how it is supposed to be built (or, similarly, how the GitHub CI passes).

[Julian Berman]

Mac Malone said:

Patrick Massot said:

I still feels very unfair that many projects have only red cross while they do build on the toolchain that announce. For instance https://github.com/leanprover-community/lean4-metaprogramming-book builds on GitHub CI.

Reservoir does regulary build packages on the the toolcahin they specify! :big_smile: leanprover-community/lean4-metaprogramming-book has a red cross because it does not build on its own toolchain with a simple lake build. It is not clear to me how it is supposed to be built (or, similarly, how the GitHub CI passes).

The book doesn't have CI that runs the actual code unfortunately (I think we left an open issue as a reminder but none of us have gotten to it to my recollection) -- all the CI it has is to generate the PDF.

[Mac Malone]

Patrick Massot said:

And I still don't understand why the reservoir landing page shows any red cross at all. It should simply filter them out (but still show them in search results of course).

I think it is nice to know that there are new and/or popular packages that do not build on any know toolchain. It can, e.g., encourage users to submit a PR to fix them if they wish to use them. It also to make the checkmarks feel more honest by demonstrating that you will get a red cross if things Reservoir cannot build them.

[Mac Malone]

@Julian Berman In that case, and if the text document is the important artifact (which I could see it being), as there been consideration of making that the thing that occurs on a default lake build?

[Julian Berman]

It's occurred to me personally yeah but I didn't suggest it anywhere nor play with trying to make it happen -- honestly I'm a bit embarrassed to have not had as much time to help out with it (and many other things). But I think it makes sense certainly -- (I think probably the compilation from lean -> md needs to fit in there too but that isn't very hard either from my recollection).

[Eric Wieser]

The reason it doesn't build is that the files are demonstrating error messages

[Eric Wieser]

But adding guard_msgs everywhere seems like a waste of time if David is working on better tools for this kind of thing

[Scott Morrison]

I think there's going to have to be a community effort to deal with lots of red crosses! We're definitely looking forward to a sea of green on the reservoir landing page.

[Scott Morrison]

Importantly, I think we should try to develop "best practices", and possibly even a rule, about how packages can declare where you should look for versions compatible with various tool chains.

[Scott Morrison]

As examples, Mathlib/Std/Aesop each create a tag for the first time they update to use a particular rc or stable tool chain, simply using e.g. v4.4.0-rc1 as the tag name.

[Scott Morrison]

lean4checker, for no particularly coherent reason, uses instead toolchain/v4.4.0-rc1.

[Scott Morrison]

It's very important that if tags or branches exist with these intended compatibilities, then reservoir does not show red crosses because the development branch is no longer compatible.

[Scott Morrison]

Whether we want ecosystem wide rules for the naming of such tags or branches, or a way to encode these intentions into a lakefile (or other configuration file), it would be nice to sort this out soon.

[Scott Morrison]

During this week I will try to do a bit of a survey of the red crosses and understand why we have too many (i.e. more than zero :-)

[Scott Morrison]

As far as I'm concerned, any red cross is not just a sign that a package is out of date, but an indication that our tooling is not providing enough help to the package author!

[Utensil Song]

It's reasonable that the landing page of Reservoir displays projects according to some ordering and without filtering. "A project fails to build ⇒ disappear from the front page" would a more disturbing experience than a gold check mark or even a red cross. Displaying the red cross at this stage is healthy, most of them seem fixable with a small PR to the project (or a little heuristics in Reservoir's CI).

One exception will be establishing the convention of branch/tag for the recent Lean versions, Reservoir could give clear hint on this situation instead of just a red cross which would takes time to investigate and wonder what's the best practice.

[Patrick Massot]

Is there any other programming language that proudly presents a webpage full of red crosses like this? Clearly there is no such thing on https://crates.io/ or https://pypi.org/

[Julian Berman]

(I have no direct opinion personally, but just to mention) PyPI does not run any CI for downstream projects (so it doesn't know the answer to have an opinion there), though there has been talk of doing so a scattered few times over the last 15 years to my recollection.

[Scott Morrison]

Just as an example: we really should not be showing a red cross for https://reservoir.lean-lang.org/packages/wellecks-ntptutorial

It has a lakefile.lean, but it is not hooked up at all:

% lake build
error: no such file or directory (error code: 2)
  file: ./././Ntptutorial.lean

[Scott Morrison]

Another way of looking at it is that every such project is "our" fault, not the author's.

[Mario Carneiro]

A major part of it is that reservoir didn't really "ask for permission" to host these projects, unlike pypi and crates.io which grow through explicit submission. Usually the work to get a green checkmark is done during submission but by skipping that step we are looking at a lot of unfinished projects and things that were not designed for consumption in this way

[Mario Carneiro]

I can't speak for pypi, but for crates.io the usual way to submit crates is using cargo publish, and this will build your project before pushing it, so you can be sure that it won't be sent unless it builds. (You can directly send things to crates.io without the build part but this is more cumbersome so most people don't do it.)

[Henrik Böving]

As an additional comment on crates.io, Rust being a language that provides hard stability guarantees does in fact have a process of running the pre release compiler against the entire Eco system before releasing so they dont break those guarantees. And despite having version numbering now Lean 4 is not really a stable release in the sense that many other languages would define stable.