leanprover-community-bot

Stream: general

[Yaël Dillies]

@leanprover-community-bot seems to be down. It hasn't updated style-exceptions.txt in 3 days now, and it should have given that I've busted some more missing docstrings.

[Johan Commelin]

@maintainers :this:

[Eric Wieser]

What even runs update_nolints.sh any more? This fork of mathlib has a CI script that looks like it should run it, but is very outdated:

[Gabriel Ebner]

It's now in a separate repo (and only run once a day). But according to the logs the nolints have been updated 8 hours ago: https://github.com/leanprover-community/azure-scripts/runs/2918812953?check_suite_focus=true

[Gabriel Ebner]

The reason it wasn't updated was because the nolints branch still existed in the mathlib repo. (The script only creates a PR only if there's no nolints branch to prevent duplicates). I've manually deleted it now: https://github.com/leanprover-community/mathlib/pull/8051

[Yaël Dillies]

@leanprover-community-bot has been down again for a week, it seems.

[Bryan Gin-ge Chen]

The same issue occurred; for some reason the nolints branch was not deleted by bors after #8257 was merged. I've deleted it just now so the job should run again tonight.