not allowed to import modules starting with Mathlib.Geometry

Stream: mathlib4

[Bjørn Kjos-Hanssen]

While working on #18711 I was surprised to get this linter message:

Modules starting with Mathlib.Topology are not allowed to import modules starting with Mathlib.Geometry

In my case, proving that one-point compactification of Euclidean space is homeomorphic to the sphere, I wanted to import the material on stereographic projection from Mathlib.Geometry.Manifold.Instances.Sphere. What to do?

[Jon Eugster]

This is a very new linter and there should be a file somewhere where the "allowed" dependencies of mathlib subdirectories can be adjusted.

[Jon Eugster]

It's aimed to help getting a more modular mathlib but I don't think anybody expects the current list to be final. (sorry on mobile, I'm sure somebody can fill in the details)

[Bjørn Kjos-Hanssen]

Sounds good @Jon Eugster I'll just add a line to overrideAllowedImportDirs (even if that means a lot of olean's have to be rebuilt locally)

[Johan Commelin]

The other option is to move the definition of the stereographic projection and all its topological properties out of the geometry folder.

[Jz Pan]

... or move your one-point compactification result to Geometry folder.