Zulip Chat Archive

Stream: general

Topic: PR topics

Violeta Hernández (Jul 24 2022 at 15:51):

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 (Jul 24 2022 at 16:24):

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

Kyle Miller (Jul 25 2022 at 02:15):

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 (Jul 25 2022 at 02:19):

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 (Jul 25 2022 at 08:55):

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

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 (Jul 25 2022 at 09:23):

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 (Jul 25 2022 at 09:24):

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 (Jul 25 2022 at 09:28):

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

Filippo A. E. Nuccio (Jul 25 2022 at 09:29):

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 (Jul 25 2022 at 09:30):

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 (Jul 25 2022 at 10:38):

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

Patrick Massot (Jul 25 2022 at 10:39):

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

Filippo A. E. Nuccio (Jul 25 2022 at 10:42):

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 (Jul 25 2022 at 10:43):

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

Filippo A. E. Nuccio (Jul 25 2022 at 10:50):

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 (Jul 26 2022 at 03:06):

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

Heather Macbeth (Jul 26 2022 at 03:13):

@Michael Stoll Just added!

Heather Macbeth (Jul 26 2022 at 03:15):

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 (Jul 26 2022 at 04:14):

Sounds good.

Antoine Labelle (Jul 26 2022 at 04:50):

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

Eric Rodriguez (Jul 31 2022 at 14:39):

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

Eric Rodriguez (Jul 31 2022 at 14:39):

doing this automatically could be nice!

Last updated: Aug 03 2023 at 10:10 UTC