Zulip Chat Archive

Stream: new members

Topic: Conflicting imports


Nathan Corbyn (Oct 18 2024 at 14:28):

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 (Oct 18 2024 at 14:40):

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 (Oct 18 2024 at 14:42):

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 (Oct 18 2024 at 14:43):

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

Vincent Beffara (Oct 18 2024 at 14:43):

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 (Oct 18 2024 at 14:44):

Oh my goodness! That was it!

Nathan Corbyn (Oct 18 2024 at 14:45):

Thank you very much!

Vincent Beffara (Oct 18 2024 at 14:45):

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

Nathan Corbyn (Oct 18 2024 at 14:45):

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

Kyle Miller (Oct 18 2024 at 15:29):

@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 (Oct 18 2024 at 15:56):

Will do!


Last updated: May 02 2025 at 03:31 UTC