Add LLVM bindings to Lean4 #10
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
bollu
force-pushed
the
19-aug-llvm-backend-files
branch
4 times, most recently
from
a3719f6
to
ec7b19b
Compare
bollu
force-pushed
the
19-aug-llvm-backend-files
branch
2 times, most recently
from
e2a4515
to
97b9c2e
Compare
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
bollu
force-pushed
the
19-aug-llvm-backend-files
branch
from
1e5e4fc
to
252af0e
Compare
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:
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This was changed in building the uber large LLVM backend patch on accident.
This reduces ambiguity and making casing consistent.
This should provide enough info about 'leanshared' cration when we want it warranted, while always printing out key things like LLVM config and LLVM flags that's super duper useful to view at a glance.
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
We now use structure Foo (ctx: Context) where private mk :: ptr : USize Also fix the whitespace issue -- 'f(var: T)' → 'f (var : T)'
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.