Topic: import order
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?
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
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.)
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?
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