[Merged by Bors] - chore(Probability/Kernel/CondCdf): cleanup

[mo271]

• depends on: [Merged by Bors] - feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... #10298

---

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... #10298
  By Dependent Issues (🤖). Happy coding!

[RemyDegenne]

Can you comment on the change of imports? Does that add many files?

[mo271]

Can you comment on the change of imports? Does that add many files?

I replaced import Mathlib.Data.Set.Image with Mathlib.Data.Set.Intervals.Disjoint and sorted the import alphabetically. Not sure how many more files that makes. Is there an easy way to list all imports of a file recursively?

[RemyDegenne]

I asked around how to check imports: lake exe graph --to X --from Y out.pdf can give a view of the imports between files, one you have cache. In this case, it looks like you added almost nothing.

[mo271]

All the imports that are additionally imported recursively due to this change:

https://gist.github.com/mo271/3c31f22eee38698d7bd9113f4f1b4e64

This is much longer than the output of the command you suggested:

lake exe graph --reduce --from Mathlib.Data.Set.Image --to Mathlib.Data.Set.Intervals.Disjoint  diff.svg

which is just this image:

[RemyDegenne]

The command I listed gives only the files between the two files in the command. That's indeed not the same as the files additionally imported.
I don't understand the list you posted. Can you explain the format "Mathlib.Tactic.GuardHypNums" -> "Mathlib.Tactic.Common"; ?

[mo271]

Yeah let me explain, I arrived at the list in the gist with the following commands:

lake exe graph --reduce  --to Mathlib.Data.Set.Image all_image.dot
lake exe graph --reduce  --to Mathlib.Data.Set.Intervals.Disjoint  all_disjoint.dot
sort all_disjoint.dot > all_disjoint.dot.sorted
sort all_image.dot > all_image.dot.sorted
comm -23 all_disjoint.dot.sorted all_image.dot.sorted

So this basically list all additional edges in the import graph

[mo271]

by the way, I think I will propose to add functionality to the ImportGraph package to just get a list of imports as a sorted list instead of the entire graph...

[RemyDegenne]

If I understand correctly, the interesting info in the list you posted is the list of files that appear in the list of edges. Those are the files imported by the new import and not the old one.

But what really interest us is the difference between the list of files imported by the union of all new imports, minus the list of files imported by the union of all old imports. It might be that Mathlib.Data.Set.Intervals.Disjoint imports many more files than Mathlib.Data.Set.Image but those files might be mostly imported by other import lines anyway.

[mo271]

That makes sense, calculating only the new edges by running

lake exe graph --reduce --to Mathlib.Data.Real.Archimedean all.dot

twice once with the new imports in place and once with only the old imports (building lake build Mathlib.Data.Real.Archimedean in between) gives only this diff

  "Mathlib.Data.Set.Intervals.Disjoint" -> "Mathlib.Data.Real.Archimedean";
  "Mathlib.Data.Set.Lattice" -> "Mathlib.Data.Set.Intervals.Disjoint";

So the only extra file seems to be Mathlib.Data.Set.Lattice

[RemyDegenne]

Great! Thanks for investigating the import issue! It would be very nice to get a bot to do that for us on PRs.
bors d+

[mathlib-bors]

✌️ mo271 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mo271]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style