lean4checker CI job

Stream: mathlib4

[Joachim Breitner]

Uff, 10min delay for lean4checker on every mathlib CI run. Is that worth it? We don’t expect that to fail normally, do we; it’s not really checking the PR at hand, but rather hunts for bugs in lean/lean4checker?

Could this be a separate CI job, running after a successful build job, that just runs cache get ; lean4checker so that users get the :check: earlier and PRs can be merged faster? Or only run on master?

[Mario Carneiro]

In some sense it's the most important part of the process

[Mario Carneiro]

because there is a hell of a lot of hope for the best thinking in our build tools

[Mario Carneiro]

It's true that errors in that stage are generally errors in lean though, unless you write some adversarial code

[Alex J. Best]

I think it would be ideal to parallelize the linting testing and lean4checker steps, or indeed everything that is done post main build / olean creation

[Eric Rodriguez]

I feel like it's important to run every so often but I agree it's highly unlikely to fail.

[Kim Morrison]

Unfortunately parallelising a big refactor, as we can only parallelize jobs, not steps.

[Kim Morrison]

(I guess we could combine steps into one, and do command line parallelization?)

[Kim Morrison]

Using jobs is then inconvenient as we need to manually transfer the build artifacts between jobs. Even if we do this by just adding lots of calls to cache get, it is probably still a win. But this ugliness is why I haven't attempted this.

[Kim Morrison]

I would prefer that we keep running lean4checker if at all possible. It very very rarely fails, but when it does we would like to know as soon as possible!

[Eric Wieser]

I think the cache get parallelization is a reasonable approach here, though explicitly transferring the cache would be more robust to network issues

[Kim Morrison]

cache get first, and then manual transfer later if it seems helpful?

[Jireh Loreaux]

Scott, could we just run lean4checker once a day on master? Or is that not frequent enough? It would save lots of CI time.

[Kim Morrison]

Where will failures go?

[Jeremy Tan]

To a Zulip thread, of course

[Mario Carneiro]

Jireh Loreaux said:

Scott, could we just run lean4checker once a day on master? Or is that not frequent enough? It would save lots of CI time.

What about running it only in staging commits?

[Kim Morrison]

Okay, I think I would be okay with checking master every 24 hours, particularly if someone else can implement it. :-) I agree CI is too slow still.

[Mario Carneiro]

I like the always-green property, as I might have mentioned in another thread :)

[Yaël Dillies]

Yeah I was coming on this thread to suggest just this: only run lean4checker on staging commits, so that we don't waste CI time in PRs.

[Kevin Buzzard]

Why are people so worried about something taking ten minutes, out of interest?

[Joachim Breitner]

For example when I have a draft PR, and I want to mark it as ready for review or merging or so, but not before I know for sure that CI is green. I keep checking the status until it’s green.

Like yesterday, when I wanted to get nightly-testing working again, a minute less CI time is a minute less until I am “done”.

[Eric Rodriguez]

I think this is something that mergify lets me do automatically, I'll have a look into supporting something like this.

[Eric Rodriguez]

(Joachim's workflow)

[Arthur Paulino]

Kevin Buzzard said:

Why are people so worried about something taking ten minutes, out of interest?

Think 10 * n_total_commits * cost_per_minute_in_$

[Joachim Breitner]

That too. Also * cost_per_minute_in_CO₂.
(Not that it matters much next to all those AI stuff happening, I guess)

[Alex J. Best]

Kevin Buzzard said:

Why are people so worried about something taking ten minutes, out of interest?

At least for me I notice this the most when testing new features for CI itself (like reviewdog, leaff), there I often make a commit that doesn't change mathlib at all, but then I have to wait 20 minutes (for lint + testing + checker) to find out I made a typo in my script...

[Joachim Breitner]

Testing CI features right now, so while I have a break of 10mins I thought I come back to this thread ;-)