Zulip Chat Archive

Stream: general

Topic: leanprover-community-bot

Yaël Dillies (Jun 26 2021 at 09:41):

@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 (Jun 26 2021 at 09:42):

@maintainers :this:

Eric Wieser (Jun 26 2021 at 10:07):

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 (Jun 26 2021 at 10:29):

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 (Jun 26 2021 at 10:30):

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 (Jul 18 2021 at 12:31):

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

Bryan Gin-ge Chen (Jul 18 2021 at 13:13):

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.

Last updated: Dec 20 2023 at 11:08 UTC