import order

Stream: general

[Reid Barton]

Mario Carneiro said:

(modulo quirks where import order matters)

Does this really happen? Is it something like: we toss all the simp lemmas that are transitively imported into some data structure, and then the order simp tries them can depend on the order they were inserted?

[Mario Carneiro]

That sounds right. Similarly with instances, as well as def_replacer, which maintains exactly one definition with an attribute by removing the attribute from whatever had it previously

[Gabriel Ebner]

This actually happened a few weeks ago, where the simp_nf linter suddenly failed after a merge to master: #2291 (The mk_all.sh script generates import statements in a nondeterministic way, making this particularly interesting to debug.)

[Yury G. Kudryashov]

Should we replace mk_all with a leanproject command that will use, e.g., alphabetical order?

[Gabriel Ebner]

Personally, I would prefer if mk_all.sh would generate just a single file with a few hundred imports (in alphabetical order). The current setup takes forever to compile.
So far we've tried to keep leanproject out of the CI setup, but I'm not opposed to change that. The mk_all.sh script is tiny though.