CI for checking files are imported

Stream: mathlib4

[Jireh Loreaux]

To whoever has control over mathlib4 CI (@Scott Morrison , @Mario Carneiro ?): Can we move the "check that all files are imported step" to a separate job like lint style? If I understand correctly this step just consists of: take all files in mathlib and list them in lexicographic order and make sure they match mathlib.lean. That shouldn't require building mathlib first and it would be good to get the feedback right away. Right now build times are short so it isn't a big deal, but it will get annoying later.

[Notification Bot]

A message was moved here from #mathlib4 > port progress by Jireh Loreaux.

[Scott Morrison]

In fact, everyone has control over this, in the sense that it is just a matter of editing .github/workflows/build.yml.in.

[Scott Morrison]

mathlib4#632, not tested yet

[Scott Morrison]

Okay, seems to work.