Zulip Chat Archive
Stream: mathlib4
Topic: source header
Johan Commelin (Dec 20 2022 at 16:08):
group_theory.group_action.opposite is also missing a header. But I need to catch a train
Johan Commelin (Dec 20 2022 at 17:31):
Huh? It does have a source header.
Johan Commelin (Dec 20 2022 at 17:35):
I have no clue why it shows up on #port-status.
Johan Commelin (Dec 20 2022 at 17:47):
Reid spotted the error: module was missing in the header.
Here's a fix: https://github.com/leanprover-community/mathlib4/pull/1127
Patrick Massot (Dec 20 2022 at 17:51):
Was this header written by hand?
Johan Commelin (Dec 20 2022 at 17:55):
Yeah, it was from an older PR
Heather Macbeth (Jan 06 2023 at 21:05):
mathlib4#1052 was merged 6 hours ago but still shows up on #port-status, seemingly because Johan's bot didn't get to it at
https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status
This PR was opened a long time ago (Dec 15) so I wondered if the problem is that it was missing a source header, but it does seem to have one.
@Johan Commelin @Reid Barton any ideas?
Reid Barton (Jan 06 2023 at 21:51):
Maybe because it is listed at https://github.com/leanprover-community/mathlib4/wiki/port-comments?
I don't see anything else wrong off-hand
Heather Macbeth (Jan 06 2023 at 21:51):
I'll try deleting that.
Reid Barton (Jan 06 2023 at 21:52):
looks like that line has been there for at least a few days
Heather Macbeth (Jan 06 2023 at 21:55):
Maybe relevant: this is one of the files which had an ad hoc port.
Reid Barton (Jan 06 2023 at 21:56):
That should probably be okay as long as the source header was added correctly, which it appears to be. If it's still not working tomorrow I'll take a closer look
Heather Macbeth (Jan 06 2023 at 22:06):
Maybe the problem is that
https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status
is not being updated at all. Last time that happened
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port_status.20not.20picking.20up.20a.20PR/near/319317052
the problem was that the script was being run from mathlib4#1108, with associated weirdness.
That PR was merged this morning so maybe there's a broken reference somewhere to the deleted branch port-status-2? @Johan Commelin
Johan Commelin (Jan 07 2023 at 04:54):
I already fixed that problem, by switching to master. The script ran several times yesterday.
Johan Commelin (Jan 07 2023 at 04:54):
This time the problems is that assert commit is not None is triggered on combinatorics.quiver.basic
Johan Commelin (Jan 07 2023 at 04:54):
I do not yet understand why. That file is ported, and has a normal looking source header.
Johan Commelin (Jan 07 2023 at 05:02):
Fixed in mathlib4#1400. There was a spurious space after the commit hash in the source header.
Johan Commelin (Jan 07 2023 at 05:03):
I'm going to make the regex that matches the hash a bit more relaxed.
Johan Commelin (Jan 07 2023 at 05:09):
#port-status is now up to date again
Last updated: Dec 20 2023 at 11:08 UTC