Zulip Chat Archive

Stream: general

Topic: Where to cut this import chain


view this post on Zulip Eric Wieser (Dec 02 2020 at 20:15):

Items at the start of the list are imported by items at the end ofthe list:

['group_theory.perm.basic',
 'data.equiv.mul_add',
 'deprecated.group',
 'algebra.group_power.basic',
 'data.nat.basic',
 'data.nat.factorial',
 'data.list.perm',
 'tactic.wlog',
 'data.fintype.basic']

I want to import data.fintype.basic in group_theory.perm.basic, but I can't right now.

view this post on Zulip Johan Commelin (Dec 02 2020 at 20:20):

Maybe data.fintype.basic is too basic to use wlog?

view this post on Zulip Johan Commelin (Dec 02 2020 at 20:20):

But also wlog seems to have pretty heavy imports... otoh, I understand that it might want to know something about permutations.

view this post on Zulip Johan Commelin (Dec 02 2020 at 20:21):

But having tactic.wlog import all that seems quite much. I wonder if we can minimize something there.

view this post on Zulip Eric Wieser (Dec 02 2020 at 20:21):

Cutting deprecated.group out shouldn't be too hard

view this post on Zulip Eric Wieser (Dec 02 2020 at 20:22):

Although I suspec the cycle reappears somewhere else

view this post on Zulip Reid Barton (Dec 02 2020 at 20:22):

How about just adding a new file

view this post on Zulip Rob Lewis (Dec 02 2020 at 20:23):

wlog is used exactly once in fintype.basic so that would be an easy cut.

view this post on Zulip Rob Lewis (Dec 02 2020 at 20:23):

But also permutations in nat.basic seems a little much, no?

view this post on Zulip Eric Wieser (Dec 02 2020 at 20:30):

I think I'll try swapping the import direction between group_power.basic and deprecated.group

view this post on Zulip Eric Wieser (Dec 02 2020 at 20:37):

#5194

view this post on Zulip Eric Wieser (Dec 03 2020 at 10:33):

Reid Barton said:

How about just adding a new file

This is probably the right move to unblock me, but this import chain looks likely to cause pain in future.

view this post on Zulip Eric Wieser (Dec 03 2020 at 10:35):

For now, the fintype import is in equiv.perm.sign instead, #5201

view this post on Zulip Eric Wieser (Dec 08 2020 at 18:00):

I cut the import of perm.basic from mul_add in #5281 - which was enough to show me that perm.basic is used by fintype.basic directly anyway, making the rest of the import chain irrelevant.


Last updated: May 13 2021 at 16:25 UTC