fail to build on windows after #77 (Add UnicodeCLib)

[notch1p]

currently when compiling on Windows the project would fail due to linker error (Log below)

✖ [13/15] Building UnicodeBasic.TableLookup:dynlib
trace: .> c:\Users\notch1p\.elan\toolchains\leanprover--lean4---v4.22.0\bin\clang.exe -shared -o C:\Us
ers\notch1p\Downloads\lean4-unicode-basic\.lake\build\lib\lean\UnicodeBasic_TableLookup.dll @C:\Users\
notch1p\Downloads\lean4-unicode-basic\.lake\build\lib\lean\UnicodeBasic_TableLookup.dll.rsp
info: stderr:
ld.lld: error: undefined symbol: unicode_case_lookup
>>> referenced by C:\Users\notch1p\Downloads\lean4-unicode-basic\.lake\build\ir\UnicodeBasic\TableLook
up.c.o.export:(l_Unicode_CLib_lookupCase___boxed)
>>> referenced by C:\Users\notch1p\Downloads\lean4-unicode-basic\.lake\build\ir\UnicodeBasic\TableLook
up.c.o.export:(l_Unicode_lookupCaseMapping)

ld.lld: error: undefined symbol: unicode_prop_lookup
>>> referenced by C:\Users\notch1p\Downloads\lean4-unicode-basic\.lake\build\ir\UnicodeBasic\TableLook
up.c.o.export:(l_Unicode_CLib_lookupProp___boxed)
>>> referenced by C:\Users\notch1p\Downloads\lean4-unicode-basic\.lake\build\ir\UnicodeBasic\TableLook
up.c.o.export:(l_Unicode_lookupGC)
>>> referenced by C:\Users\notch1p\Downloads\lean4-unicode-basic\.lake\build\ir\UnicodeBasic\TableLook
up.c.o.export:(l_Unicode_lookupGC___boxed)
>>> referenced 16 more times
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\notch1p\.elan\toolchains\leanprover--lean4---v4.22.0\bin\clang.exe' 
exited with code 1
Some required builds logged failures:
- UnicodeBasic.TableLookup:dynlib
error: build failed

I suspect this has something to do with the UnicodeCLib we're currently using which uses CFFI. After switching to a commit before the addition of such library I can confirm that it builds successfully. But the reason that this would only fail on Windows is unclear to me: Maybe because ld can't find the static unicodeclib.a specifically on Windows? -- But I'm not sure.

So I compared the current lakefile to one that a project of mine are currently using (which also uses CFFI but can build on Windows), and it turns out that what's missing is a extern_lib declaration:

extern_lib libunicodeclib := UnicodeCLib.fetch

after adding the above we can successfully build on windows and this modification doesn't affect existing builds on other platforms (See workflow).

I've made a PR to fix this, see #82.

[fgdorais]

I was worried this would happen! Thanks for the report!

[fgdorais]

Investigation is ongoing. This may be a Lake bug.

[notch1p]

For someone else who encountered this bug: As of Lake version 5.0.0-src+797c613 (Lean version 4.24.0), this bug still persists. While now we may use the manual extern_lib trick to fix this temporarily, as a small enhancement it would be a little smoother with (in the user's lakefile.lean):

meta if System.Platform.isWindows then
  post_update do
    let some p <- findPackage? "UnicodeBasic".toName | return ()
    let path := p.dir / "lakefile.lean"
    let lakefile <- IO.FS.readFile path
    let externDef := "extern_lib libuc := UnicodeCLib.fetch"
    IO.FS.withFile path .append fun h =>
      unless lakefile.endsWith externDef do
        h.putStr externDef

The post_update hook will run on the first lake build/exe invocation as well as subsequent lake update.

although a cleaner solution (if you are the package owner) would be to just use a conditional extern def for Windows.

[fgdorais]

Could you edit PR #82 to make it conditional? I could merge that as a temporary fix.

[fgdorais]

The temporary fix has been merged. I'm leaving this open until it is fixed upstream. No additional work will be done until then.

[monsterkrampe]

It looks like I have the same problem but on NixOS instead of Windows.
The temporary fix of adding extern_lib libunicodeclib := UnicodeCLib.fetch also works for me.

If this also affects other Linux Distros, I would have assummed that more people would complain though.
But I fail to see right now, how the unicodeclib.so shared lib would be discovered automatically on any system since it only exists locally in .lake/build/lib. Or at least I don't see why NixOS should behave differently from other distros when it comes to a local .so.

Anyway, it's not the first time I have a hard time with shared libraries under NixOS 😅
If we are confident that this works on less exotic Linux distros, then I'll just go back to figuring out why the .so is not discovered on my system :D
Otherwise, is just putting extern_lib libunicodeclib := UnicodeCLib.fetch unconditionally an option?

EDIT: I'm just realizing that without putting extern_lib libunicodeclib := UnicodeCLib.fetch on my system, the UnicodeCLib does not even seem to be built. Consequently, there is also no .so generated for it that could be found. This makes things even more mysterious to me. But maybe you guys will enlighten me :)

[fgdorais]

Mac @tydeu As far as I can tell this needs to be fixed in Lake? I'm not sure what the fundamental issue is. Thoughts?

[notch1p]

On my own Debian/Ubuntu machine it just works and it’s the same with github actions. i’m not familiar with nix so I can’t say. Currently the `meta if` clause only applies to windows machine and I don’t think Lean has some API to filter specific linux distros but you can certainly get that information from `/etc/os-release` On 3 Dec 2025, at 14:23, Lukas Gerlach ***@***.***> wrote:  [https://avatars.githubusercontent.com/u/12497479?s=20&v=4]monsterkrampe left a comment (fgdorais/lean4-unicode-basic#81)<#81 (comment)> It looks like I have the same problem but on NixOS instead of Windows. The temporary fix of adding extern_lib libunicodeclib := UnicodeCLib.fetch also works for me. If this also affects other Linux Distros, I would have assummed that more people would complain though. But I fail to see right now, how the unicodeclib.so shared lib would be discovered automatically on any system since it only exists locally in .lake/build/lib. Anyway, it's not the first time I have a hard time with shared libraries under NixOS 😅 If we are confident that this works on less exotic Linux distros, then I'll just go back to figuring out why the .so is not discovered on my system :D Otherwise, is just putting extern_lib libunicodeclib := UnicodeCLib.fetch unconditionally an option? — Reply to this email directly, view it on GitHub<#81 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AEPBVSSSQ32MUPMOUCAZ33D37Z6UJAVCNFSM6AAAAACD7TJ6XGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTMMBVGI4DEOBYHA>. You are receiving this because you authored the thread.Message ID: ***@***.***>

[monsterkrampe]

It might be an option to extend the conditional to cover not only Windows but also NixOS, true.
But first, I would like to understand, why this is not working right now.

Out of curiosity, I just tried to build a DynLib instead of a static lib for the UnicodeCLib. I don't really have any experience with that so I'm not sure if this is doing the right thing but at least it compiles!
This is the diff:

diff --git a/lakefile.lean b/lakefile.lean
index 78f010f..17898ce 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,7 +13,7 @@ package UnicodeBasic where
   reservoir := true
   precompileModules := true
 
-target UnicodeCLib pkg : FilePath := do
+target UnicodeCLib pkg : Dynlib := do
   let mut oFiles : Array (Job FilePath) := #[]
   for file in (← (pkg.dir / "UnicodeCLib").readDir) do
     if file.path.extension == some "c" then
@@ -21,8 +21,8 @@ target UnicodeCLib pkg : FilePath := do
       let src ← inputTextFile file.path
       let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-O", "-fPIC"]
       oFiles := oFiles.push <| ← buildO obj src weakArgs
-  let name := nameToStaticLib "unicodeclib"
-  buildStaticLib (pkg.sharedLibDir / name) oFiles
+  let name := nameToSharedLib "unicodeclib"
+  buildSharedLib name (pkg.sharedLibDir / name) oFiles #[]
 
 -- temporary fix for Windows
 meta if System.Platform.isWindows then
@@ -30,7 +30,7 @@ extern_lib libunicodeclib := UnicodeCLib.fetch
 
 @[default_target]
 lean_lib UnicodeBasic where
-  moreLinkObjs := #[UnicodeCLib]
+  moreLinkLibs := #[UnicodeCLib]
 
 lean_lib UnicodeData

It might be noteworthy that there are 16 build steps now instead of 15 where one of the first ones compiles UnicodeCLib. This does not happen when building the static library version.

Feel free to tell me if this is not surprising at all. It is to me but maybe only because this is uncharted territory for me :D

[notch1p]

I guess this aligns with what Mac said earlier: #82 (comment) (you made it a dynlib and specified it in moreLinkLibs so it gets linked to module dynlibs)

I tried the diff patch, but for Windows however,

• lld would output

lld: error: unable to find library -lunicodeclib.dll

(Even though unicodeclib.dll is there and is built BEFORE everything) and the extern_lib trick doesn't work now.

• Another solution is for precompileModules to be set to false if we were to ditch extern_lib (for some reasons; I mentioned this in the above discussion as well).

There're probably inconsistencies across platforms as well as the implementation of lake itself, making this thing convoluted.

for reference, the windows diff patch is

diff --git a/lakefile.lean b/lakefile.lean
index 78f010f..106f1b7 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,7 +13,7 @@ package UnicodeBasic where
   reservoir := true
   precompileModules := true

-target UnicodeCLib pkg : FilePath := do
+target UnicodeCLib pkg : Dynlib := do
   let mut oFiles : Array (Job FilePath) := #[]
   for file in (← (pkg.dir / "UnicodeCLib").readDir) do
     if file.path.extension == some "c" then
@@ -21,16 +21,16 @@ target UnicodeCLib pkg : FilePath := do
       let src ← inputTextFile file.path
       let weakArgs := #["-I", (← getLeanIncludeDir).toString, "-O", "-fPIC"]
       oFiles := oFiles.push <| ← buildO obj src weakArgs
-  let name := nameToStaticLib "unicodeclib"
-  buildStaticLib (pkg.sharedLibDir / name) oFiles
+  let name := nameToSharedLib "unicodeclib"
+  buildSharedLib name (pkg.sharedLibDir / name) oFiles #[]

 -- temporary fix for Windows
 meta if System.Platform.isWindows then
-extern_lib libunicodeclib := UnicodeCLib.fetch
+extern_lib libunicodeclib := UnicodeCLib.fetch <&> (Dynlib.path <$> ·)

 @[default_target]
 lean_lib UnicodeBasic where
-  moreLinkObjs := #[UnicodeCLib]
+  moreLinkLibs := #[UnicodeCLib]

Also, I was worried meta if does not take IO Bool but it actually does, that makes it easier to filter specific linux distros.

[monsterkrampe]

The discussion in the PR is quite insightful, I had missed that!
I can also confirm that setting precompileModules to false let's me build successfully.

But if I understand correctly, I should probably just wait until this is fixed in lake.
Thank you very much :)