PR adding a file fails

Stream: mathlib4

[Etienne Marion]

#31666 is failing because it is not finding a file which I added. It was working well before the module system I arrived, but I changed the imports in the file and added the @[expose] public section at the beginning and it's still fail. The error does not seem to mention module though so I am not sure it is related. Here is what appears in the build mathlib section of CI (lake build works locally).

Run cd pr-branch
+ cd pr-branch
+ echo '::group::{test curl}'
{test curl}
+ echo ::endgroup::
+ ../master-branch/scripts/lake-build-with-retry.sh Mathlib
Building Mathlib with up to 5 attempts...
**** start of lake build: attempt 1
✖ [0/0] Running job computation
  error: no such file or directory (error code: 2)
    file: /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib/MeasureTheory/Function/ConditionalExpectation/Pullout.lean
Some required targets logged failures:
- job computation
error: build failed
Error: Process completed with exit code 1.

[Kevin Buzzard]

I conjecture that this is a casing issue. Your PR does not build on my linux machine (which is case sensitive) with the error

error: no such file or directory (error code: 2)
  file: /home/buzzard/Mathlib/Mathlib/MeasureTheory/Function/ConditionalExpectation/Pullout.lean

and indeed, in that directory I only find PullOut.lean with a capital O. I think the machines which run CI are also linux machines. Maybe you are using a Windows machine? I think that this is case-insensitive so might not object to the difference in spelling.

[Etienne Marion]

Oh you're probably right, thanks! I am on a mac actually, I thought it was case sensitive too but apparently not...

[Etienne Marion]

Yes it works!

[Etienne Marion]

So what happened is that when I fixed the merge conflict because of the module system I retyped the import with the wrong case.

[Thomas Murrills]

Perhaps we should have a casing linter for imports? :eyes:

[Michael Rothgang]

Would that linter check the file system, or Mathlib.lean?

[Michael Rothgang]

(The latter would make it much nicer to implement: it could be rolled into the Header linter.)

[Filippo A. E. Nuccio]

Thomas Murrills said:

Perhaps we should have a casing linter for imports? :eyes:

At least we should say it somewhere in the doc, in case someone falls into the same trap and cannot understand where the problem comes from