[Merged by Bors] - chore(Data/Set): split Finite.lean into `Defs`, `Basic`, `Lemmas` by Vierkantor · Pull Request #18619 · leanprover-community/mathlib4

Vierkantor · 2024-11-04T17:09:50Z

Data.Set.Finite had a lot of imports and in turn was imported often. So let's split it up along import lines:

Data/Finite/Defs.lean now contains the definition of Set.Finite
Data/Set/Finite/Basic.lean knows only Set.Finite and Finset
Data/Finite/Prod.lean now contains finiteness results of products of sets
Data/Fintype/Pi.lean now contains finiteness results of sets of functions
Data/Set/Finite/Lattice.lean contains finiteness results of lattice operations on sets
Data/Set/Finite/List.lean contains finiteness results on lists converted to sets
Data/Set/Finite/Monad.lean also knows about the monad structure on Set
Data/Set/Finite/Powerset.lean contains finiteness results on powersets
Data/Set/Finite/Range.lean contains finiteness results on Set.range
Data/Set/Finite/Lemmas.lean is for lemmas about Set.Finite (and therefore does not contain any Finite instances itself).

github-actions · 2024-11-04T17:10:42Z

PR summary fdb9025585

Import changes exceeding 2%

%	File
+11.28%	`Mathlib.Data.Finite.Defs`
+2.27%	`Mathlib.Data.Fintype.Pi`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.DFinsupp.Defs	510	449	-61 (-11.96%)
Mathlib.Order.Interval.Set.Infinite	510	450	-60 (-11.76%)
Mathlib.Data.MLList.BestFirst	514	455	-59 (-11.48%)
Mathlib.Algebra.Group.FiniteSupport	519	460	-59 (-11.37%)
Mathlib.Data.Finite.Defs	133	148	+15 (+11.28%)
Mathlib.Algebra.Star.Pointwise	573	525	-48 (-8.38%)
Mathlib.Data.Finset.Grade	589	547	-42 (-7.13%)
Mathlib.Combinatorics.SimpleGraph.Basic	516	482	-34 (-6.59%)
Mathlib.Data.Set.Pointwise.Finite	526	492	-34 (-6.46%)
Mathlib.Data.Finsupp.Defs	528	497	-31 (-5.87%)
Mathlib.Data.Fintype.Order	531	500	-31 (-5.84%)
Mathlib.Data.Finset.Preimage	512	484	-28 (-5.47%)
Mathlib.Order.SupClosed	513	487	-26 (-5.07%)
Mathlib.Combinatorics.Hall.Finite	510	485	-25 (-4.90%)
Mathlib.Order.CompleteSublattice	516	493	-23 (-4.46%)
Mathlib.Data.Fintype.Fin	526	503	-23 (-4.37%)
Mathlib.Data.Set.Countable	527	504	-23 (-4.36%)
Mathlib.Order.SuccPred.LinearLocallyFinite	588	564	-24 (-4.08%)
Mathlib.GroupTheory.GroupAction.Basic	576	553	-23 (-3.99%)
Mathlib.Algebra.BigOperators.Group.Finset	526	505	-21 (-3.99%)
Mathlib.Data.Finset.NAry	510	490	-20 (-3.92%)
Mathlib.Data.Finset.Slice	531	511	-20 (-3.77%)
Mathlib.Combinatorics.SetFamily.Shatter	532	512	-20 (-3.76%)
Mathlib.Data.Finset.Interval	595	573	-22 (-3.70%)
Mathlib.Order.Partition.Finpartition	537	518	-19 (-3.54%)
Mathlib.RingTheory.NonUnitalSubsemiring.Basic	588	568	-20 (-3.40%)
Mathlib.Algebra.BigOperators.Ring	564	545	-19 (-3.37%)
Mathlib.Data.Setoid.Partition	538	520	-18 (-3.35%)
Mathlib.Data.Set.MemPartition	510	493	-17 (-3.33%)
Mathlib.Order.Filter.Basic	511	494	-17 (-3.33%)
Mathlib.Order.PartialSups	512	495	-17 (-3.32%)
Mathlib.Algebra.Ring.Subsemiring.Basic	606	586	-20 (-3.30%)
Mathlib.Order.UpperLower.LocallyFinite	523	506	-17 (-3.25%)
Mathlib.Order.Atoms.Finite	529	512	-17 (-3.21%)
Mathlib.Order.ConditionallyCompleteLattice.Finset	512	496	-16 (-3.12%)
Mathlib.Data.Nat.PrimeFin	549	532	-17 (-3.10%)
Mathlib.Algebra.Order.Rearrangement	665	645	-20 (-3.01%)
Mathlib.Algebra.Module.Submodule.Range	616	598	-18 (-2.92%)
Mathlib.Combinatorics.SimpleGraph.Dart	517	502	-15 (-2.90%)
Mathlib.Order.Category.NonemptyFinLinOrd	646	628	-18 (-2.79%)
Mathlib.Order.KonigLemma	594	578	-16 (-2.69%)
Mathlib.Algebra.BigOperators.Finprod	595	579	-16 (-2.69%)
Mathlib.RingTheory.Localization.Defs	684	666	-18 (-2.63%)
Mathlib.Order.Partition.Equipartition	602	587	-15 (-2.49%)
Mathlib.GroupTheory.Perm.ClosureSwap	646	631	-15 (-2.32%)
Mathlib.Combinatorics.SimpleGraph.Maps	519	507	-12 (-2.31%)
Mathlib.Data.Fintype.Pi	441	451	+10 (+2.27%)
Mathlib.GroupTheory.Perm.Sign	672	657	-15 (-2.23%)
Mathlib.Algebra.Group.Pointwise.Finset.Basic	675	666	-9 (-1.33%)
Mathlib.Combinatorics.HalesJewett	534	527	-7 (-1.31%)
Mathlib.Data.Fintype.CardEmbedding	532	526	-6 (-1.13%)
Mathlib.AlgebraicTopology.SplitSimplicialObject	823	814	-9 (-1.09%)
Mathlib.Combinatorics.SimpleGraph.Finite	555	549	-6 (-1.08%)
Mathlib.Order.Filter.AtTopBot	540	535	-5 (-0.93%)
Mathlib.SetTheory.Cardinal.Basic	640	635	-5 (-0.78%)
Mathlib.GroupTheory.GroupAction.Quotient	720	715	-5 (-0.69%)
Mathlib.MeasureTheory.SetAlgebra	548	547	-1 (-0.18%)
Mathlib.LinearAlgebra.Multilinear.Basic	745	744	-1 (-0.13%)
Mathlib.Algebra.Group.ConjFinite	752	751	-1 (-0.13%)

Import changes for all files

Files	Import difference
There are 3087 files with changed transitive imports taking up over 133114 characters: this is too many to display!
You can run `scripts/import_trans_difference.sh all` locally to see the whole output.

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (0.14, 0.00)

Current number	Change	Type
65	-1	large files
220	4	bare open (scoped) Classical

Current commit fdb9025585
Reference commit 6ae3e986f0

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

YaelDillies · 2024-11-04T17:42:56Z

Hmm, Bhavik and I had another plan. I will write more later

Ruben-VandeVelde · 2024-11-07T21:37:31Z

@YaelDillies please do, when you're able:)

YaelDillies · 2024-11-10T13:56:08Z

Sorry for the delay. My wrists feel better today, so here are my thoughts:

Finite and Set.Finite are really close
To fight API getting locally linearised over time, we want to ensure that a local API (eg the Set.Finite API) has as many non-linearisable leaf files as possible.
"Construction files" (eg files about Set.Finite and Prod/Pi/Option, ...) are a perfect example of non-linearisable files (very few interactions exist/are stated between the various possible constructions).

Therefore, Bhavik and I's plan was to/I would suggest you do the following:

Put Finite and Set.Finite in the same file, to make sure the latter doesn't get considered heavier than the former. Concretely, merge Data.Finite.Defs and Data.Set.Finite.Defs.
Make Data.Finite.<Construction> a leaf file locally. Concretely, swap the imports between Data.Finite.<Construction> and Data.Set.Finite.Lemmas. Hopefully, Data.Set.Finite.Lemmas doesn't need existing anymore.

Vierkantor · 2024-11-11T13:25:21Z

Thanks for writing out your suggestions, I'll try them out and see how it goes.

Mathlib/Tactic/Linter/DoubleImports.lean

Vierkantor · 2024-11-13T18:06:33Z

Okay, everything builds so I think this is ready for review again. Does this match your plans somewhat, @YaelDillies? :)

YaelDillies · 2024-11-13T18:23:16Z

Something seems off. Why is this PR adding 600 more lines than it is removing?

YaelDillies

Having gone through the entire diff, it looks like those 600 new lines are all accounted for by the module docs of the new files! 😳

I like the new file structure, but I would still like Finite and Set.Finite to be closer to each other. See below for concrete suggestions.

YaelDillies · 2024-11-13T20:40:16Z

Mathlib/Data/Set/CoeSort.lean

Why are you splitting this off Data.Set.Operations? Should this be a separate PR?

Data.Set.Operations pulls in quite a bit of unneeded imports via Logic.Function.Basic and Mathlib.Data.SProd. But looking at the import graph right now, it doesn't seem quite as hefty as I remembered, so I'm not opposed to dropping the change, or adding it to a separate PR for further debate. What would you prefer?

I thought Data.Set.Operations was supposed to be very light, so I am wary of atomising it even further. Either dropping the change or moving it to a separate PR would be fine

I just dropped the change.

Oh, now there's a build error in Mathlib/Algebra/Group/Int.lean:20:18: Declaration @Set.range is not allowed to be imported by this file.

It is defined in Mathlib.Data.Set.Operations, which is imported by Mathlib.Data.Finite.Defs, which is imported by Mathlib.Algebra.Group.TypeTags, which is imported by Mathlib.Algebra.Group.Even, which is imported by Mathlib.Algebra.Group.Nat, which is imported by this file.

I have reverted the revert of the splitting, and I'll make a new PR for it. (Which this one will need to depend on.)

That assert_not_exists seems... too stringent

True, and I don't like the dependency on the other PR. I think I will drop the assert_not_exists and make a note to readd it in #19031.

Mathlib/Data/Set/Finite/Pi.lean

Mathlib/Data/Set/Finite/Prod.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

This reverts commit 90aa687.

YaelDillies · 2024-11-15T12:22:06Z

Thanks! This looks very good now. The extra 10 imports to Data.Fintype.Pi are actually just very basic tactic files, while the -60 imports to some files is substantial, so this seems to be a net win.

maintainer merge

jcommelin · 2024-11-16T08:26:57Z

Thanks 🎉

bors merge

…8619) `Data.Set.Finite` had a lot of imports and in turn was imported often. So let's split it up along import lines: * `Data/Finite/Defs.lean` now contains the definition of `Set.Finite` * `Data/Set/Finite/Basic.lean` knows only `Set.Finite` and `Finset` * `Data/Finite/Prod.lean` now contains finiteness results of products of sets * `Data/Fintype/Pi.lean` now contains finiteness results of sets of functions * `Data/Set/Finite/Lattice.lean` contains finiteness results of lattice operations on sets * `Data/Set/Finite/List.lean` contains finiteness results on lists converted to sets * `Data/Set/Finite/Monad.lean` also knows about the monad structure on `Set` * `Data/Set/Finite/Powerset.lean` contains finiteness results on powersets * `Data/Set/Finite/Range.lean` contains finiteness results on `Set.range` * `Data/Set/Finite/Lemmas.lean` is for lemmas *about* `Set.Finite` (and therefore does not contain any `Finite` instances itself). Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2024-11-16T09:10:02Z

Pull request successfully merged into master.

Build succeeded:

Although `Data.Set.Operations` is somewhat light-weight, it still pulls in a few imports. In particular, if we want to move the definition of `Set.Finite` to `Data.Finite.Defs`, then `Algebra.Group.Int` will complain that it's not allowed to import `Set.range` from `Data.Set.Operations`; this split will allow us to do the move without removing an `assert_not_exists`. See also this discussion on GitHub: #18619 (comment)

…8619) `Data.Set.Finite` had a lot of imports and in turn was imported often. So let's split it up along import lines: * `Data/Finite/Defs.lean` now contains the definition of `Set.Finite` * `Data/Set/Finite/Basic.lean` knows only `Set.Finite` and `Finset` * `Data/Finite/Prod.lean` now contains finiteness results of products of sets * `Data/Fintype/Pi.lean` now contains finiteness results of sets of functions * `Data/Set/Finite/Lattice.lean` contains finiteness results of lattice operations on sets * `Data/Set/Finite/List.lean` contains finiteness results on lists converted to sets * `Data/Set/Finite/Monad.lean` also knows about the monad structure on `Set` * `Data/Set/Finite/Powerset.lean` contains finiteness results on powersets * `Data/Set/Finite/Range.lean` contains finiteness results on `Set.range` * `Data/Set/Finite/Lemmas.lean` is for lemmas *about* `Set.Finite` (and therefore does not contain any `Finite` instances itself). Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Although `Data.Set.Operations` is somewhat light-weight, it still pulls in a few imports. In particular, if we want to move the definition of `Set.Finite` to `Data.Finite.Defs`, then `Algebra.Group.Int` will complain that it's not allowed to import `Set.range` from `Data.Set.Operations`; this split will allow us to do the move without removing an `assert_not_exists`. See also this discussion on GitHub: #18619 (comment)

Although `Data.Set.Operations` is somewhat light-weight, it still pulls in a few imports. In particular, if we want to move the definition of `Set.Finite` to `Data.Finite.Defs`, then `Algebra.Group.Int` will complain that it's not allowed to import `Set.range` from `Data.Set.Operations`; this split will allow us to do the move without removing an `assert_not_exists`. See also this discussion on GitHub: #18619 (comment) Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Splitting.20docs.23Set.2EinstCoeSortType.20to.20its.20own.20file.3F

Vierkantor added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-data Data (lists, quotients, numbers, etc) labels Nov 4, 2024

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 5, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 5, 2024

Vierkantor force-pushed the split-Data.Set.Finite branch from 1a666e1 to 034a398 Compare November 7, 2024 11:03

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 7, 2024

Vierkantor mentioned this pull request Nov 8, 2024

chore(LinearAlgebra/Finsupp): split Finsupp.lean into many smaller files #18772

Closed

4 tasks

Vierkantor added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 11, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 11, 2024

Vierkantor force-pushed the split-Data.Set.Finite branch 2 times, most recently from 1cf3f03 to 6f234b2 Compare November 13, 2024 14:03

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Nov 13, 2024

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 13, 2024

YaelDillies reviewed Nov 13, 2024

View reviewed changes

Mathlib/Tactic/Linter/DoubleImports.lean Outdated Show resolved Hide resolved

Vierkantor force-pushed the split-Data.Set.Finite branch from e88f9c2 to bf06429 Compare November 13, 2024 15:40

Vierkantor removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 13, 2024

j-loreaux requested a review from YaelDillies November 13, 2024 18:18

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 13, 2024

YaelDillies reviewed Nov 13, 2024

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 13, 2024

Vierkantor force-pushed the split-Data.Set.Finite branch from aabae69 to 825cf38 Compare November 14, 2024 09:30

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 14, 2024

Vierkantor removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 14, 2024

Vierkantor and others added 13 commits November 15, 2024 11:48

shake

61f19e9

Merge Set/Finite/Defs.lean and Finite/Defs.lean

0fe422c

Move the CoeSort instance for Set to its own file

5adea53

Split Data.Set.Finite.Lemmas

65b9136

Shake

fd44aae

Readd required imports

888b59b

More fixing

650c224

Shake and fix

43f598d

Merge Data.Set.Finite.Prod and Data.Finite.Prod

3bf0e49

mk_all

8bb610d

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Revert "Move the CoeSort instance for Set to its own file"

91487cf

This reverts commit 90aa687.

Merge Data.Set.Finite.Pi into Data.Fintype.Pi

26108fe

Drop an assert_not_exists

53e7997

Vierkantor force-pushed the split-Data.Set.Finite branch from 8f0f1d0 to 53e7997 Compare November 15, 2024 10:49

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 15, 2024

useless section

fdb9025

Vierkantor added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 15, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 16, 2024

mathlib-bors bot changed the title ~~chore(Data/Set): split Finite.lean into Defs, Basic, Lemmas~~ [Merged by Bors] - chore(Data/Set): split Finite.lean into Defs, Basic, Lemmas Nov 16, 2024

mathlib-bors bot closed this Nov 16, 2024

mathlib-bors bot deleted the split-Data.Set.Finite branch November 16, 2024 09:10

Conversation

Vierkantor commented Nov 4, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 4, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary fdb9025585

Import changes for modified files

Declarations diff

Uh oh!

YaelDillies commented Nov 4, 2024

Uh oh!

Ruben-VandeVelde commented Nov 7, 2024

Uh oh!

YaelDillies commented Nov 10, 2024

Uh oh!

Vierkantor commented Nov 11, 2024

Uh oh!

Uh oh!

Vierkantor commented Nov 13, 2024

Uh oh!

YaelDillies commented Nov 13, 2024

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

YaelDillies Nov 13, 2024

Choose a reason for hiding this comment

Uh oh!

Vierkantor Nov 14, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Nov 14, 2024

Choose a reason for hiding this comment

Uh oh!

Vierkantor Nov 14, 2024

Choose a reason for hiding this comment

Uh oh!

Vierkantor Nov 14, 2024

Choose a reason for hiding this comment

Uh oh!

Vierkantor Nov 14, 2024

Choose a reason for hiding this comment

Uh oh!

YaelDillies Nov 14, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Vierkantor Nov 14, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

YaelDillies commented Nov 15, 2024

Uh oh!

jcommelin commented Nov 16, 2024

Uh oh!

mathlib-bors bot commented Nov 16, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Vierkantor commented Nov 4, 2024 •

edited

Loading

github-actions bot commented Nov 4, 2024 •

edited

Loading

YaelDillies Nov 14, 2024 •

edited

Loading