Environment already contains _cstage1

Stream: lean4

[Scott Morrison]

Does anyone have a suggestion for how to start diagnosing:

import Mathlib.Util.WhatsNew failed, environment already contains 'Mathlib.WhatsNew.whatsNew._cstage1' from Mathlib.Util.Whatsnew

[Sebastian Ullrich]

Is this a macOS FS case insensitivity issue?

[Scott Morrison]

That's it!

[Sebastian Ullrich]

We should probably take a look at how other languages solve this, if at all

[Reid Barton]

In Haskell a module starts with module A.B.C where so, in a sense, the file name doesn't even matter--what matters is that the declared module name matches the imported module name.

[Reid Barton]

So, that's not very helpful for us

[Reid Barton]

In the absence of a explicitly declared module name in the file, I guess the only sensible behavior is to treat the filesystem as case-sensitive, by asking the filesystem for the actual path and checking the case is correct (I assume this is possible somehow)

[Sebastian Ullrich]

Agreed on the "somehow" :)

[Sebastian Ullrich]

In the worst case, we'll have to traverse the containing directory and check if any filename literally matches the given one

[Reid Barton]

I hope that a case-insensitive filesystem does not allow two files in the same directory whose names differ only in case. Or am I misunderstanding?

[Sebastian Ullrich]

It definitely shouldn't. If you create such a directory on a case-sensitive filesystem, copying it to a case-insensitive one should fail (or leave you with just one of the files).

[Reid Barton]

In any case I agree the correct implementation of this policy is likely to be tricky and something to avoid reinventing if possible

[Reid Barton]

Apparently the Mac file system (APFS) also has the same behavior regarding Unicode normalization--it is normalization-insensitive, but preserving.

[Reid Barton]

In mathlib we could just stick to ASCII characters in file names, but in general it seems reasonable to use other characters and then the correct behavior is maybe not as obvious as in the case of, well, case