Import error

Stream: mathlib4

[Gian Cordana Sanjaya]

Hello, it seems that I got an error just from these two lines in Lean 4.9.0:

import Mathlib.Data.Int.Modeq
import Mathlib.Data.Nat.Periodic

The error says:

import Mathlib.Data.Int.Modeq failed, environment already contains 'Int.«_aux_Mathlib_Data_Int_ModEq___macroRules_Int_term_≡_[ZMOD_]_1»._cstage1' from Mathlib.Data.Int.ModEq

[Yaël Dillies]

Uhoh, that looks like some autogenerated auxiliary declaration got autogenerated twice

[Bhavik Mehta]

This seems to work fine on the web editor, (correcting .Modeq to .ModEq, since .Modeq doesn't exist in mathlib): https://live.lean-lang.org/#code=import%20Mathlib.Data.Int.ModEq%0Aimport%20Mathlib.Data.Nat.Periodic . Perhaps you have a local file Mathlib.Data.Int.Modeq that shouldn't exist?

[Gian Cordana Sanjaya]

Oh, good point. I didn't notice that the correct file name is .ModEq; changing it fixed my problem.

So, I guess the real issue for me now is that just import Mathlib.Data.Int.Modeq on itself works when it shouldn't. I don't see .Modeq either locally, and going directly to the file via one of the theorems it contain shows that the file is .ModEq as well.

[Kim Morrison]

Which OS are you on?

[Dagur Asgeirsson]

I've had something similar happen to me on MacOS Sonoma 14.5, making a capitalisation typo like this in the imports and everything works fine locally, but then I get errors in CI (as I should)

[Gian Cordana Sanjaya]

I'm also using MacOS Sonoma 14.5.

[Sebastian Ullrich]

lean#4538 should fix that