!4#2983 #port-dashboard race condition

Stream: mathlib4

[Eric Wieser]

We've ended up with an unfortunate race condition in this PR. The sequence of things that happened was:

• The PR was not ready to port
• @Yury G. Kudryashov made a PR (#18608) that would make it ready to port
• The port dashboard reads in the latest mathlib3 and declares it ready-to-port
• @Moritz Doll dutifully makes a PR, but mathport still has the old not-ready-to-port version

[Eric Wieser]

I guess the easy solution is to have #port-dashboard perform the dependency analysis on the version mathport was last run on; but then that information will be more stale than it currently is

[Moritz Doll]

In this case it is not a big problem, but generally it might be annoying. Although I don't know whether it is worth the effort to fix this.

[Jireh Loreaux]

I expect that this will be sufficiently rare that we should not go out of our way to fix it.

[Eric Wieser]

Maybe we should just use #port-comments at step 2 to record what's going on in future

[Jeremy Tan]

https://github.com/leanprover-community/mathlib4/actions/runs/4459289886 this workflow for !4#2983 has been building for 4+ hours and yet has not reached a conclusion

[Jeremy Tan]

Somebody needs to stop it manually or we'll hit usage limits

[Eric Wieser]

It's running on servers we own, there are no usage limits relevant here.

[Eric Wieser]

Probably the server finished but lost connection to github and couldn't report it, so I guess it doesn't matter that you hit "cancel".

[Jeremy Tan]

Now what should we do about the non-terminating workflow?

[Jeremy Tan]

never mind, it was terminated

[Jeremy Tan]

image.png Currently the new file hangs on this theorem, at least locally