Zulip Chat Archive

Stream: general

Topic: import order


view this post on Zulip Reid Barton (Apr 23 2020 at 16:00):

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?

view this post on Zulip Mario Carneiro (Apr 23 2020 at 16:05):

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

view this post on Zulip Gabriel Ebner (Apr 23 2020 at 17:30):

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.)

view this post on Zulip Yury G. Kudryashov (Apr 23 2020 at 17:31):

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

view this post on Zulip Gabriel Ebner (Apr 23 2020 at 17:33):

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.


Last updated: May 17 2021 at 22:15 UTC