Zulip Chat Archive

Stream: mathlib4

Topic: synchronization label bot

Jireh Loreaux (Dec 14 2022 at 16:45):

@Eric Wieser, did the mathlib4 synchronization label bot die? I can't find an open PR (the last one I found that was closed was from last week), and there are now a ton of files that need the label.

Eric Wieser (Dec 14 2022 at 16:46):

Yes, here's the failure: https://github.com/leanprover-community/mathlib/actions/runs/3690518843/jobs/6247604123#step:5:50

Eric Wieser (Dec 14 2022 at 16:47):

It's not happy with the filename that doesn't exist

Eric Wieser (Dec 14 2022 at 16:47):

Should be an easy fix, but I don't have time right now

Eric Wieser (Dec 14 2022 at 16:48):

Removing that line from the port wiki, running the bot, then adding it back would also be enough in the short term

Eric Wieser (Dec 14 2022 at 16:50):

You can run the bot manually from the actions page

Jireh Loreaux (Dec 14 2022 at 17:03):

Thanks, I got it.

Jireh Loreaux (Dec 14 2022 at 17:04):

It's #17943. I've checked it, but I'm just waiting for the current bors batch in mathlib4 to finish.

Jireh Loreaux (Dec 14 2022 at 17:07):

Actually, I got this warning in the check for modifications to ported files:

Base commit: ae193735714ee12590325bff0a20cba1380fd4d4
Head commit: 075f6ac3fa40ccdc03dcf7a5bcc0a0dc0f98e8cf
Error: The head commit for this pull_request event is not ahead of the base commit. Please submit an issue on this action's GitHub repo.

Is this because I asked the bot to re-run the failed job instead of starting a new job?

Jireh Loreaux (Dec 14 2022 at 17:14):

Aha, I guess it's because I made a change to fix something.

Eric Wieser (Dec 14 2022 at 17:26):

That error is fixed by #17936

Eric Wieser (Dec 14 2022 at 17:27):

Aha, I guess it's because I made a change to fix something.

Yes, CI doesn't run on the bot output (there is no need for it to!)

Johan Commelin (Dec 19 2022 at 18:34):

The bot has died again:
https://github.com/leanprover-community/mathlib/actions/runs/3727264113/jobs/6321252042#step:5:54

I haven't yet debugged what went wrong.

Eric Wieser (Dec 19 2022 at 19:02):

The yaml file mentions a mathlib3 file that doesn't exist, and the bot tried to add a comment to it

Reid Barton (Dec 19 2022 at 19:03):

Well, that shouldn't happen any more! Except if it runs at an unlucky time I guess

Eric Wieser (Dec 19 2022 at 19:06):

What happens now when a lean3 file is renamed?

Eric Wieser (Dec 19 2022 at 19:07):

I think probably the way the yaml file is being used is WAI, and the bot is buggy

Reid Barton (Dec 19 2022 at 19:07):

If it hasn't been ported then the "yaml file" (port status wiki page) will automatically get updated with the new module name

Reid Barton (Dec 19 2022 at 19:07):

If it has been ported then probably bad things happen?

Eric Wieser (Dec 19 2022 at 19:08):

As long as the new version doesn't delete the entry about the ported file if the lean3 file goes missing

Reid Barton (Dec 19 2022 at 19:08):

I assume we can agree that renaming already-ported files isn't a good idea

Eric Wieser (Dec 19 2022 at 19:08):

Sure, but race conditions happen, and when they do it's best to have a record of what happened so it can be manually cleaned up

Reid Barton (Dec 19 2022 at 19:09):

The "yaml file" doesn't contain any data that can't be computed from mathlib3 + mathlib4 + the ad-hoc comments page

Reid Barton (Dec 19 2022 at 19:10):

What would happen is that the mathlib4 ported file would refer to a mathlib3 module that no longer exists, probably confusing some tools, but we could fix it by manually adjusting the header

Reid Barton (Dec 19 2022 at 19:10):

and meanwhile the "new" mathlib3 file would appear as unported

Eric Wieser (Dec 19 2022 at 22:38):

Fixed in https://github.com/leanprover-community/mathlib/pull/17978, probably

Eric Wieser (Dec 19 2022 at 22:39):

I can't do a test run of the last commit in the chain for some reason

Eric Wieser (Jan 02 2023 at 20:51):

:ping_pong:

Last updated: Dec 20 2023 at 11:08 UTC