-
Notifications
You must be signed in to change notification settings - Fork 6
Description
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.