VSCode OK but lake build link error

Stream: lean4

[Nicolas Rouquette]

In this project, https://github.com/NicolasRouquette/dimensional-calculus.lean4,
I found that I could use Lean.Rat like this:

import Lean.Data.rat

-- Arithmetic for dimensional calculus
namespace DimensionalAnalysis

inductive DCalc : Type
  | symbol : String -> DCalc
  | mul : DCalc -> DCalc -> DCalc
  | div : DCalc -> DCalc -> DCalc
  | power : DCalc -> Lean.Rat -> DCalc
  deriving Repr

It took me a while to figure this out.. it was not obvious to me that Lean.Rat requires importing Lean.Data.rat.

In VSCode, I can run the #check and #eval commands without a problem.
However, when I build with lake, I get a link error:

error: ld.lld: error: undefined symbol: initialize_Lean_Data_rat
>>> referenced by .\build.lean4\ir\Arith.o:(initialize_Arith)

In VSCode, I can navigate to Lean.Data.rat, which brings up this file:

~\.elan\toolchains\leanprover--lean4---nightly-2022-01-23\lib\lean\src\lean\data\rat.lean

It is surprising to me that VSCode can resolve the dependency but lake cannot.

What do I need to do to link this code?

Is it a dependency in the lakefile.lean or something else?

• Nicolas.

[Gabriel Ebner]

This looks like an issue with case-insensitive file systems (like windows has). Does it work if you change import Lean.Data.rat to import Lean.Data.Rat?

[Nicolas Rouquette]

Yes it does! Now it links cleanly! Thanks!

According to Windows' fsutil command, my folder had case sensitivity disabled:

fsutil file queryCaseSensitiveInfo .

Perhaps it might be less confusing to suggest to Windows users to enable case sensitivity for their lean project folders.

• Nicolas.

[Mac]

Note that this error only appears in the lake build because the error happens at link time, and VSCode (currently) doesn't do any linking to refresh dependencies.

[Mac]

Also, the problem here is less about the filesystem and more a result of the fact that module names are case sensitive and fixed at compiled time. Thus, a module compiled as Lean.Data.Rat cannot be imported as Lean.Data.rat. The same thing would happen if you built a Foo.olean from a Foo.lean, renamed it to Bar.olean, and tried to import Bar.

[Chris Lovett]

Hey @Mac, hopefully the lean compiler is always case sensitive about imports? If not we should fix that.