24 oct llvm backend files via cmake #12
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
link to zlib correctly on macos Thanks to @tobiasgrosser: https://github.com/tobiasgrosser/lean4/pull/6/files#diff-148715d6ea0c0ea0a346af3f6bd610d010d490eca35ac6a9b408748f7ca9e3f4 add LLVM bindings link against LLVM via llvm-config
We can use 'llvm-config' during build time and bake in the flags. There is no need to ship 'llvm-config' with 'stage1/bin'.
This fixed the CI error on Linux Release: ld.lld: error: unknown argument '-Bdynamic-L/home/runner/work/lean4/lean4/build/llvm/lib' ld.lld: error: unable to find library -lLLVM-15
The windows build does not define a '$CP' variable, so switch to plain old 'cp'.
How did this stuff ever work on linux? I need to run `llvm-target/bin/llvm-config` to find out the linker options I need for the target LLVM? But the target `llvm-config` is an `aarch64` binary, which we definitely can't run on the host `x86_64` machine! Do we take on faith that `llvm-host/bin/llvm-config` will provide flags that are approximately correct, and move ahead with that? That seems like a dubious assumption to me. It seems like it used to work on linux, as I had missed the `-DLLVM_CONFIG=path/to/llvm-config` option in the linux builds. So it was (luckily) finding the (host?) `llvm-config` and configuring itself correctly?
I feel that previously, the paths were working out due
to dumb luck, or me manually setting up LD_LIBRARY_PATH
in the install script.
Locally, 'leanc --print-ldflags' prints out:
```
sirpinski :: lean-llvm/lean4 » leanc --print-ldflags
-I /home/bollu/.elan/toolchains/leanprover--lean4---nightly/include -fPIC -fvisibility=hidden -L /home/bollu/.elan/toolchains/leanprover--lean4---nightly/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -lm -Wl,--as-needed -lgmp -Wl,--no-as-needed -ldl -pthread
```
Note that we only have
`-L /home/bollu/.elan/toolchains/leanprover--lean4---nightly/lib/lean`
I would have to either (a) move the `llvm-15.so` into `lib/lean`,
or (b) add a linker path to the parent directory of `-L /home/bollu/.elan/toolchains/leanprover--lean4---nightly/lib`
for it to pick up LLVM.
Let's actually test this by looking at what
`leanc --print-{cflags,ldflags} ` produces.
We see that on the build runner, we get the flags: + lean-4.0.0-linux/bin/leanc --print-ldflags -I /home/runner/work/lean4/lean4/lean-4.0.0-linux/include -fPIC -fvisibility=hidden -L /home/runner/work/lean4/lean4/lean-4.0.0-linux/lib/lean -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -L/home/runner/work/lean4/lean4/build/llvm/lib -lLLVM-15 -lm -Wl,--as-needed -lgmp -Wl,--no-as-needed -ldl -pthread See that we have -L: 1. /home/runner/work/lean4/lean4/build/llvm/lib 2. /home/runner/work/lean4/lean4/lean-4.0.0-linux/lib/lean The path (1) is generated by `llvm-config`, relative to its location. It's also completely bunk. If we want to generate a sensible path from `llvm-config`, we should keep `llvm-config` within the `stage1/bin` tree, and then query `stage1/bin/llvm-config --libs` or whatever. Alternatively, We add another path like (2), expect to point to: /home/runner/work/lean4/lean4/lean-4.0.0-linux/lib/llvm/ which will give it access to the LLVM libs. This commit attempts to perform solution (2), which adds a new path. I am not a CMake expert, so this might take a couple tries to get right.
See that the LLVM libs are copied to 'ROOT/lib/', not to `ROOT/llvm/lib/'. + tree --du -h lean-4.0.0-linux + grep -E ' (Init|Lean|Lake|LICENSE|[a-z])' ├── [8.9K] LICENSE ├── [ 67K] LICENSES ├── [8.0M] bin ... ├── [ 46M] include ... ├── [837M] lib (@@@@@@@@) ... │ ├── [712M] lean ... │ │ ├── [5.5M] libInit.a │ │ ├── [ 79M] libLean.a │ │ ├── [5.6M] libleancpp.a │ │ ├── [632K] libleanrt.a │ │ └── [ 61M] libleanshared.so │ ├── [ 13] libLLVM-15.0.1.so -> libLLVM-15.so │ ├── [ 59M] libLLVM-15.so (@@@@@@@@) │ ├── [ 13] libLLVM.so -> libLLVM-15.so ...
This should cause `llvm-config` to spit out the correct paths for includes, libs, etc. This is also very jank, since we are copying the *host* `llvm-config` into the *target release* directory. This is OK for testing, but we need to fix this hack, or do something else before release.
This reverts commit 3f969ba.
This is the last commit before I go to bed, I promise. I hope that adding the path to where we ought to pick up the libraries will allow us to link against the right libraries.
Debugging why we are unable to find LLVM symbols: 2022-10-20T00:51:35.0046819Z /nix/store/9izhv7bayzj8sr7m5n7c4qw1qk2fhq9s-binutils-2.38/bin/ld: /home/runner/work/lean4/lean4/build/stage0/lib/lean/libleanshared.so: undefined reference to `LLVMGetTargetFromTriple' 2022-10-20T00:51:35.0047692Z /nix/store/9izhv7bayzj8sr7m5n7c4qw1qk2fhq9s-binutils-2.38/bin/ld: /home/runner/work/lean4/lean4/build/stage0/lib/lean/libleanshared.so: undefined reference to `LLVMLinkModules2' 2022-10-20T00:51:35.0049782Z /nix/store/9izhv7bayzj8sr7m5n7c4qw1qk2fhq9s-binutils-2.38/bin/ld: /home/runner/work/lean4/lean4/build/stage0/lib/lean/libleanshared.so: undefined reference to `LLVMGetBasicBlockParent' 2022-10-20T00:51:35.0052435Z /nix/store/9izhv7bayzj8sr7m5n7c4qw1qk2fhq9s-binutils-2.38/bin/ld: /home/runner/work/lean4/lean4/build/stage0/lib/lean/libleanshared.so: undefined reference to `LLVMGetDefaultTargetTriple'
For whatever reason, nix believes the llvm-config is that of llvm-11:
Don't use the binary `llvm-config`, instead use LLVM's cmake files to pick up libraries and includes. This ought to be much more stable than running binaries.
convert cmake's semicolon separated list of libraries to appropriate ldflags. This should give us a working link against LLVM without ever needing to invoke 'llvm-config'. Or so the theory goes.
Find the correct names by cross-referencing 'llvm-config --components' and the contents of the directory 'llvm-build/lib/'
I am unsure what to do about the linux/linux debug builds, since they have an ancient version of LLVM that doesn't ship all the targets we want. Do we disable LLVM builds on these configurations? To we update the 'nix-shell' to have a more up-to-date version of LLVM?
Sound over-approximation. If we still have linking errors, then I shall be sad.
This appears to solve the linking problems, for reasons that are unknown to me.
bollu
force-pushed
the
master
branch
3 times, most recently
from
9af0d1a
to
1d855cb
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.