EReal instance

Stream: mathlib4

[Antoine Chambert-Loir]

Importing these two files

import Mathlib.Topology.Instances.Ereal
import Mathlib.Data.Real.Ereal

causes a strange error import Mathlib.Data.Real.Ereal failed, environment already contains 'EReal.instMulPosReflectLTERealInstMulERealInstERealZeroToPreorderInstERealPartialOrder.proof_1' from Mathlib.Data.Real.EReal

Am I doing something wrong ?

[Kevin Buzzard]

I get

stderr:
error: no such file or directory (error code: 2)
  file: ./././Mathlib/Topology/Instances/Ereal.lean

so it looks to me like you have a corrupted mathlib (maybe just a file that needs deleting). What does git status report?

[Anatole Dedecker]

On current master, both files are named EReal, not Ereal. I think you must have some old oleans corresponding to old file names which could confuse Lean.

[Anatole Dedecker]

The fix is obviously to use the correct file names, but could you confirm the diagnosis by checking that you get the right error message after lean exe cache clean! && lean exe cache get!?

[Kevin Buzzard]

I remember being very confused when I discovered that import X could work even if X.lean didn't exist! It broke my model of what was going on. In Lean 3, it sufficed to have X.olean (and if X.olean was out of date then now you're in real trouble)

[Antoine Chambert-Loir]

Anatole Dedecker said:

The fix is obviously to use the correct file names, but could you confirm the diagnosis by checking that you get the right error message after lean exe cache clean! && lean exe cache get!?

with s/lean/lake/, I presume ? — I'm just trying, but I get the same error…
I am now trying to lake update && lake exe cache get…

[Antoine Chambert-Loir]

No change…

[Antoine Chambert-Loir]

OK! This was due to the lower score r in the import ….Ereal.
I changed both to EReal, and the problem was solved in the MWE, but not in the main project because another file was also loading ….Ereal.

[Kevin Buzzard]

It sounds like you have spurious files which shouldn't be there. If this is a project which depends on mathlib then just remove the entire lake-packages directory (i.e. your copy of mathlib + std + ... which the repo depends on) and type lake exe cache get again; this should remove the bad files.

[Antoine Chambert-Loir]

I did that and the initial problem persists (on MacOS).
Also, if Misc.lean contains

import Mathlib.Data.Real.Ereal

-- Mathlib.Data.Real.EReal is loaded
example : MulPosReflectLT EReal := inferInstance

(note the lowercase r) and Main.leancontains

import Misc.lean
import Mathlib.Data.Real.Ereal

then Mathlib.Data.Real.EReal is loaded in both files (uppercase R!), but the second gives an error.

[Kevin Buzzard]

It's very surprising to me that both my suggestion and Anatole's suggestion don't fix the problem.

[Anne Baanen]

Back when I used Mac OS I recall that the file system is case insensitive, so sometimes programs would get confused between uppercase and lowercase file names. Here it looks like Lean considers Ereal and EReal to be different files (one of which should not exist) but the OS loads them both. I wonder if the same happens on Windows?

[Anne Baanen]

(One specific issue I recall is collaborating via Dropbox and my friend complaining that my changes weren't showing up. Turned out they had an uppercase filename and I was editing a lowercase one.)

[Anatole Dedecker]

Ooooooooh that is an interesting explanation

[Jireh Loreaux]

Really? HFS+ is case insensitive? That's ridiculous to me, but you seem to be correct.&text=One%20or%20other%20can%20break,insensitive%20is%20the%20default%20however).

[Antoine Chambert-Loir]

I think that something happens like what @Anne Baanen is saying, except that I chose my file system to be case sensitive. So I wonder whether there are some inconsistencies somewhere…

[Antoine Chambert-Loir]

After having read @Jireh Loreaux , I realize that the case sensitive file format is in fact case insensitive:

(23:03) pro-acl > rm test
(23:03) pro-acl > cat Test
cat: Test: No such file or directory
(23:03) pro-acl > echo Hello world >> test
(23:03) pro-acl > cat Test
Hello world
(23:03) pro-acl >

[Vincent Beffara]

HFS+ is IIRC "case-insensitive but case-preserving"