Uh Oh, build failed

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

Yikes! I approved PR#33, but the build failed. (Should there be a way to tell that a PR will fail build? There is in Mathlib, but I don't see check marks/X's on these PRs?..)

[Alex Kontorovich]

Is there a way to revert to previous commit and kick 33 back out to be fixed by the contributor? (Or maybe someone can quickly figure out what went wrong and fix it?) Thanks!...

[Alex Kontorovich]

It looked good and useful to me, updating the version of Mathlib being used and some reorganization, so I let it through (without much understanding what it was doing...)

[Mario Carneiro]

Alex Kontorovich said:

(Should there be a way to tell that a PR will fail build? There is in Mathlib, but I don't see check marks/X's on these PRs?..)

The reason you don't see X's is because the CI is set to only act on pushes here

[Mario Carneiro]

you want to also run on pull_request

[llllvvuu]

Note that you'll need a different .yml for the PR CI check, which doesn't deploy the website. It should suffice to make a copy and delete everything except https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/.github%2Fworkflows%2Fpush.yml#L88-101 or so. Can also delete all permissions except contents: read

[llllvvuu]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/35

[llllvvuu]

The build issue is because some of my work got merged into mathlib, so the same lemmas here can be deleted. I can do that once I get desktop access

[Chris Henson]

If keeping one CI file is preferable to you, you can also add something like if: github.ref == 'refs/heads/main' to make certain jobs conditional.

[Alex Kontorovich]

Ok thanks. Ian helped me revert to the previous version that built successfully. And he'll change it so that CI runs on PRs, so this doesn't happen again in the future. Thanks for your help!

[milomg]

Oops just saw this conversation, replied here about what the easy fix would be https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/35#issuecomment-1932681180

[Ian Jauslin]

I implemented build checks on pull requests. Will be useful for the future! Thanks everyone!

[milomg]

I believe unless we add a merge queue this PR wouldn't have been caught (because it did pass tests before merging #28)

Reading on merge queues: https://github.blog/2023-07-12-github-merge-queue-is-generally-available/

[Alex Kontorovich]

I think (?) we did just add a merge queue?...

[Alex Kontorovich]

Or perhaps not...? Maybe what I mean is: if I see two PRs, both of which have passed CI, I'll merge one, and wait to check that the other one still passes CI... (?)

[milomg]

This is a pretty rare case that we probably don't need to worry about, but if you want I can create a workflows/merge-queue.yml file

[Ian Jauslin]

@Alex Kontorovich, if you have 2 PR's, you merge one, then relaunch the build test on the second one. The merge queue would automate this procedure. I'd be happy to set that up if this happens too often. Let me know if it seems useful.

[Alex Kontorovich]

It's not an issue yet, so let's not waste your time. But it's good to know that there is a solution, should it become a problem!