Zulip Chat Archive

Stream: mathlib4

Topic: red x

Kevin Buzzard (Sep 01 2023 at 15:40):

Is it a coincidence that since merging #6823 all the commits to mathlib4 master have red x's?

https://github.com/leanprover-community/mathlib4/commits/master

Mario Carneiro (Sep 01 2023 at 15:43):

@Scott Morrison These aren't supposed to fail the build, right?

Mario Carneiro (Sep 01 2023 at 15:43):

although it appears the job is failing because of a permissions error

Johan Commelin (Sep 01 2023 at 15:43):

The problem seems to be that the bot is denied pushing to GH

Mario Carneiro (Sep 01 2023 at 15:45):

leanprover-community-mathlib4-bot does have "maintain" access to the repo

Scott Morrison (Sep 01 2023 at 23:49):

Oops. Sorry, weekend activities here, I won't have a moment to look at this until now+8. I will work it out then, but anyone should feel free to fix or revert if they want to!

Scott Morrison (Sep 02 2023 at 06:58):

Looks like this was fixable merely by modifying permissions on a token. Hopefully future commits to master will get a green tick!

Scott Morrison (Sep 02 2023 at 07:37):

Working now.

Last updated: Dec 20 2023 at 11:08 UTC