Zulip Chat Archive

Stream: maths

Topic: circular imports in mathlib

view this post on Zulip Kevin Buzzard (Oct 02 2018 at 13:58):

Johannes said in the p-adic PR

I'm fine with merging, with one exception: Please don't import topology in data/polynomial. I guess we need a analysis/polynomial.lean for the continuity statement.

I don't like this, as we get into a huge mess if we have too much cyclic dependencies between the top level directories. I think data shouldn't depend on analysis or the *_theory directories.

I've never thought about these issues. Are there general rules written down somewhere about what is acceptable and what is not when it comes to this sort of question?

Last updated: May 18 2021 at 07:19 UTC