is the bot dead

Stream: triage

[Johan Commelin]

The bot seems dead...

[Bryan Gin-ge Chen]

It seems to be sleeping because we haven't touched the repo in a while: https://github.com/leanprover-community/azure-scripts/actions/workflows/random_issue.yml

BTW did we want to switch to mathlib4 issues / PRs? https://github.com/leanprover-community/azure-scripts/pull/14

[Bryan Gin-ge Chen]

I've gone ahead and re-enabled all the workflows in the repo. However, it seems that the "Delete old archives from Azure" job has been failing for a while:

https://github.com/leanprover-community/azure-scripts/actions/runs/6031893893

Maybe we changed an API key without updating the secret?

[Bryan Gin-ge Chen]

@Scott Morrison Sorry! I realized the bot still wasn't fully updated, so I made some more fixes: https://github.com/leanprover-community/azure-scripts/pull/16 :pray:

[Scott Carnahan]

It's been more than a month since the last bot post. Who should we call?

[Eric Wieser]

I have power to fix this, but not today

[Bryan Gin-ge Chen]

I think I touched the bot last so I’ll take a look now

[Bryan Gin-ge Chen]

Ah, as expected the workflow was disabled due to lack of activity in the repo. I've re-enabled it, so we should be good for another 60 days or so...