Zulip Chat Archive

Stream: mathlib4

Topic: mathlib4#588


Jireh Loreaux (Nov 21 2022 at 19:30):

Can someone review mathlib4#588? It's now at the top of the list of files which unlock the most stuff. I co-authored it with Anatole, so I shouldn't review it.

Eric Rodriguez (Nov 21 2022 at 23:26):

there's still a lot of s in the #aligns - I thought this wasn't wanted?

Jireh Loreaux (Nov 21 2022 at 23:47):

I can add notes for these, but the first three are just orders of implicit arguments (actually the third one might also be that Seq.seq and has_seq.seq have different types, but this is known and expected). If you look at the translation error for Sum.bind it seems that mathport got it wrong, it shouldn't be dubious. If you want to look at the dubious translation errors, see commit: 41b163554e4c5dca5ea9e09b27ef475cafe61606

Eric Rodriguez (Nov 21 2022 at 23:49):

sorry, I'm still new to the porting process; so should these be left in if the aligns are still mildly dubious? I thought they were autogenerated by mathport and were meant to be all taken out before the file was "ported"

Jireh Loreaux (Nov 21 2022 at 23:52):

No, the purpose of the is to indicate that the type of the mathlib3 version and the mathlib4 version don't match. This is just a marker for mathport so that in future references to this declaration it knows to use the mathlib4 type. I don't think the is ever added automatically by mathport (I could be wrong here), it just suggest to the user to use it.

Jireh Loreaux (Nov 21 2022 at 23:54):

So, the should stay in when the translation is dubious, but it's good to indicate for future reference why it was marked as dubious (this requires human assessment).

Eric Rodriguez (Nov 21 2022 at 23:59):

I see! I think it'd be good to add the explanations in.

Scott Morrison (Nov 22 2022 at 00:00):

Yeah, I think that every \_x that gets left in should probably have a comment.

Scott Morrison (Nov 22 2022 at 00:01):

(and if mathport reports a dubious translation, but it actually looks okay, just remove the \_x.)

Jireh Loreaux (Nov 22 2022 at 00:02):

I had added comments, but I need to be done for the evening.


Last updated: Dec 20 2023 at 11:08 UTC