awaiting-CI, #bors, and the PR #queue

Stream: general

[Yaël Dillies]

(wanna rename to "awaiting-CI, #bors, and the PR #queue"? :wink:)

[Yaël Dillies]

For the status failure, is there any way to discriminate between between a CI failure and a bors failure? It happened to one of my PRs a while back to be put off the queue after a failed batch which means it subsequently got forgotten as it wasn't showing up on the queue.

[Johan Commelin]

This is indeed frustrating. But I'm not aware of fine-grained control over these failures. It would be good if GH allowed us to do cases on the failure status.

[Scott Morrison]

You can also vote up my issue on the bors repository. :-)

[Johan Commelin]

Until that bors issue is fixed, could we have a tiny github action that overwrites these :cross_mark: generated by bors?

[Bryan Gin-ge Chen]

I'm thinking of adding some steps to the CI to keep "awaiting-CI" updated as well as adding a label "oleans-up-to-date" (naming suggestions welcome) which indicates whether there are up-to-date oleans available via leanproject. Here's what I have in mind:

• when a new CI job starts, remove "oleans-up-to-date"
• when "Build mathlib" succeeds, add a label "oleans-up-to-date"
• when all jobs have finished, remove "awaiting-CI" (here we could also have leanprover-community-bot add "bors r+" to a PR with "ready-for-bors" or another label; the downside is that anyone with push access could add that label and trigger a merge.)

[Eric Rodriguez]

what about "has-oleans"?

[Bryan Gin-ge Chen]

#9491

[Bryan Gin-ge Chen]

Whoops, this is trickier than I thought it would be. The issue is that our CI runs on every pushed commit, whereas labels are associated to a PR and there isn't a 1 to 1 association between commits and PRs. Would it make sense to perform the above-listed actions on all PRs whose branches contain the pushed commit or are there some cases where that's undesirable?

[Ruben Van de Velde]

The has-oleans one should only apply if the commit is the tip of the branch, no?

[Bryan Gin-ge Chen]

Yes, that's right. We have a job which auto-cancels workflows running on out-of-date commits which I think should catch that, although I should think a little bit more about whether there are any weird race conditions.

[Bryan Gin-ge Chen]

OK, I'm stuck on the following. Right now, as long as leanpkg build has started, the job will upload oleans even if the build fails. The proposed behavior would be that "has-oleans" gets applied as well, which I think is reasonable.

Now consider the following sequence of events:

1. Commit 1 is pushed to a branch, triggering build 1
2. Commit 2 gets pushed to the same branch, triggering build 2
3. Build 2 cancels build 1.

Because it takes time for build 1 to get canceled and for it to finish uploading oleans, etc., the following is difficult to avoid:

4. Build 2 removes "has-oleans" from the PR
5. Build 1 uploads oleans and then applies "has-oleans" to the PR

Now the PR "has-oleans", but not up-to-date ones (at least until build 2 uploads its oleans).

[Eric Wieser]

Is has-oleans actually that useful?

[Eric Wieser]

Stale oleans in a leaf file are often just as good as fresh ones

[Scott Morrison]

I think with the recent changes to leanproject get-cache it's no longer so essential to mark has-oleans. (Or, if we do want to mark it, no longer essential that we get it perfectly right!)

[Bryan Gin-ge Chen]

OK, I'll drop has-oleans for now and see if I can get something just to remove awaiting-CI.