Inconsistent handling of capitalization in module names

[robdockins]

Prerequisites

• [ X] 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.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

When a module with capital letters is imported into another module, the name of the module is inconsistently rendered in the generated code, eventually leading to missing symbol errors in the linker.

Steps to Reproduce

1. Run the included build script:

leanbug.zip

Expected behavior:

Program should compile and print "hi!" when run.

Actual behavior:

Missing symbols in the linker:

$ ./build.sh
+ export LEAN_PATH=/usr/local/lib/lean/library:.
+ LEAN_PATH=/usr/local/lib/lean/library:.
+ lean --make camelCase.lean
+ lean --make lowercase.lean
+ lean -c camelCase.cpp camelCase.lean
+ lean -c lowercase.cpp lowercase.lean
+ leanc -o test lowercase.cpp camelCase.cpp
Undefined symbols for architecture x86_64:
  "initialize_camelCase(lean::object*)", referenced from:
      initialize_lowercase(lean::object*) in lowercase-9b5b9c.o
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)

Examining the generated camelCase.cpp we can find the function initialize_camelcase, where the module name appears to have been forced into lowercase.

Reproduces how often: [What percentage of the time does it reproduce?]

100% reproducable

Versions

$ lean --version
Lean (version 4.0.0, commit 52b86c3b4b7e, Release)

macOS 10.14.6

Additional Information

Maybe this is related to issues with filesystem case-sensitivity?

[leodemoura]

Thanks for posting the problem. We are aware of this issue, but it will not be fixed in the near future since we consider it of low priority.
As a temporary workaround, please always use lower case file names as we are doing at
https://github.com/leanprover/lean4/tree/master/library/init

[Kha]

I assume this must be fixed now that we do indeed use PascalCase file naming.