New label "tech debt"

Stream: mathlib4

[Michael Rothgang]

I just went ahead and created a new label "tech debt". I would like to use this to label issues tracking cross-cutting technical debt across mathlib, such as (incomplete and subjective list)

• unimplemented mathlib3 linters
• porting notes
• adaptation notes, if there are issues filed about them
• old mathlib3 names
• nolints that shouldn't stay
• style exceptions
• splitting large files
• removing autoImplicit (to the extent this is wanted)

(Not all of this currently has an issue, and perhaps shouldn't. But labelling the ones there are seems helpful enough.)
I find it useful to get some overview this way. It might also attract people who like fixing such things (such as me :-)).

If you think this is not a good idea, I'd be particularly interested in your opinion :smile:

[Johan Commelin]

I think this is a very good idea. Thanks a lot for starting on this!