label after-port

Stream: mathlib4

[Yury G. Kudryashov]

While porting, I notice various APIs/definitions that can be improved. Before the port started, I would procrastinate, then create a PR with a refactor. Now, it is not a good time for refactors but I don't want to forget about these ideas (even if half of them will never be implemented). So, I'm going to create a bunch of issues labeled after-port. Any suggestions/objections?

[Mario Carneiro]

Seems fine to me. Should they be opened against mathlib3 or mathlib4?

[Yury G. Kudryashov]

mathlib4

[Yury G. Kudryashov]

Because after the port, mathlib3 will be frozen.

[Eric Wieser]

Issues can be moved between repos anyway

[Yury G. Kudryashov]

I want to be able to ref. them by numbers and don't loose these refs after the port (also, I'm trying to stop myself from working on the Lean 3 repo).

[Eric Wieser]

I think if you move an issue the old url redirects

[Eric Wieser]

So whatever you pick, the refs won't be lost

[Yury G. Kudryashov]

Anyway, I already created a few of them in the mathlib4 repo.

[Eric Wieser]

On a related note, we should probably go though mathlib 4 and qualify all references to mathlib 3 GitHub issues

[Mario Carneiro]

oh you mean in (ported) comments?

[Mario Carneiro]

probably we should go through mathlib3 and do that; once it gets in mathlib4 it's hard to differentiate from mathlib4 issue references

[Eric Wieser]

Yeah, any occurrence of #NNNN or gh-NNNN in a comment should probably get a mathlib3 prefix

[Johan Commelin]

Except for NNNN = 2003 :wink:

[Eric Wieser]

Mario Carneiro said:

probably we should go through mathlib3 and do that; once it gets in mathlib4 it's hard to differentiate from mathlib4 issue references

We have a rapidly closing window where the numbers are mostly far enough apart to get away with it

[Mario Carneiro]

we should hopefully be qualifying lean4 PR numbers already