Zulip Chat Archive

Stream: general

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

Yaël Dillies (Oct 01 2021 at 08:19):

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

Yaël Dillies (Oct 01 2021 at 08:21):

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 (Oct 01 2021 at 08:30):

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 (Oct 01 2021 at 08:45):

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

Johan Commelin (Oct 01 2021 at 08:48):

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 (Oct 01 2021 at 14:37):

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 (Oct 01 2021 at 15:01):

what about "has-oleans"?

Bryan Gin-ge Chen (Oct 01 2021 at 18:53):


Bryan Gin-ge Chen (Oct 01 2021 at 19:07):

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 (Oct 01 2021 at 19:14):

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

Bryan Gin-ge Chen (Oct 01 2021 at 19:19):

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 (Oct 01 2021 at 20:06):

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:

  1. Build 2 removes "has-oleans" from the PR
  2. 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 (Oct 01 2021 at 22:40):

Is has-oleans actually that useful?

Eric Wieser (Oct 01 2021 at 22:46):

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

Scott Morrison (Oct 01 2021 at 23:01):

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 (Oct 01 2021 at 23:30):

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

Last updated: Dec 20 2023 at 11:08 UTC