Zulip Chat Archive

Stream: general

Topic: Building lean from source with DLLVM=ON

Ahmed Zaki (Jan 16 2024 at 16:20):

Hi, I am trying to build lean4 from source in order to get bc generation working. I build LLVM 15 and I tried to set the location of llvm-config when running cmake but I still get an error when running make.

cmake -DLLVM=ON -DLLVM_CONFIG=/home/user/llvm-project-15.0.7.src/build/bin/llvm-config -DCMAKE_CXX_COMPILER=/home/user/llvm-project-15.0.7.src/build/bin/clang++ -DCMAKE_C_COMPILER=/home/user/llvm-project-15.0.7.src/build/bin/clang ../..

The error is

CMake Error at runtime/CMakeLists.txt:22 (message):
  building 'lean.h.bc', need CMAKE_CXX_COMPILER_ID to match Clang to build
  LLVM bitcode file of Lean runtime.

Any idea whats wrong here ?

Henrik Böving (Jan 16 2024 at 16:33):

I usually compile with the env vars CC and CXX set to clang and clang++ respectively, that works without issues.

Henrik Böving (Jan 16 2024 at 16:33):

Note that the generated LLVM IR is currently worse than what you get from C code performance wise so unless you have a good reason to use the LLVM backend you probably do not want to right now

Ahmed Zaki (Jan 16 2024 at 16:39):

Thanks ! For some reason even using the env vars didn't do it and I still get the same error. I am using LLVM 15.0.0.7 and I built that , not sure if there is a specific config of LLVM 15 that needs to be set ? I do need the IR but not for performance reasons I just want to see what the IR looks like for some cases.

Henrik Böving (Jan 16 2024 at 16:48):

I just set it up with this: cmake -DLLVM=ON -DLLVM_CONFIG=$(which llvm-config) ../../ where I included the bin of my llvm installation int he path and set the CXX/CC to the values above and it worked without issues for me.

The LLVM IR that we generate is almost in 1:1 correspondence with the C output which in turn is a straight forward translation from the internal IR that you can view with set_option trace.compiler.ir.result true if you want to.

Ahmed Zaki (Jan 16 2024 at 17:12):

Thank you ! Turns out I had a cacheing issue that caused it to fail building. All good now :) . Thank you for the pointer to view the internal IR. That's very useful ! So I can do that on per project basis without having to build lean with LLVM=ON ?

Henrik Böving (Jan 16 2024 at 17:16):

the IR that I am referring to with the tracing option is not LLVM IR, it is the internal compiler IR that is generic across all backends so yes you can always use this.

Henrik Böving (Jan 16 2024 at 17:19):

Can you tell me what you wish to do with the IR exactly? Maybe I can provide further pointers in that case.

Ahmed Zaki (Jan 16 2024 at 17:23):

I am looking at doing some program analysis using the IR

Sebastian Ullrich (Jan 17 2024 at 15:37):

Henrik Böving said:

Note that the generated LLVM IR is currently worse than what you get from C code performance wise so unless you have a good reason to use the LLVM backend you probably do not want to right now

@Henrik Böving Do we have a tracking issue for this?

Henrik Böving (Jan 17 2024 at 17:34):

Sebastian Ullrich said:

Henrik Böving said:

Note that the generated LLVM IR is currently worse than what you get from C code performance wise so unless you have a good reason to use the LLVM backend you probably do not want to right now

Henrik Böving Do we have a tracking issue for this?

I don't think so, when I originally discovered this it seemed like some failure of LLVM to do inlining (the generated IR itself is okay, it's what happens with it after -O3) and I planned to fix it with @Siddharth Bhat but then a ton of stuff happen on Siddharth's side so its still not fixed :(. Do you want me to open one?

Sebastian Ullrich (Jan 17 2024 at 17:37):

Yes please!

Henrik Böving (Jan 17 2024 at 18:16):

https://github.com/leanprover/lean4/issues/3192 This is a rather rudimentary description but I recently switched laptops so I dont have the entire example at hand right now.