port_status not picking up a PR

Stream: mathlib4

[Frédéric Dupuis]

#port-status is not picking up #1193, probably due to some sort of capitalization issue.

[Shreyas Srinivas]

It has not picked upon mathlib4#1194 either

[Heather Macbeth]

Is it possible that the punctuation in my port-status comment

'note 23 Dec: don't start this until mathport has run again'

broke it? I will edit just in case.

[Reid Barton]

Yes this was the problem (the single quote within single quotes was invalid yaml). I guess the comments aren't completely free-form...
In fact, you shouldn't need quotes around the comment at all in most cases.

[Heather Macbeth]

Is #port-status frozen again? Looks like @Johan Commelin's half-hourly auto-updates to the wiki haven't run for the last three hours:
https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status

[Johan Commelin]

Yup, something broke. I'm running a script from mathlib4#1108. My server tries to rebase that PR on top of master, but the PR now has a conflict. It would be good to get that PR merged.

[Johan Commelin]

I fixed the merge conflict on the PR.

[Eric Wieser]

I think it might be worth putting all these scripts in a new mathlib-port-status repo

[Eric Wieser]

There's no real point going through bors with them, is there?

[Reid Barton]

That seems reasonable to me

[Reid Barton]

I guess one question is how convenient we want to make it for people to run the scripts manually

[Reid Barton]

I've been sort of assuming that people mostly aren't doing that, and instead just look at Johan's page.

[Henrik Böving]

Can confirm that's what I am doing

[Eric Wieser]

It also means we can drop the external server and run the script directly from github actions ,and host the page at leanprover-community.github.io/mathlib-port-status

[Eric Wieser]

(I'm happy to look into that once the scripts are there)