CI failure on `main`

Stream: batteries

[Kim Morrison]

We just had a broken main: std4#533 was green, but after hitting main it failed. I fixed it in #541, which I merged myself.

[Kim Morrison]

Might be time for bors or mergify!

[Mario Carneiro]

We can also use GHMQ, std has fairly low CI requirements

[Mario Carneiro]

I think that's what lean core is using?

[Kim Morrison]

Yes, we use the GHMQ and it has been fine for us there.

[Joachim Breitner]

I’d be in favor of unifying the CI and repo setup for lean and std as far as possible, given that std is becoming more and more an inalienable part of “lean” from the user point of view, and ideally contributers shouldn’t learn different workflows.

[Mario Carneiro]

I'm not sure I would go that far. Lean has an unusual CI setup for a lot of reasons related to bootstrapping, and it also produces releases unlike std (because it's a compiler not a library), and it has bots running stuff on std and mathlib (maybe we'll borrow some of that)

[Mario Carneiro]

(Furthermore I have major qualms regarding the contribution pipeline in lean4 core, and do my best to promote a more open model in std)

[Joachim Breitner]

I expect that std will have to be part of releases in the future anyways, so the release process somehow has to straddle both repos anyways.

Of course the bootstrapping issue remain core-specific – but even more reasons to make contributions to std at least as pleasant as to core, so that little code as possible is affected by the bootstrapping complications.

In particular, the CI integration with mathlib should also be available on std, shouldn’t it?

I would hope that we find a way that contributions to either repo are as qualm-free as possible :-)

(This is all my opinion here, nothing official.)