Zulip Chat Archive

Stream: PR reviews

Topic: group_theory/subgroup/basic reduction #17862


Ruben Van de Velde (Jan 19 2023 at 13:31):

Does anyone want to review this before the rising tide engulfs it (maybe 10 PRs or so away)?

Eric Wieser (Jan 19 2023 at 13:35):

13 unported files and 2 in progress PRs away, according to https://leanprover-community.github.io/mathlib-port-status/

Ruben Van de Velde (Jan 19 2023 at 13:37):

Oh, cool page

Riccardo Brasca (Jan 19 2023 at 13:48):

I will have a look later today

Riccardo Brasca (Jan 19 2023 at 15:13):

Can you explain a little bit why this splitting is useful? I am not against it, it's just to be sure to understand the purpose of the PR.

Ruben Van de Velde (Jan 19 2023 at 15:25):

Just that the file is huge - top 5 of biggest files in mathlib, IIRC - and this seemed like a reasonable way to start doing something about it. "this is not worth it" would be a fine review too, as far as I'm concerned :)

Riccardo Brasca (Jan 19 2023 at 15:30):

Ah, I didn't notice is so big!

Riccardo Brasca (Jan 19 2023 at 15:32):

Wow, it's more than 3000 lines. Let's split it then.

Riccardo Brasca (Jan 19 2023 at 15:32):

Delegated. There is a line that I think has been forgotten.

Ruben Van de Velde (Jan 19 2023 at 15:58):

@Riccardo Brasca thanks - could you clarify your comment? I moved the description to src/group_theory/subgroup/simple.lean, though no longer as a bullet point

Riccardo Brasca (Jan 19 2023 at 15:59):

Exactly, I mean you could add a "main definition" section to that file.

Ruben Van de Velde (Jan 19 2023 at 16:15):

Done, thanks. I merged master for good measure, will put it on the queue when CI comes back


Last updated: Dec 20 2023 at 11:08 UTC