mathlib currently shows a build failure for v4.3.0

[kim-em]

It seems that when reservoir wanted to test everything on v4.3.0, it checked out a9f7e64691 of Mathlib, and correctly found that this didn't compile against v4.3.0. However, as this commit of Mathlib had explicitly moved on to a later toolchain v4.4.0-rc1, I don't think we should have put a red X against the v4.3.0 toolchain, rather than keeping the green check for the previous commit which did work against v4.3.0.

[tydeu]

@semorrison It appears that unfortunately Reservoir never had a successful mathlib build for 4.3.0: leanprover/reservoir-index@1c84d78. However, #9 should ensure that builds failures never do end up overwriting previous successes.

[kim-em]

Does it make sense to just manually clear out this particular failure?

[tydeu]

@semorrison I thought of doing that, but similar failures will just reappear whenever we test a stable branch against mathlib, since the latest stable will rarely ever be compatible with mathlib.

[kim-em]

I think it's essential that reservoir shows green ticks next to every stable release on the Mathlib page, and moreover makes it obvious to the viewer how that should obtain a copy of Mathlib that compiles against those stable releases!

We put a lot of effort into making that posssible, and it's not okay for reservoir to just throw this away.

I don't particularly mind how it is done:

• manually?
• walking Mathlib's master branch, identifying the last commits on each stable release and testing those?
• providing a mechanism for Mathlib to communicate to reservoir that it promises that each stable v4.X.0 will have a tag also named v4.X.0 that will compile against that toolchain, and have reservoir act on this information

[tydeu]

@semorrison I agree that Reservoir should somehow extract Mathlib's version tags. And I plan to work on a way to do that soon (though, sadly, it won't happen until after Lean Together). This issue can track that, while the more general discussion of the what Reservoir should compare against can occur in #10.

[tydeu]

With Reservoir 1.0 (#45), we can now store builds per version tag extract from the repository, addressing the major feature request of this issue., I have also manually triggered builds for mathlib on these old versions (giving them green checks on Reservoir). While filling in such builds is a process that should ideally be automated in the future, that seems like a separate issue. Thus, I am closing this one.