Build failure on macOS with Nix

Stream: lean4 dev

[Leni Aniva]

Has anyone else encountered this issue while building the target .#packages.x86_64-darwin.leanc in recent commits using Nix on macOS?

The issue occurred with invalid linker flags for the target libInit_shared.
I have a draft PR here that doesn't completely solve the problem.

I think it has something to do with the linker flags while building libInit.a because the log shows this warning when building libInit_shared:

leanc> ld: warning: directory not found for option '-L/nix/store/v2y691apvl5y0crkwlzvpfkplvh09qx2-lean-bin-tools/lib/lean'
leanc> ld: warning: ignoring file /nix/store/m5mkq2bbq66z4xxyzprr39nlx80dbl0a-Lean-lib/libLean.a, building for macOS-x86_64 but attempting to link with file built for unknown-unsupported file format ( 0x21 0x3C 0x74 0x68 0x69 0x6E 0x3E 0x0A 0x2F 0x20 0x20 0x20 0x20 0x20 0x20 0x20 )
leanc> ld: warning: ignoring file /nix/store/xdzls0mjd8y2nb2fasrb8xlbyp3l9fx0-Lake-lib/libLake.a, building for macOS-x86_64 but attempting to link with file built for unknown-unsupported file format ( 0x21 0x3C 0x74 0x68 0x69 0x6E 0x3E 0x0A 0x2F 0x20 0x20 0x20 0x20 0x20 0x20 0x20 )
leanc> ld: warning: ignoring file /nix/store/n8pzs12zzpd55h7zff6xqss0nv0dckmk-Init-lib/libInit.a, building for macOS-x86_64 but attempting to link with file built for unknown-unsupported file format ( 0x21 0x3C 0x74 0x68 0x69 0x6E 0x3E 0x0A 0x2F 0x20 0x20 0x20 0x20 0x20 0x20 0x20 )

The build failure occurs further downstream when building leanc:

leanc> Undefined symbols for architecture x86_64:
leanc>   "_initialize_Init", referenced from:
leanc>       _initialize_Leanc in Leanc.o
leanc>   "_initialize_Lean_Compiler_FFI", referenced from:
leanc>       _initialize_Leanc in Leanc.o
...

but I think its a issue because the undefined symbols such as _initialize_Init indeed shows up in libInit.a

[Leni Aniva]

The split of leanshared into libInit_shared and leanshared happened on this commit by Sebastian

[Leni Aniva]

I've fixed most of the missing symbol errors except for this one: _lean_initialize

[Leni Aniva]

I'm stuck. I tried to mimic the packages.nix file before Sebastian's change but it still could not compile

[Leni Aniva]

I fixed it!: https://github.com/leanprover/lean4/pull/3811

[Leni Aniva]

if you're a macOS nix user please try this branch out and see if it works. It compiles on my machine

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Leni Aniva works for me!

[Leni Aniva]

merged into master. Hopefully we get this patch in 4.9.0

[Kim Morrison]

This will land in v4.10.0-rc1, which Mathlib will (hopefully) move to in a few days.

[Kim Morrison]

(Although I guess since it only touches nix configuration, I can backport it if someone tells me it is valuable!)

[Joachim Breitner]

(done)

[Leni Aniva]

Kim Morrison said:

(Although I guess since it only touches nix configuration, I can backport it if someone tells me it is valuable!)

did you backport it? Its very useful for us using macOS

[Kim Morrison]

I didn't, sorry.