generating Mathlib.lean

Stream: mathlib4

[Floris van Doorn]

CI uses the script

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

to generate Mathlib.lean. When I do this locally (on Ubuntu 20.04) I get a slightly different ordering for a file whose name is a prefix of another file:
https://github.com/leanprover-community/mathlib4/pull/112/commits/f3acd7729b969036225a3dd7b0147c502d25f3d4
(left is generated by me, right by CI).
Can we make this more reliable?

[Sebastian Ullrich]

You probably need to set the locale for sort as in https://github.com/leanprover/lean4/blob/master/script/update-stage0#L7

[Floris van Doorn]

Thanks! Replacing sort by LC_ALL=C sort indeed gives the same behavior for me.

[Mac]

I'm curious why are you still generating Mathlib.lean since it is no longer necessary to build mathlib?

[Mac]

From what I understood, the whole point of the glob feature @Mario Carneiro requested for Lake was to avoid this file.

[Scott Morrison]

If you point me to how to use the globs I'll switch to using them!