Log.Base and Zmod.Basic conflicting with each other (?)

Stream: mathlib4

[Rahul Saha]

Hey guys, I am using the latest mathlib4 commit for a project and have the following two imports:

import Mathlib.Analysis.SpecialFunctions.Log.Base
import Mathlib.Data.Zmod.Basic

Individually, each of these imports work fine. But when put together as above, it gives the following error:

import Mathlib.Data.Zmod.Basic failed, environment already contains 'Int.castAddHom._at.ZMod.lift._spec_1._cstage2' from Mathlib.Data.ZMod.Basic

I am not sure how to parse this, perhaps there is some circular import happening somewhere? Some help would be appreciated, thank you!

[Anatole Dedecker]

Ah we've had this a few days ago! It's Mathlib.Data.ZMod.Basicwith a capital M.

[Anatole Dedecker]

Let me guess, you're on MacOS?

[Rahul Saha]

yep MacOS

[Rahul Saha]

and thanks that worked!

[Anatole Dedecker]

An explanation of what goes wrong: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/EReal.20instance/near/383550857

[Anatole Dedecker]

Basically: you import the Zmod file (which does not exist), but MacOS is """nice""" enough to give the ZMod file to Lean instead. But the problem is that another file imports ZMod, and Lean has no idea that these files are actually the same!

[Rahul Saha]

oh wow, that's quite silly behavior from the os, thanks for the explanation.

[Yury G. Kudryashov]

AFAIR, Windows has case-insensitive filesystem too.

[Kevin Buzzard]

I think it's case-insensitive in a different way! Read the extensive discussion in the linked thread :-)