fix: Add platform dependent flag to lib target in nix

[lenianiva]

(Currently doesn't build on Darwin. Help wanted)

Closes #3810 (RFC or bug issue number fixed by this PR, if any)

[lenianiva]

WIP: Although both libInit_shared and leanshared can build, currently there's a missing symbol error:

$ nix build .#packages.x86_64-darwin.leanc

gives

ld: warning: directory not found for option '-L/nix/store/6bk086vc6m88274aapc6md587l7p1s4d-lean-bin-tools/lib/lean'
Undefined symbols for architecture x86_64:
  "_lean_initialize", referenced from:
      _main in Leanc.o
ld: symbol(s) not found for architecture x86_64
clang-11: error: linker command failed with exit code 1 (use -v to see invocation)

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-03-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-03-30 22:09:37)
• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-04-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-04-26 23:19:12)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 366f3ac272b6a12b19cabd8573652fc138804bdf --onto ea46bf2839ad1c98d3a0c3e5caad8a81f812934c. (2024-06-10 16:49:43)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 30a922a7e914a37c98e2c4ab88440e347084172f --onto 5c978a2e2437e30e2c01a9b027b2944d709919c9. (2024-06-28 03:31:48)

[jetjinser]

Any progress? I'm in the same predicament and I really want it to work on my x86_64-darwin. Is there anything I can do to help?

I finally found that missing symbol _lean_initialize is in leancpp, and this dependency is not in Leanc.executable.

Frankly speaking, I am a bit confused because I don't understand how lean is built 😔.

[nomeata]

From my side the status is that I'm rooting for you here, and fixes can be merged, but usage of nix beyond what we need for the CI setup need to be taken care of by those that use it. Hope you understand.

[lenianiva]

Any progress? I'm in the same predicament and I really want it to work on my x86_64-darwin. Is there anything I can do to help?

I finally found that missing symbol _lean_initialize is in leancpp, and this dependency is not in Leanc.executable.

Frankly speaking, I am a bit confused because I don't understand how lean is built 😔.

can you poke around the build targets of nix/bootstrap.nix a bit to see what is going on? When I tried to fix it I looked at the symbol table of libInit_shared and leanc etc. to see if they have the symbols required, but I don't know why it still doesn't compile.

[lenianiva]

I'll periodically merge master into this branch and see if anything changes, but I have spent >8h on this and I could not make more progress

[lenianiva]

Any progress? I'm in the same predicament and I really want it to work on my x86_64-darwin. Is there anything I can do to help?

I finally found that missing symbol _lean_initialize is in leancpp, and this dependency is not in Leanc.executable.

Frankly speaking, I am a bit confused because I don't understand how lean is built 😔.

How is leancpp not a dependency of Leanc.executable? The linker flags of leanshared has -lleancpp, and leanshared is a dependency of leanc.

Lean is built with bootstrapping, and there is a function in nix/bootstrap.nix which builds a single stage. There is some problem with this function so the relevant symbols for _lean_initialize didn't go into leanc

[lenianiva]

Any progress? I'm in the same predicament and I really want it to work on my x86_64-darwin. Is there anything I can do to help?

I finally found that missing symbol _lean_initialize is in leancpp, and this dependency is not in Leanc.executable.

Frankly speaking, I am a bit confused because I don't understand how lean is built 😔.

I fixed it!

[jetjinser]

Any progress? I'm in the same predicament and I really want it to work on my x86_64-darwin. Is there anything I can do to help? I finally found that missing symbol _lean_initialize is in leancpp, and this dependency is not in Leanc.executable. Frankly speaking, I am a bit confused because I don't understand how lean is built 😔.

I fixed it!

marvelous! 😍

[nomeata]

@jetjinser, did you have a chance to review and test the fix?

[jetjinser]

@jetjinser, did you have a chance to review and test the fix?

Yes! It actually built successfully on my x86_64-darwin machine! It looks like nix specifies the correct lib on darwin.