mathport lag

Stream: mathlib4

[Patrick Massot]

Mario Carneiro said:

I'm still not seeing the mathport issue

Let's try to untangle this from the other conversation from the original thread. The mathport issue is that the file Order/GaloisConnection in mathlib3port is still full of suprand infi at this time, despite the fact that mathlib4 has had relevant align for a while.

[Anatole Dedecker]

The problem comes even sooner: the file Order/CompleteLattice in mathlib3port is still the autoported one (which explains why mathport doesn't know about the new #aligns)

[Mario Carneiro]

so this is a CI problem? From that second file it is clear that mathport does not have an alignment here

[Gabriel Ebner]

For mathport to pick up any mathlib4 updates, you need to update the mathlib4 version in mathport.

[Gabriel Ebner]

Currently mathport depends on a five day old version of mathlib4.

[Patrick Massot]

Ok, so this is definitely a CI issue: why isn't CI updating mathport to the latest mathlib4?

[Gabriel Ebner]

Because it used to be the case that every mathlib4 update broke mathport and you had to fix things manually. It's only very recently that mathlib4 has started growing glinntheory files (which don't break mathport).

[Patrick Massot]

Can we have CI that tries to update but pushed only when things aren't broken?

[Gabriel Ebner]

CI is now updating mathport to the latest mathlib4 twice a day.