Zulip Chat Archive
Stream: mathlib4
Topic: mathlib3port not updating
Johan Commelin (Jan 17 2023 at 06:47):
https://github.com/leanprover-community/mathlib3port was last updated 3 days ago
cc @Mario Carneiro @Gabriel Ebner
Johan Commelin (Jan 17 2023 at 06:50):
It seems to be timing out https://github.com/leanprover-community/mathport/actions/runs/3935945845/jobs/6732060407
Johan Commelin (Jan 17 2023 at 06:53):
Running the mathport action used to take about 45mins, then suddenly it bumped to ~2hrs. So I guess it's just being cancelled by the next run, all the time.
Johan Commelin (Jan 17 2023 at 06:54):
Unreachable code has been reached: https://github.com/leanprover-community/mathport/actions/runs/3925923824/jobs/6711163868
Johan Commelin (Jan 17 2023 at 06:55):
And in the end it always seems to crash with
Failed to port { package := "Mathbin", mod3 := `data.polynomial.mirror }
Johan Commelin (Jan 17 2023 at 06:57):
But data.polynomial.mirror hasn't been touched since Nov 25. So it can't be related to a change in that file.
Eric Wieser (Jan 17 2023 at 11:26):
Johan Commelin (Jan 17 2023 at 11:42):
I'm getting old... I had already forgotten about that thread :oops: :see_no_evil:
Gabriel Ebner (Jan 18 2023 at 04:41):
The updates have resumed.
Johan Commelin (Jan 18 2023 at 04:56):
Wow, that's awesome!
Kevin Buzzard (Jan 18 2023 at 08:58):
Thank you!
Last updated: Dec 20 2023 at 11:08 UTC