PR topics

Stream: general

[Violeta Hernández]

I just noticed that we now have GitHub tags for the topics of PRs. That's a great idea! Kudos to whoever added them.

[Violeta Hernández]

May I suggest t-set-theory or is that too niche?

[Kyle Miller]

As part of the ongoing discussion among maintainers for how to improve the PR process, there were two simple suggestions that seemed good to implement immediately:

1. We're now using the PR assignment feature to record who's responsible for reviewing a PR. Everyone should keep helping by reviewing PRs like before, but this should make it clearer who will do the final sign-off.

2. We're introducing subject area tags to make it easier for reviewers to find relevant PRs. The list of tags is still very much a work in progress, and it seems now is a good time to start brainstorming what the rest of the list might look like. Every label that starts with a t- is a subject area tag.

[Kyle Miller]

I think we're looking to have the tags be coarse as possible so that it's not unwieldy, but fine enough that reviewers can find things to review without navigating a long list of PRs.

[Filippo A. E. Nuccio]

I would have thought that starting with the list of main mathlib folders would have been at the same time coherent and helpful. It now contains 26 folders, namely

• algebra
• algebraic_geometry
• algebraic_topology
• analysis
• category_theory
• combinatorics
• computability
• control
• data
• dynamics
• field_theory
• geometry
• group_theory
• information_theory
• linear_algebra
• logic
• measure_theory
• meta
• model_theory
• number_theory
• order
• probability
• representation_theory
• ring_theory
• set_theory
• topology

If this is too big, I would say that at least 12/14 topics are needed. We could add measure theory and combinatorics. I would also isolate commutative_algebra (or ring_theory) and group_theory from the algebra topic.

[Stuart Presnell]

But wouldn't that be somewhat redundant, because the folder appears in the filename? For example, #15661 "feat(order/filter/basic): add filter.has_basis.bInter_mem" is tagged t-topology not t-order or t-filter.

[Patrick Massot]

About filters specifically, maybe it's time to move them from the order folder to the topology folder. That would be a lot less confusing for many purposes.

[Yaël Dillies]

I was wondering whether they should go under data, actually. Their file structure shares a lot with set and finset.

[Filippo A. E. Nuccio]

Personally, I think that from a mathematical point of view they really have a "topological" flavour and considering them "fundamental data" might be a bit of a stretch.

[Patrick Massot]

Yaël's idea reminded me we also have to get rid of the data folder (or at least remove a lot of stuff from there).

[Chris Hughes]

I never really liked the data folder. It was never clear to me what counted as data.

[Patrick Massot]

Indeed this is one of the reasons why I think we should remove as much as possible from this folder.

[Filippo A. E. Nuccio]

I agree. Things like nat and int might be there, but already real might have its place elsewhere. Or we get rid of it altogether, also a good idea (though I would find it hard to decide where to put the definition of natural numbers...)

[Patrick Massot]

The definition of natural numbers is obviously not in mathlib but in the core library.

[Filippo A. E. Nuccio]

Oh right, it was certainly the bad example. But there are many results about nat in data, I believe. I simply meant to say that there might be things that are so basic that I would have no idea on how to classify them, that's all.

[Michael Stoll]

I'm missing t-number theory in the current label list.

[Heather Macbeth]

@Michael Stoll Just added!

[Heather Macbeth]

By the way, we (maintainers) were thinking that since "number theory" contains quite a lot of different things, maybe we should ask that more advanced number theory PRs be double-tagged t-algebra for algebraic number theory or t-analysis for analytic number theory. What do you think?

[Michael Stoll]

Sounds good.

[Antoine Labelle]

I think t-category-theory could be pertinent too?

[Eric Rodriguez]

I just saw this on reddit: https://www.lloydatkinson.net/posts/2022/automate-pull-request-labels-based-on-changed-files-with-actions/

[Eric Rodriguez]

doing this automatically could be nice!