coercion from nnrat to nnreal?

Stream: Is there code for X?

[Alex Kontorovich]

Does the coercion from nnrat to nnreal not exist? I looked around a bit and couldn't find it immediately... Is it worthwhile adding it? (Sure, it can be done indirectly, but that gets annoying if there are a lot of such...) Thanks!

[Johan Commelin]

If it doesn't exist, it certainly should be added.

[Johan Commelin]

I think nnrat is relatively new, so I can indeed imagine that the coe doesn't exist yet.

[Yaël Dillies]

I have an open PR for it (#16554), but it got swallowed by the tide. It certainly can be fixed now that it's fully underwater.

[Eric Wieser]

That looks like a rather unpleasant PR to forward-port

[Yaël Dillies]

Why so? The infrastructure is already here in the form of rat.cast, so it's not like there are additional coercion problems to figure out.

[Reid Barton]

Without looking into it in depth, probably the part where it modifies 25 files?

[Reid Barton]

It worries me that this might not be obvious.

[Eric Wieser]

+614 -275

[Eric Wieser]

Although what's relevant is how much of the diff lies in already-ported files

[Yaël Dillies]

Oh most changes will disappear once I've merged master. I opened this PR when the imports were still a tangled mess, so most of the diff is spent fixing them.

[Yaël Dillies]

Good news, #16554 is mostly compiling,modulo a few easy sorries and the guard_exists monoid_hom that @Scott Morrison put in file#algebra/order/field/defs (which I think we'll have to give up on if we don't want to split another 20 files).

[Yaël Dillies]

Bad news is that it touches 33 files

[Reid Barton]

Shall we just close it?

[Eric Wieser]

Are there any auxiliary lemmas (not about the new nnrat.cast) from that PR that could be split to a separate PR? I can't tell which lemmas are new and which are moves.

[Eric Wieser]

Forward-porting a handful of rfl lemmas is totally reasonable IMO, forward-porting a major refactor likely less so

[Eric Wieser]

Things like ulift.up_nat_cast, assuming that's new in that PR

[Yaël Dillies]

Reid Barton said:

Shall we just close it?

I don't see why. We will eventually want nnrat.cast, be it in mathlib or mathlib4 (and indeed Alex wants it now). The work on the mathlib side is mostly done, and most of the work on the mathlib4 side will be done by mathport.

[Reid Barton]

Yaël Dillies said:

most of the work on the mathlib4 side will be done by mathport.

No, most of the work on the mathlib4 side will be done by reviewers

[Yaël Dillies]

As Eric noticed, things can be done incrementally. There are about 4 PRs worth of new content, one or two PRs worth of moving stuff around (about half of which is not ported yet), and then one PR that actually adds nnrat.cast and its API.

[Reid Barton]

Great, so it sounds like this PR can be closed.

[Reid Barton]

And then the subsequent PRs can be judged on their own merits.

[Yaël Dillies]

Yeah well I will just make dependent PRs.

[Yaël Dillies]

No need to close anything.

[Reid Barton]

This sounds like making life harder for everyone.

[Eric Wieser]

Reid Barton said:

No, most of the work on the mathlib4 side will be done by reviewers

For porting new files, reviewers have the ability to ask for a diff with mathport, which massively reduces what they actually have to review. Until we have similar automation for forward-ports, the review load is sadly much higher for forward-ports than it is for first-ports. Using #port-status to compare the mathlib3 diff and mathlib4 diff helps a little, but not enough

[Reid Barton]

It's also just intrinsically more complicated since instead of one thing to consider (the mathlib 3 source) you have three (the old mathlib 3 source, the new mathlib 3 source, the old mathlib 4 source).

[Eric Wieser]

In theory the only change you should have to consider is the change to the mathlib3port source. Unfortunately that contains a bunch of nonsense for ported files that makes a diff tricky