Zulip Chat Archive

Stream: lean4

Topic: VSCode OK but lake build link error


Nicolas Rouquette (Jan 24 2022 at 17:24):

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 (Jan 24 2022 at 17:36):

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 (Jan 24 2022 at 18:37):

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 (Jan 24 2022 at 23:11):

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 (Jan 24 2022 at 23:17):

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 (Feb 10 2022 at 04:09):

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


Last updated: Dec 20 2023 at 11:08 UTC