Removing unnecessary uses of `PartENat`

Stream: mathlib4

[Kim Morrison]

I'd be pretty happy to see the end of PartENat (I appreciate there is some difference regarding computability, but I think this is irrelevant for the places in Mathlib that currently use it).

[Kim Morrison]

I had a quick look at Mathlib.RingTheory.PowerSeries, one of the few places still using it. It's clear that one can switch out PartENat for ENat there --- the branch#powerseries_enat is partial progress, and just needs some proof repair: everything downstream works.

[Kim Morrison]

If anyone would like to adopt that, that would be lovely. :-)

[Kim Morrison]

Otherwise, hopefully #19624 goes a long way to reducing our use of PartENat, by introducing ENat.card, and switching over Set.encard to use it (+ some cleanup elsewhere).

[Kim Morrison]

In fact, it looks like we can just deprecate PartENat.card at the same time.

[Kim Morrison]

#19622 completes the removal of PartENat from PowerSeries.

[Kim Morrison]

and the followup #19648 finishes the deprecation of PartENat.card, incidentally giving some substantial import reductions elsewhere.

[Eric Wieser]

I guess your plan is to land the first just before the 1.14 release, and the second just after?

[Kim Morrison]

I think both can go in now, can't they?

[Eric Wieser]

I though deprecations were supposed to stick around for at least one non-rc release

[Eric Wieser]

Otherwise a user bumping only through releases one at a time will never see the warning

[Kim Morrison]

All the deprecations are sticking around?

[Kim Morrison]

Oh, you don't like that I've moved the deprecations into Deprecated.

[Kim Morrison]

Okay, let's wait for #19648 for at least a few days then.

[Eric Wieser]

Oh, your PR title confused me

[Eric Wieser]

But I didn't think the Deprecated folder was part of our deprecation process, since that still breaks everyone who doesn't import it

[Kim Morrison]

Yes, I moved things to Deprecated specifically in order to be able to avoid importing these files, as it significantly untangles the import graph in this case.

[Kim Morrison]

I really don't want to wait 6 months for these import reductions.

[Johan Commelin]

Eric Wieser said:

But I didn't think the Deprecated folder was part of our deprecation process, since that still breaks everyone who doesn't import it

I don't think that there are many downstream projects affected by this move. And if so, it's nothing a grep can't solve. We regularly move lemmas between files (or split them), and people have to deal with the fallout. I don't think this is any worse.

[Eric Wieser]

Kim Morrison said:

I really don't want to wait 6 months for these import reductions.

I think we can speed up any deprecation to a single release if it makes things easier; so the worst case should be only one month, assuming Lean keeps up its release cadence (and if it doesn't, mathlib can always set its own tagging cadence in future)

[Ruben Van de Velde]

Or throw import Mathlib at it

[Eric Wieser]

grep isn't reliable in the face of to_additive

[Eric Wieser]

Ruben Van de Velde said:

Or throw import Mathlib at it

It would be great if we could document this somewhere as a migration recommendation for people running lake update Mathlib

[Eric Wieser]

(though it would be even better if Lean could look at the ileans of all dependencies and suggest imports when you reference a name that doesn't exist!)

[Kim Morrison]

Eric Wieser said:

(though it would be even better if Lean could look at the ileans of all dependencies and suggest imports when you reference a name that doesn't exist!)

@Marc Huisinga, is there any possibility of doing this? Somehow giving extra hints in VSCode to the user about names that don't exist, but would with further imports?

[Kim Morrison]

Eric Wieser said:

Ruben Van de Velde said:

Or throw import Mathlib at it

It would be great if we could document this somewhere as a migration recommendation for people running lake update Mathlib

I have added a section at https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

[Kim Morrison]

(both suggesting import Mathlib, and explaining how to incrementally bump through intermediate tagged releases)

[Johan Commelin]

Thanks! I've kicked it on the queue now.

[Marc Huisinga]

Kim Morrison said:

Eric Wieser said:

(though it would be even better if Lean could look at the ileans of all dependencies and suggest imports when you reference a name that doesn't exist!)

Marc Huisinga, is there any possibility of doing this? Somehow giving extra hints in VSCode to the user about names that don't exist, but would with further imports?

This is planned for next quarter, though it's a bit more complicated than what Eric suggests.