forked from leanprover/lean4
-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
24 oct llvm backend files via llvm config #14
Open
bollu
wants to merge
25
commits into
master
Choose a base branch
from
24-oct-llvm-backend-files-via-llvm-config
base: master
Could not load branches
Branch not found: {{ refName }}
Could not load tags
Nothing to show
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
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:
Thanks for your contribution! Please make sure to follow our Commit Convention. |
This should fix the path issues we have. Currently, `llvm-config` spits out paths like: > 2022-10-24T14:21:30.1620266Z TODO: change to debug > llvm-config: libdir '/home/runner/work/lean4/lean4/build/llvm-host/lib' > ldflags '-L/home/ runner/work/lean4/lean4/build/llvm-host/lib' > cxxflags: -I/home/runner/work/lean4/lean4/build/llvm-host/ > includedir: /home/runner/work/lean4/lean4/build/llvm-host/include
Run lean-*/bin/leanc --print-cflags + lean-4.0.0-linux_aarch64/bin/leanc --print-cflags /home/runner/work/_temp/c5e995cd-aa15-4a4a-a4d9-e97601ae4409: line 1: lean-4.0.0-linux_aarch64/bin/leanc: cannot execute binary file: Exec format error See that the other option Run lean-*/bin/* || true also skips this on `aarch64`
bollu
force-pushed
the
master
branch
2 times, most recently
from
July 27, 2023 17:21
84ffecb
to
9af0d1a
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.