Zulip Chat Archive
Stream: mathlib4
Topic: !4#3068
Jeremy Tan (Mar 24 2023 at 03:50):
!4#3068 your turn on this one, @Eric Wieser
Eric Wieser (Mar 24 2023 at 08:55):
It doesn't look like you followed the porting comments there
Eric Wieser (Mar 24 2023 at 09:12):
port-status#algebra/monoid_algebra/division
Eric Wieser (Mar 24 2023 at 09:17):
Notably, the version you ported is out of date; although I'm not sure why the page I link above doesn't say that
Jeremy Tan (Mar 24 2023 at 10:50):
Eric Wieser said:
It doesn't look like you followed the porting comments there
I did follow the porting comments
Eric Wieser (Mar 24 2023 at 10:50):
The comment says
please wait for mathlib#18633 to be through mathport
Jeremy Tan (Mar 24 2023 at 10:50):
It was through mathport already
Jeremy Tan (Mar 24 2023 at 10:51):
Now let's fix the deterministic timeouts
Eric Wieser (Mar 24 2023 at 10:51):
Jeremy Tan said:
It was through mathport already
Mathport runs at about midnight UTC, PR #18633 was merged at 1:43AM UTC
Eric Wieser (Mar 24 2023 at 10:54):
Unfortunately #port-dashboard has crashed (or rather, the script producing the data source it consumes has) so it's showing you stale information from 17 hours ago
Jeremy Tan (Mar 24 2023 at 10:55):
You probably need to change the schedule at which mathport runs, so that every time a PR gets merged on the mathlib3 side it runs
Jeremy Tan (Mar 24 2023 at 10:58):
To a first approximation, that is. The new schedule will wait for 2 hours after a PR is merged. If no new PRs are merged during that time, Mathport runs
Jeremy Tan (Mar 24 2023 at 11:06):
@Eric Wieser how do you know the script feeding #port-dashboard crashed?
Eric Wieser (Mar 24 2023 at 11:08):
Jeremy Tan said:
You probably need to change the schedule at which mathport runs, so that every time a PR gets merged on the mathlib3 side it runs
mathport takes more than 3 hours to run, so that wouldn't have helped here anyway
Eric Wieser (Mar 24 2023 at 11:09):
Jeremy Tan said:
Eric Wieser how do you know the script feeding #port-dashboard crashed?
I looked at #port-wiki (linked from https://github.com/leanprover-community/mathlib-port-status#architecture), and saw that it hasn't been updated for a while
Jeremy Tan (Mar 24 2023 at 11:12):
Surely mathport only needs to consider changed files rather than rerunning it on all files at every run?
Jeremy Tan (Mar 24 2023 at 14:43):
Who can make #port-status work again?
Eric Wieser (Mar 24 2023 at 14:51):
Johan Commelin is the person who runs the script. I sent them a PM earlier today.
Johan Commelin (Mar 24 2023 at 14:59):
Hmm, my server seems to be down.
Johan Commelin (Mar 24 2023 at 14:59):
I'll look into it tonight, when I'm back home.
Johan Commelin (Mar 24 2023 at 14:59):
Ooh no! Probably it is because the RSA key change on github
Johan Commelin (Mar 24 2023 at 15:00):
so git pull on my server is now failing
Johan Commelin (Mar 24 2023 at 15:01):
I'll try to fix it tonight
Oliver Nash (Mar 24 2023 at 15:37):
This hiccup emphasises to me how great #port-status is and, correspondingly, how grateful I am to the author @Eric Wieser and the distributor @Johan Commelin . Thanks guys!
Johan Commelin (Mar 24 2023 at 18:18):
I've updated the github key. Hopefully things start working again.
Eric Wieser (Mar 24 2023 at 19:02):
Looks to be live again!
Eric Wieser (Mar 24 2023 at 19:03):
Eric Wieser said:
Eric Wieser said:
Notably, the version you ported is out of date; although I'm not sure why the page I link above doesn't say that
The page now does say that, so everything is working as intended.
Last updated: Dec 20 2023 at 11:08 UTC