Link errors on MacOS (and Windows?) because of case insensitive filesystem

[goens]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

In MacOS, if a file has the wrong capitalization, I get a link error instead of a file-not-found error. This seems to be because the symbols are derived from the filename and are case-sensitive but since the MacOS filesystem is not case-sensitive, it will find the file but not be able to link correctly. I filed this for Lake but @tydeu advised it is a general Lean issue and I should file it here instead. From their comment, I suspect this should also happen in Windows but have no windows machine to check it on.

Steps to Reproduce

❯ lake init Test
❯ mv Test.lean TesT.lean
❯ lake build
Building Test
Compiling Test
Building Main
Compiling Main
Linking test
error: > /Users/goens/.elan.arm/toolchains/leanprover--lean4---nightly-2023-03-01/bin/leanc -o ./build/bin/test ./build/ir/Main.o ./build/ir/Test.o
error: stderr:
ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib
ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 12.1.0, which is newer than target minimum of 12.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 12.1.0, which is newer than target minimum of 12.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 12.1.0, which is newer than target minimum of 12.0.0
ld64.lld: error: undefined symbol: _initialize_Test
>>> referenced by ./build/ir/Main.o:(symbol _initialize_Main+0x78)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/Users/goens/.elan.arm/toolchains/leanprover--lean4---nightly-2023-03-01/bin/leanc` exited with code 1

Expected behavior: I'd expect the same behavior as in Linux, and/or at least a friendlier error message (it was hard to figure out the root of this issue). On Linux I get:

On Linux, on the other hand, this doesn't happen:

❯ lake init Test
❯ mv Test.lean TesT.lean
❯ lake build
error: no such file or directory (error code: 2)
  file: ./././Test.lean

If a file-not-found error is impossible in this case because of the Filesystem, maybe filename-derived symbols should also be case-insensitive, in which case the linker should work?

Actual behavior: See above.

Reproduces how often: Every time.

Versions

MacOS 12.1 (ARM)

❯ lake --version
Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-03-01)
❯ lean --version
Lean (version 4.0.0-nightly-2023-03-01, commit 0da281f, Release)
❯ elan --version
elan 1.4.2 (4a1b1b918 2022-09-13)

Additional Information

I'm not sure if this is related to #1035 but might be worth mentioning

[Kha]

This should be fixed with #4538

[Kha]

My bad, that was actually reverted in #4896