Order.GaloisConnection

Stream: mathlib4

[Patrick Massot]

I opened mathlib4#1093 to port order.galois_connection but it isn't actually usable yet because mathlib3port doesn't have Order.CompleteLattice so names do not match yet. Does anyone understand when mathlib3port will catch up?

[Patrick Massot]

I give up trying to use OneShot to fix this. I'm simply trying random things and going from one incomprehensible error to the next one.

[Kevin Buzzard]

The last time I checked (a week or two ago) my conclusion was that it runs every day late afternoon UK time (about 4pm) so maybe 5pm your time?

[Reid Barton]

It runs twice a day now but indeed at 5 am / 5 pm CEST, and finishes about an hour later

[Patrick Massot]

In the mean time @Frédéric Dupuis opened a competing PR in mathlib4#1099 without waiting for mathport to do its job. Frédéric, did you do the alignment by hand (which would be a huge waste of time) or did you find a way to use make oneshot?

[Patrick Massot]

Note that his PR also has a worrying comment about super slow elaboration. Do we now have more tool to investigate this?

[Kevin Buzzard]

Is order_dual a structure yet? This might fix things. It cannot be a type synonym in lean 4 unless we want to go back to the bad old days of leakage, because it is not possible in lean 4 to retrospectively make the declaration irreducible. I need to do two hours of admin right now but I can start on the refactor this afternoon assuming it's not already been done. Note that I made MulOpposite a structure in mathlib4#1036 -- reviews welcome!

[Kevin Buzzard]

I know we're not supposed to be refactoring as we go along but this is one case where the inability to port directly (because we can't make the definitions irreducible) somewhat forces our hand. The refactor of MulOpposite was surprisingly painless.

[Eric Wieser]

It cannot be a type synonym in lean 4 unless we want to go back to the bad old days of leakage,

Does leakage matter for porting? We're not writing any new code, so if the mathlib3 version didn't leak then the mathlib4 version shouldn't either

[Eric Wieser]

AFAIK, the only purposes of irreducible in Lean 3 are 1) sanity checks and 2) performance optimizations; both of which could be postponed till after the port.

[Eric Wieser]

If lean 4 is still seeing through the type synonym in places Lean 3 didn't, do we have a bug filed / confirmation of whether the change is deliberate?

[Kevin Buzzard]

Yes, things are breaking, for example in GroupTheory.GroupAction.Defs there's currently a porting note "was one liner" and it goes back to a one-liner after the change. What motivated me was the inability to port the line attribute [irreducible] MulOpposite -- in some sense the PR is a port of that line. But if we don't want it now, we can wait. Because of defeq eta for structures it shouldn't be a painful refactor, whenever it happens.

[Anatole Dedecker]

Patrick Massot said:

In the mean time Frédéric Dupuis opened a competing PR in mathlib4#1099 without waiting for mathport to do its job. Frédéric, did you do the alignment by hand (which would be a huge waste of time) or did you find a way to use make oneshot?

Looks like too much people wanted to port that file :stuck_out_tongue_wink:

[Anatole Dedecker]

Patrick Massot said:

Note that his PR also has a worrying comment about super slow elaboration. Do we now have more tool to investigate this?

I have the same problem in Order.CompleteBooleanAlgebra (will open PR soon). There is a simple but disappointing solution: use @ to tell Lean you want to apply the lemma to α and not αᵒᵈ...

[Frédéric Dupuis]

Sorry, I was not aware of the already open PR for this file, I just picked an available file from the port status page and started working! Yes, I did the alignment by hand, it actually wasn't that bad.

[Frédéric Dupuis]

OrderDual is still a type synonym and not a structure, which makes me even more confused about the elaboration problems. It really behaved as if converting between α and αᵒᵈ had to be done explicitly using ofDual and toDual but maybe I misinterpreted what was going on.

[Anatole Dedecker]

Also, the last commit to the mathport repo didn't seem to fix the alignments either (so I did the alignment by hand in CompleteBooleanAlgebra too, and can confirm it is not that bad)

[Kevin Buzzard]

All that seems to be happening with this type synonym thing is simply that Lean 4 elaborates in a different way to Lean 3, and we're all used to the Lean 3 way of doing it so when that fails we are confused.

[Eric Wieser]

Combined with the fact that we skipped out on lots of ofDual and toDuals in lean3 proofs, because the rule was roughly "do things right in the statement, but anything goes if the proof goes through"

[Heather Macbeth]

Frédéric Dupuis said:

It really behaved as if converting between α and αᵒᵈ had to be done explicitly using ofDual and toDual but maybe I misinterpreted what was going on.

@Frédéric Dupuis By the way, I did some minimization a couple of weeks ago about issues with type synonyms:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Type.20synonyms
Do you think this is the same issue?

[Frédéric Dupuis]

It's similar, but here providing extra information doesn't completely solve the problem, we are still left with performance issues.

[Frédéric Dupuis]

Here I think the elaborator is struggling to figure out that αᵒᵈᵒᵈ is the same as α.

[Patrick Massot]

Frédéric Dupuis said:

Sorry, I was not aware of the already open PR for this file, I just picked an available file from the port status page and started working! Yes, I did the alignment by hand, it actually wasn't that bad.

You missed three sources of information: this zulip thread, the list of opened PRs and the yaml-wiki file, so I'm really curious to know what you did to check before starting. That being said there was no real duplication of work since I stopped as soon as I realized mathport wasn't doing its job;

[Patrick Massot]

Anatole Dedecker said:

Also, the last commit to the mathport repo didn't seem to fix the alignments either (so I did the alignment by hand in CompleteBooleanAlgebra too, and can confirm it is not that bad)

@Mario Carneiro this thread is a mess mixing at least three different conversations, but that one is for you. It seems mathport doesn't pick up alignments instructions.

[Frédéric Dupuis]

Patrick Massot said:

Frédéric Dupuis said:

Sorry, I was not aware of the already open PR for this file, I just picked an available file from the port status page and started working! Yes, I did the alignment by hand, it actually wasn't that bad.

You missed three sources of information: this zulip thread, the list of opened PRs and the yaml-wiki file, so I'm really curious to know what you did to check before starting. That being said there was no real duplication of work since I stopped as soon as I realized mathport wasn't doing its job;

I checked Johan's port status page to pick something to work on, and this file was still listed as "No" on this page when I started working on it. I didn't double-check anywhere else though.

[Reid Barton]

"No" just means that the file has not been fully ported yet

[Frédéric Dupuis]

I meant it was listed as "No" with no mathlib4 PR next to it.

[Reid Barton]

Ah

[Anatole Dedecker]

I think Johan’s page is only updated once a day, right ?

[Johan Commelin]

every hour

[Johan Commelin]

I can increase, if wanted

[Reid Barton]

But also the link to "this page" doesn't go to Johan's port status page.

[Johan Commelin]

It now runs every 30 mins

[Johan Commelin]

10 mod 30, actually.

[Johan Commelin]

https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status is now also updated every 30 mins, from my server.

[Johan Commelin]

We can do that from github CI in the future

[Frédéric Dupuis]

My understanding is that the link goes to what Johan's page is generated from, no? So I checked it hadn't been updated in the meantime when I added my PR there.

[Anatole Dedecker]

Yes sorry I misunderstood

[Mario Carneiro]

Patrick Massot said:

Anatole Dedecker said:

Also, the last commit to the mathport repo didn't seem to fix the alignments either (so I did the alignment by hand in CompleteBooleanAlgebra too, and can confirm it is not that bad)

Mario Carneiro this thread is a mess mixing at least three different conversations, but that one is for you. It seems mathport doesn't pick up alignments instructions.

Is there an issue being reported here? You all seem to be working in some shared context but I can't make heads or tails of it. MWE please?

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib4/pull/1099/files#r1051747996

[Mario Carneiro]

I'm still not seeing the mathport issue

[Kevin Buzzard]

oh there are several conversations happening at once :-(

[Anatole Dedecker]

Sorry for the delay. Actually I misinterpreted the problem, it just seems that the mathlib3port repo hasn't catched up with the state of mathlib4. What is the process for that?