AkraBazzi not allowed to import measure theory

Stream: mathlib4

[Thomas Browning]

The directory dependency linter prevents files in Computability from importing files in MeasureTheory. In particular, the file Computability.AkraBazzi.AkraBazzi is not allowed to import any measure theory. But I'm running into problems on #34456 where the reasonable looking import of Analysis.Meromorphic.Basic into Analysis.SpecialFunctions.Complex.LogDeriv is resulting in a problem via the following chain:
MeasureTheory.Constructions.BorelSpace.Basic -> Analysis.Meromorphic.Basic -> Analysis.SpecialFunctions.Complex.LogDeriv -> Analysis.SpecialFunctions.Pow.Deriv -> Computability.AkraBazzi.AkraBazzi.

Any thoughts on what should be done here?

[Yaël Dillies]

Can the final import be made private?

[Thomas Browning]

Yes, but that doesn't appease the linter

[Yaël Dillies]

Then probably the linter should be fixed!

[Yaël Dillies]

We developed a lot of tooling before the module system became a thing, before even we really understood what modules were. I expect there will be a lot of thinking required to update this tooling to the new reality of things

[Frédéric Dupuis]

I don't think this linter makes much sense in the first place, it's simply not true that no result about computability involves measure theory. In fact the standard statement of Akra Bazzi literally has an integral in it; as far as I know mathlib is the only place that states it using a sum.

[Thomas Browning]

For now I've added an exception for Akra-Bazzi to the PR, but both of these points are worth looking into I think.

[Thomas Browning]

Yaël Dillies said:

Then probably the linter should be fixed!

Although isn't the linter mostly to avoid nasty circular import issues long-term? You can still have circular imports with private imports, right?

[Yaël Dillies]

Length 2 cycles only, so that's fine?

[Ruben Van de Velde]

No, it's more about modularizing mathlib

[Yury G. Kudryashov]

As far as I understand, the initial list of banned imports was built based on what was in the repo, not based on what should be banned forever. I think that it should act like a reminder to think once if the import is actually needed (and add an exception or remove an entry, if it is) rather than a big "NO".

[Yury G. Kudryashov]

E.g., I'm going to allow complex analysis to import algebraic topology soon, because you need simply connected sets etc for the Riemann mapping theorem.

[Anne Baanen]

Yury G. Kudryashov said:

As far as I understand, the initial list of banned imports was built based on what was in the repo, not based on what should be banned forever. I think that it should act like a reminder to think once if the import is actually needed (and add an exception or remove an entry, if it is) rather than a big "NO".

As the developer of this linter, Yuri is exactly right. Adding an exception allowing Computability.AkraBazzi to import MeasureTheory is the way to go here.

[Johan Commelin]

Should the warning/error message of the linter communicate this better? (I haven't studied it.)

[Ben Eltschig]

Yury G. Kudryashov said:

E.g., I'm going to allow complex analysis to import algebraic topology soon, because you need simply connected sets etc for the Riemann mapping theorem.

#33364 on abstract simplicial complexes is also currently blocked by the rule that analysis files can't import algebraic topology files, so that would be another argument to remove that specific rule - though if I understand this thread right, the solution until that happens is to just add an exception for that file?

[Yury G. Kudryashov]

I think that we should disable this rule, or restrict it to specific subfolders of Analysis. Say, Analysis/Calculus, until it needs algebraic topology.

[Michael Rothgang]

Adding an exception to the rule (e.g., for Analysis/Convex/SimplicialComplex) seems reasonable to me.