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