!4#1238

Stream: PR reviews

[Jeremy Tan]

@Yaël Dillies are you still working on this forwardport?

[Eric Wieser]

This one is a mess, since the change happened before we were tracking SHAs properly

[Eric Wieser]

I think the thing to do is just port the file from scratch

[Ruben Van de Velde]

!4#3448 ports Algebra.Order.AbsoluteValue from scratch, still needs some fixes. I may have time tonight to look into them, but feel free to pick up if you have time

[Yaël Dillies]

I still think we should fix mathlib because some issues we're encountering with the port are due to bad design there

[Ruben Van de Velde]

Same for !4#3449

[Ruben Van de Velde]

Yaël Dillies said:

I still think we should fix mathlib because some issues we're encountering with the port are due to bad design there

I'm not sure what that means. Do you want to make more changes to mathlib3? That still doesn't mean we should leave this PR in limbo, I think

[Eric Wieser]

I think @Yaël Dillies' point is that there is no point reporting from scratch if we're going to refactor mathlib3 again; it's just a waste of effort to (re-port from scratch + forward-port) vs (re-port from scratch)

[Eric Wieser]

It also seems like there is no reason to expedite bringing this file back in sync

[Yaël Dillies]

I will be busy this weekend, but I shall try to fix it all on Monday

[Jeremy Tan]

Somewhat miraculously !4#3449 now passes CI while re-porting and removing a few porting notes in passing, and is now ready for review

[Eric Wieser]

Not particularly miraculous since !4#3449 doesn't do anything other than tweak formatting and delete porting notes. @Ruben Van de Velde, you might want to check that the commits @Jeremy Tan pushed make sense to you. I suspect we should just throw away the PR unless the porting notes really are now irrelevant.