deprecated.group

Stream: mathlib4

[Winston Yin (尹維晨)]

Should deprecated.group be ported or should attempts be made to actually deprecate it during porting?

[Eric Wieser]

Just port it

[Johan Commelin]

@Winston Yin (尹維晨) Despite the name, the stuff in there isn't actually deprecated. (I know, I'm sorry for the terrible name.)
It should be demoted from a typeclass to a regular structure. But that is a refactor that should not be done during the port.

[Winston Yin (尹維晨)]

Thanks. I ask because it's been the highest not-yet-PR-ed file on the port status page for some time

[Eric Wieser]

I don't think that's a good metric for choosing to port it (edit: #port-status)

[Eric Wieser]

As Kevin has said in the past, looking at the graph and picking something interesting is a better approach

[Johan Commelin]

I think it's a pretty good metric actually. Except for something like course material that is urgently needed and hence bumping certain files higher up the priority queue, I think #port-status is a good approximation in general.

[Chris Hughes]

I think it is deprecated by now last time I checked. I don't think anything in mathlib depends on it

[Yaël Dillies]

import deprecated only appears in deprecated files

[Chris Hughes]

#18066

[Mauricio Collares]

See #13506

[Johan Commelin]

Chris Hughes said:

I think it is deprecated by now last time I checked. I don't think anything in mathlib depends on it

To me, your second sentence doesn't imply the first.

[Winston Yin (尹維晨)]

There is now mathlib4#1368