Conflicting imports

Stream: new members

[Nathan Corbyn]

I've authored a file (call it file B) with some auxiliary results that depends on a couple of files from MathLib. When I import these into another file (file A) in my workspace, I get a conflict as some of the MathLib imports in file A already import the imports from file B. How do I deal with this? The error I'm getting is: import MathLib.CategoryTheory.Adjunction.Reflective failed, environment already contains 'CategoryTheory.coreflectorAdjunction._rarg._cstage2' from Mathlib.CategoryTheory.Adjunction.Reflective

[Etienne Marion]

Does removing the error imports in file A solves it? If A import B and B imports C there is no need to import C in A

[Nathan Corbyn]

In A I'm importing:

import Mathlib.CategoryTheory.Sites.Coverage
import Mathlib.CategoryTheory.Sites.Sieves
import Mathlib.CategoryTheory.Sites.Sheaf
import Mathlib.CategoryTheory.Sites.Sheafification
import Mathlib.CategoryTheory.Sites.Equivalence

and in B I'm importing

import MathLib.CategoryTheory.Adjunction.Reflective
import MathLib.CategoryTheory.Yoneda

I think the problem is that the A imports also import MathLib.CategoryTheory.Adjunction.Reflective

[Nathan Corbyn]

The error goes away if I remove the imports in A, but then A doesn't build anymore :sweat_smile:

[Vincent Beffara]

Careful about MathLib vs Mathlib if you have a case-insensitive OS, in principle lean knows not to import the same file twice but here there is a typo that confuses it.

[Nathan Corbyn]

Oh my goodness! That was it!

[Nathan Corbyn]

Thank you very much!

[Vincent Beffara]

(On a case-sensitive OS, the imports on B would just fail.)

[Nathan Corbyn]

I didn't even notice the case---thank you so much

[Kyle Miller]

@Nathan Corbyn Would you mind adding a comment on lean4#2768 with details of what operating system you are using and the output of #eval Lean.versionString? Thanks!

[Nathan Corbyn]

Will do!