switching `shake` to run nightly/weekly?

Stream: mathlib4

[Kim Morrison]

I spend a lot of time waiting for CI to re-run after lake exe shake --fix.

I love shake, and definitely want it run all the time. But can we run it periodically outside of the PR process? I would be happy to set up the bots that run it, and report failures to zulip if something goes wrong. (Or even happier if someone else could do this!!).

[Kim Morrison]

And I suspect it is not just me who this holds up. It's moreover a confusing thing to have to deal with for newcomers, and probably better concentrated in experts hands than requiring everyone to interact with it.

[Mario Carneiro]

Another possibility: shake still runs but you can lake exe shake --defer which adds to a "defer" key in noshake which acts just like "ignore", and then lake exe shake --defer --fix will apply any deferred fixes

[Mario Carneiro]

(we could also have lake exe shake --fix also apply deferred fixes, since you will probably be recompiling a big fraction of mathlib anyway and it seems like a good time to empty the queue)

[Pim Otte]

As a newcomer, I did manage to wrongly fix imports, by blindly trusting lake exe shake --fix, but I think this was due to a bug that has been fixed recently.

Something along the same lines that might also be a thing for newcomers: The different (?) linters. The first one that runs immediately is fine, but the one that triggers on missing documentation for def runs after the build, which increases the length of the feedback loop.

Now that I think about this, I will probably write a prepush hook for myself (for both linting and shake). If the issue with shake is "I forgot to run it locally", then that might also be a broader solution?

[Kim Morrison]

Mario Carneiro said:

Another possibility: shake still runs but you can lake exe shake --defer which adds to a "defer" key in noshake which acts just like "ignore", and then lake exe shake --defer --fix will apply any deferred fixes

Doesn't this have the same problem, requiring an extra CI pass to get to green? I'm not really concerned about the difference between --fix and --defer: I just don't want to have to think about it so often.

[Kim Morrison]

If there are people (maintainers particularly) who would support turning it off for every CI run (and instead running periodically), I would appreciate +1s indicating as much. It is a bunch of work to set up the periodic run, and do not want to do that work and then have objections.

[Damiano Testa]

I'm not a maintainer, but would welcome having shorter CI. If you end up getting the periodic run of shake, maybe lean4checker could be placed on the same schedule?

[Kim Morrison]

Yes, definitely.

[Kim Morrison]

I have been hoping someone else would do that for some time. :-)

[Damiano Testa]

Honestly, I tried, but I have some deep misunderstanding of how CI works...

[Damiano Testa]

Or rather, GitHub actions.

[Kim Morrison]

I struggle too, CI is no fun.

[Damiano Testa]

Maybe a simple solution is to run some steps only at a certain time? And maybe configure an empty push at this time to trigger a run with the full CI?

[Kim Morrison]

@Damiano Testa, could you look at https://github.com/leanprover-community/mathlib4/pull/12004?

[Kim Morrison]

And #12005 is an initial attempt at running shake periodically, asking humans for help if something goes wrong. I barely thought about this one, and have to go hop on a plane, so please treat with some skepticism! :-)

[Johan Commelin]

I think Mario is in the best position to judge how hard it is to do library-wide shake-fixes.

[Johan Commelin]

So I would want to give his vote triple-weight, or something like that.

[Ruben Van de Velde]

The actual lake exe shake run takes negligible time, as I recall. I think the main argument to keep it per-pr is that letting issues pile up makes them harder to fix

[Mario Carneiro]

Scott Morrison said:

Mario Carneiro said:

Another possibility: shake still runs but you can lake exe shake --defer which adds to a "defer" key in noshake which acts just like "ignore", and then lake exe shake --defer --fix will apply any deferred fixes

Doesn't this have the same problem, requiring an extra CI pass to get to green? I'm not really concerned about the difference between --fix and --defer: I just don't want to have to think about it so often.

Kinda? The second run would not take an hour, because it would not involve changing mathlib. (It would be a similar level of pain as the "you didn't import everything" linter - you do a standard action and then the CI for the second run quickly catches back up to this point and continues with the rest of the checks.)

We can also try to ensure that this step failing does not prevent later steps from running (and ditto for other lints and tests), since it's better if you can have fewer dialogues with CI

[Mario Carneiro]

Ruben Van de Velde said:

The actual lake exe shake run takes negligible time, as I recall. I think the main argument to keep it per-pr is that letting issues pile up makes them harder to fix

Right. This is my main concern with letting it slip, shake fixes become increasingly incoherent the more you try to fix at once, and there is a lot of time lost if you need to do a second pass since any change to imports will involve a lengthy recompile before you can do fixes to the fixes

[Mario Carneiro]

So a fully automated shake fix run will fail a good portion of the time and require human interaction on a regular basis. That's why my idea is to instead keep the human in the loop but allow authors to use --defer instead of --fix if they are in a hurry, and the next person to run --fix will pick up the slack

[Kim Morrison]

Hmm... I still think --defer is too much work.

Could we try out #12005, and see if it is manageable? I think the failure modes are:

• the failures that get reported at 24 hour intervals are sufficiently more difficult than the every-PR failures
• no one responds to the requests for help from the bot when there are failures
• only I respond :-)

[Mario Carneiro]

well if someone other than me is doing the work, and the work size remains bounded, I don't have objections to setting up an alternative system, at least as a test

[Yaël Dillies]

I agree that there are a bunch of checks that could be run periodically rather than on each CI run. What I'm thinking of is:

• shake
• lean4checker
• everything is imported (actually this one could be run on each bors batch if we knew how to)
• the list of nolints/nostyles is up to date (we lost that automation during the port)

[Yaël Dillies]

Basically any check whose failure can be fixed without possibly having to revert the PR that caused it is eligible to be run periodically rather than on every run (I guess lean4checker has that property only if we trust that mathlib contributors aren't malicious)

[Kim Morrison]

Re: #12005, running shake daily, I think to test it properly we're going to need to remove shake as a standard CI step, introduce an intentional redundant import for shake to remove, and see how it goes.

Can I proceed with that?