Compilation warnings

Stream: mathlib4

[Jonas van der Schaaf]

Hello, I'm trying to do some basic model theory in Lean defining a topology on some type. When building this I get the following (shortened) warning:

warning: Mathlib/ModelTheory/Types.lean:10:0: Modules starting with Mathlib.ModelTheory are not allowed to import modules starting with Mathlib.Topology. This module depends on Mathlib.Topology.Defs.Basic which is imported by .... which is imported by this module.

I'd like to merge these changes into mathlib if possible. Do I need to resolve this warning before opening a pull request and if so, how do I do this? Lake tells me that I can disable the linter, but this sounds wrong.

[Ruben Van de Velde]

You can open the pr, which will make it easier for people to help. There will need to be some kind of solution before we merge the pr, but what it will be depends on the situation