Print minimal files in import tree in CI

[zeramorphic]

This PR adds a CI step that prints the names of all files in the LeanCamCombi source directory whose list of imports does not contain any import from LeanCamCombi. These files are good candidates to be upstreamed to mathlib.

[zeramorphic]

Sample output:

sky@pop-os:~/code/LeanCamCombi$ grep -r --files-without-match 'import LeanCamCombi' LeanCamCombi
LeanCamCombi/Mathlib/GroupTheory/GroupAction/Defs.lean
LeanCamCombi/Mathlib/Logic/Basic.lean
LeanCamCombi/Mathlib/Logic/Nontrivial/Basic.lean
LeanCamCombi/Mathlib/Logic/Relation.lean
LeanCamCombi/Mathlib/Analysis/Convex/Function.lean
LeanCamCombi/Mathlib/Order/BooleanAlgebra.lean
LeanCamCombi/Mathlib/Order/Closure.lean
LeanCamCombi/Mathlib/Order/Disjoint.lean
LeanCamCombi/Mathlib/Order/Category/BoolAlg.lean
LeanCamCombi/Mathlib/Order/Hom/Set.lean
LeanCamCombi/Mathlib/Order/Hom/Lattice.lean
LeanCamCombi/Mathlib/Order/Birkhoff.lean
LeanCamCombi/Mathlib/Order/RelClasses.lean
LeanCamCombi/Mathlib/Order/Synonym.lean
LeanCamCombi/Mathlib/Algebra/Order/SMul.lean
LeanCamCombi/Mathlib/Algebra/Order/Ring/Defs.lean
LeanCamCombi/Mathlib/Algebra/Order/Module.lean
LeanCamCombi/Mathlib/Algebra/Order/Group/Defs.lean
LeanCamCombi/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
LeanCamCombi/Mathlib/Data/Finset/Lattice.lean
LeanCamCombi/Mathlib/Data/Finset/Pointwise.lean
LeanCamCombi/Mathlib/Data/Finset/Sups.lean
LeanCamCombi/Mathlib/Data/Set/Prod.lean
LeanCamCombi/Mathlib/Data/Set/Image.lean
LeanCamCombi/Mathlib/Data/Nat/Order/Lemmas.lean
LeanCamCombi/Mathlib/Data/Nat/Factors.lean
LeanCamCombi/Mathlib/Data/Fintype/Basic.lean
LeanCamCombi/Mathlib/Data/Sym/Sym2.lean
LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shatter.lean
LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shadow.lean
LeanCamCombi/Mathlib/Combinatorics/Colex.lean
LeanCamCombi/ExampleSheets/Graph/ES1.lean
LeanCamCombi/ExampleSheets/Graph/ES2.lean
LeanCamCombi/DiscreteDeriv.lean
LeanCamCombi/LittlewoodOfford.lean

[YaelDillies]

Very nice! Could that be restricted to files that don't contain sorry? Also everything under Archive (this folder doesn't yet exist) and ExampleSheet is explicitly not something to be upstreamed.

[zeramorphic]

New output is:

LeanCamCombi/Mathlib/Algebra/Order/Group/Defs.lean
LeanCamCombi/Mathlib/Algebra/Order/Ring/Defs.lean
LeanCamCombi/Mathlib/Analysis/Convex/Function.lean
LeanCamCombi/Mathlib/Combinatorics/Colex.lean
LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shadow.lean
LeanCamCombi/Mathlib/Data/Finset/Lattice.lean
LeanCamCombi/Mathlib/Data/Finset/Pointwise.lean
LeanCamCombi/Mathlib/Data/Finset/Sups.lean
LeanCamCombi/Mathlib/Data/Fintype/Basic.lean
LeanCamCombi/Mathlib/Data/Nat/Factors.lean
LeanCamCombi/Mathlib/Data/Nat/Order/Lemmas.lean
LeanCamCombi/Mathlib/Data/Set/Image.lean
LeanCamCombi/Mathlib/Data/Set/Prod.lean
LeanCamCombi/Mathlib/Data/Sym/Sym2.lean
LeanCamCombi/Mathlib/GroupTheory/GroupAction/Defs.lean
LeanCamCombi/Mathlib/Logic/Basic.lean
LeanCamCombi/Mathlib/Logic/Nontrivial/Basic.lean
LeanCamCombi/Mathlib/Logic/Relation.lean
LeanCamCombi/Mathlib/Order/BooleanAlgebra.lean
LeanCamCombi/Mathlib/Order/Category/BoolAlg.lean
LeanCamCombi/Mathlib/Order/Disjoint.lean
LeanCamCombi/Mathlib/Order/Hom/Lattice.lean
LeanCamCombi/Mathlib/Order/Hom/Set.lean
LeanCamCombi/Mathlib/Order/RelClasses.lean
LeanCamCombi/Mathlib/Order/Synonym.lean

[zeramorphic]

I can't yet easily add Archive to the list of search paths - it doesn't exist yet, so grep throws an error. It's easy to add later though.

[zeramorphic]

We now get a file docs/_includes/files_to_upstream.md with content

- [`LeanCamCombi/Mathlib/Algebra/Order/Group/Defs.lean`](https://github.com/YaelDillies/LeanCamCombi/blob/main/LeanCamCombi/Mathlib/Algebra/Order/Group/Defs.lean)
- [`LeanCamCombi/Mathlib/Algebra/Order/Ring/Defs.lean`](https://github.com/YaelDillies/LeanCamCombi/blob/main/LeanCamCombi/Mathlib/Algebra/Order/Ring/Defs.lean)
- [`LeanCamCombi/Mathlib/Analysis/Convex/Function.lean`](https://github.com/YaelDillies/LeanCamCombi/blob/main/LeanCamCombi/Mathlib/Analysis/Convex/Function.lean)
- [`LeanCamCombi/Mathlib/Combinatorics/Colex.lean`](https://github.com/YaelDillies/LeanCamCombi/blob/main/LeanCamCombi/Mathlib/Combinatorics/Colex.lean)
...

I've .gitignored it for now, as it would be a noisy file. It's been added to index.md so it'll display on the landing page for the project - you can then move it where you want it.