Check that all files are imported

Stream: mathlib4

[Riccardo Brasca]

What does the "Check that all files are imported" stage of CI? in mathlib4#615 I get the following error at that stage

Run git diff --exit-code
diff --git a/Mathlib.lean b/Mathlib.lean
index ca7bf7d..f2b63a3 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -15,6 +15,7 @@ import Mathlib.Algebra.Order.Group
 import Mathlib.Algebra.Order.Monoid
 import Mathlib.Algebra.Order.MonoidLemmas
 import Mathlib.Algebra.Order.Ring
+import Mathlib.Algebra.PemptyInstances
 import Mathlib.Algebra.Ring.Basic
 import Mathlib.CategoryTheory.ConcreteCategory.Bundled
 import Mathlib.Control.Random
Error: Process completed with exit code 1.

[Jon Eugster]

Mathlib.lean is meant to import all files of Mathlib, so you want to add your newly ported file there.

[Riccardo Brasca]

Thanks! We should add this to the wiki

[Patrick Massot]

Riccardo, you should always feel free to add information to this wiki page.

[Riccardo Brasca]

I am doing it, but are we really supposed to add the new file by hand or do we have a script for that?

[Scott Morrison]

I've been doing it by hand (when CI reminds me to do it...)

[Scott Morrison]

.github/workflows/build.yml says:

find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

[Scott Morrison]

Also, your file should be called PEmptyInstances.