From 791bba0091134bfc0bc3c94fb688c84fc59c90b7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 21 Apr 2025 19:18:18 +0200 Subject: [PATCH] feat: LLVM 15 -> 19 (#6063) This PR updates the version of LLVM and clang used by and shipped with Lean to 19.1.2 Fixes #5649 --- .github/workflows/ci.yml | 15 ++- script/prepare-llvm-linux.sh | 16 ++- src/CMakeLists.txt | 4 +- src/Lean/Compiler/IR/LLVMBindings.lean | 4 + src/library/compiler/llvm.cpp | 175 +++++++++++++------------ 5 files changed, 113 insertions(+), 101 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 63ea783340..1dc4be497f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -139,20 +139,21 @@ jobs: let large = ${{ github.repository == 'leanprover/lean4' }}; const isPr = "${{ github.event_name }}" == "pull_request"; let matrix = [ + /* TODO: to be updated to new LLVM { "name": "Linux LLVM", "os": "ubuntu-latest", "release": false, "check-level": 2, "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}", - "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst", + "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst", "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*", "binary-check": "ldd -v", // foreign code may be linked against more recent glibc // reverse-ffi needs to be updated to link to LLVM libraries "CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'", "CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config" - }, + }, */ { // portable release build: use channel with older glibc (2.26) "name": "Linux release", @@ -160,7 +161,7 @@ jobs: "release": true, "check-level": 0, "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}", - "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst", + "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst", "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*", "binary-check": "ldd -v", // foreign code may be linked against more recent glibc @@ -207,7 +208,7 @@ jobs: "release": true, "check-level": 2, "shell": "bash -euxo pipefail {0}", - "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst", + "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst", "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*", "binary-check": "otool -L", "tar": "gtar" // https://github.com/actions/runner-images/issues/2619 @@ -218,7 +219,7 @@ jobs: "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64", "release": true, "shell": "bash -euxo pipefail {0}", - "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst", + "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst", "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*", "binary-check": "otool -L", "tar": "gtar", // https://github.com/actions/runner-images/issues/2619 @@ -239,7 +240,7 @@ jobs: "CMAKE_OPTIONS": "-G \"Unix Makefiles\"", // for reasons unknown, interactivetests are flaky on Windows "CTEST_OPTIONS": "--repeat until-pass:2", - "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst", + "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst", "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*", "binary-check": "ldd" }, @@ -250,7 +251,7 @@ jobs: "release": true, "check-level": 2, "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}", - "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst", + "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst", "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*" }, // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index ac634aee4e..767e3547cb 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -1,5 +1,5 @@ #!/usr/bin/env bash -set -uo pipefail +set -euxo pipefail # run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in # ``` @@ -14,6 +14,7 @@ set -uo pipefail else ln -s llvm llvm-host fi +mkdir -p stage0/lib mkdir -p stage1/{bin,lib,lib/glibc,include/clang} CP="cp -d" # preserve symlinks # a C compiler! @@ -25,6 +26,8 @@ cp -L llvm/bin/llvm-ar stage1/bin/ # dependencies of the above $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/ $CP $ZLIB/lib/libz.so* stage1/lib/ +# also copy USE_LLVM deps into stage 0 +$CP llvm/lib/libLLVM*.so* $ZLIB/lib/libz.so* stage0/lib/ # general clang++ dependency, breaks cross-library C++ exceptions if linked statically $CP $GCC_LIB/lib/libgcc_s.so* stage1/lib/ # bundle libatomic (referenced by LLVM >= 15, and required by the lean executable to run) @@ -39,18 +42,18 @@ $CP $GLIBC/lib/*crt* stage1/lib/ # runtime (cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1) $CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a $LIBUV/lib/libuv.a stage1/lib/ -# LLVM 15 appears to ship the dependencies in 'llvm/lib//' and 'llvm/include//' -# but clang-15 that we use to compile is linked against 'llvm/lib/' and 'llvm/include' +# LLVM 19 appears to ship the dependencies in 'llvm/lib//' and 'llvm/include//' +# but clang-19 that we use to compile is linked against 'llvm/lib/' and 'llvm/include' # https://github.com/llvm/llvm-project/issues/54955 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* llvm/lib/ $CP llvm-host/lib/*/lib{c++,c++abi,unwind}.* llvm-host/lib/ # libc++ headers are looked up in the host compiler's root, so copy over target-specific includes -$CP -r llvm/include/*-*-* llvm-host/include/ +$CP -r llvm/include/*-*-* llvm-host/include/ || true # glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)! $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc # libpthread_nonshared.a must be linked in order to be able to use `pthread_atfork(3)`. LibUV uses this function. $CP $GLIBC/lib/libpthread_nonshared.a stage1/lib/glibc -for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done +for f in $GLIBC/lib/{ld,lib{c,dl,m,rt,pthread}}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done OPTIONS=() echo -n " -DLEAN_STANDALONE=ON" echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'" @@ -64,7 +67,8 @@ fi # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers), # but do not change sysroot so users can still link against system libs echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang" -echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'" +# ld.so is usually included by the libc.so linker script but we discard those +echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic ROOT/lib/glibc/ld.so -Wl,--no-as-needed -fuse-ld=lld'" # when not using the above flags, link GMP dynamically/as usual echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'" # do not set `LEAN_CC` for tests diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index abebbd9cbc..2e1498d9b8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -365,8 +365,8 @@ if(LLVM) execute_process(COMMAND ${LLVM_CONFIG} --version COMMAND_ERROR_IS_FATAL ANY OUTPUT_VARIABLE LLVM_CONFIG_VERSION ECHO_OUTPUT_VARIABLE OUTPUT_STRIP_TRAILING_WHITESPACE) string(REGEX MATCH "^[0-9]*" LLVM_CONFIG_MAJOR_VERSION ${LLVM_CONFIG_VERSION}) message(STATUS "Found 'llvm-config' at '${LLVM_CONFIG}' with version '${LLVM_CONFIG_VERSION}', major version '${LLVM_CONFIG_MAJOR_VERSION}'") - if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "15") - message(FATAL_ERROR "Unable to find llvm-config version 15. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'") + if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "19") + message(FATAL_ERROR "Unable to find llvm-config version 19. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'") endif() # -DLEAN_LLVM is used to conditionally compile Lean features that depend on LLVM string(APPEND CMAKE_CXX_FLAGS " -D LEAN_LLVM") diff --git a/src/Lean/Compiler/IR/LLVMBindings.lean b/src/Lean/Compiler/IR/LLVMBindings.lean index b58aa02818..0d5e63a81f 100644 --- a/src/Lean/Compiler/IR/LLVMBindings.lean +++ b/src/Lean/Compiler/IR/LLVMBindings.lean @@ -63,6 +63,7 @@ structure Module (ctx : Context) where private mk :: ptr : USize instance : Nonempty (Module ctx) := ⟨{ ptr := default }⟩ +/- structure PassManager (ctx : Context) where private mk :: ptr : USize instance : Nonempty (PassManager ctx) := ⟨{ ptr := default }⟩ @@ -70,6 +71,7 @@ instance : Nonempty (PassManager ctx) := ⟨{ ptr := default }⟩ structure PassManagerBuilder (ctx : Context) where private mk :: ptr : USize instance : Nonempty (PassManagerBuilder ctx) := ⟨{ ptr := default }⟩ +-/ structure Target (ctx : Context) where private mk :: ptr : USize @@ -313,6 +315,7 @@ opaque createTargetMachine (target : Target ctx) (tripleStr : @&String) (cpu : @ @[extern "lean_llvm_target_machine_emit_to_file"] opaque targetMachineEmitToFile (targetMachine : TargetMachine ctx) (module : Module ctx) (filepath : @&String) (codegenType : LLVM.CodegenFileType) : BaseIO Unit +/- @[extern "lean_llvm_create_pass_manager"] opaque createPassManager : BaseIO (PassManager ctx) @@ -333,6 +336,7 @@ opaque PassManagerBuilder.setOptLevel (pmb : PassManagerBuilder ctx) (optLevel : @[extern "lean_llvm_pass_manager_builder_populate_module_pass_manager"] opaque PassManagerBuilder.populateModulePassManager (pmb : PassManagerBuilder ctx) (pm : PassManager ctx): BaseIO Unit +-/ @[extern "lean_llvm_dispose_target_machine"] opaque disposeTargetMachine (tm : TargetMachine ctx) : BaseIO Unit diff --git a/src/library/compiler/llvm.cpp b/src/library/compiler/llvm.cpp index f75bdb7d4a..892502a546 100644 --- a/src/library/compiler/llvm.cpp +++ b/src/library/compiler/llvm.cpp @@ -26,8 +26,8 @@ Lean's IR. #include "llvm-c/Target.h" #include "llvm-c/TargetMachine.h" #include "llvm-c/Types.h" -#include "llvm-c/Transforms/PassBuilder.h" -#include "llvm-c/Transforms/PassManagerBuilder.h" +//#include "llvm-c/Transforms/PassBuilder.h" +//#include "llvm-c/Transforms/PassManagerBuilder.h" #endif // This is mostly boilerplate, suppress warnings @@ -135,6 +135,8 @@ static inline LLVMBasicBlockRef lean_to_BasicBlock(size_t s) { return reinterpret_cast(s); } +/* TODO: update to new pass manager + // == LLVM <-> Lean: PassManagerRef == static inline size_t PassManager_to_lean(LLVMPassManagerRef s) { return reinterpret_cast(s); @@ -152,6 +154,7 @@ static inline size_t PassManagerBuilder_to_lean(LLVMPassManagerBuilderRef s) { static inline LLVMPassManagerBuilderRef lean_to_PassManagerBuilder(size_t s) { return reinterpret_cast(s); } +*/ // == LLVM <-> Lean: AttributeRef == static inline size_t Attribute_to_lean(LLVMAttributeRef s) { @@ -1184,90 +1187,90 @@ extern "C" LEAN_EXPORT lean_object *lean_llvm_target_machine_emit_to_file(size_t #endif // LEAN_LLVM } -extern "C" LEAN_EXPORT lean_object *lean_llvm_create_pass_manager(size_t ctx, - lean_object * /* w */) { -#ifndef LEAN_LLVM - lean_always_assert( - false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " - "the LLVM backend function.")); -#else - return lean_io_result_mk_ok(lean_box_usize(PassManager_to_lean(LLVMCreatePassManager()))); -#endif // LEAN_LLVM -} - -extern "C" LEAN_EXPORT lean_object *lean_llvm_run_pass_manager(size_t ctx, size_t pm, size_t mod, - lean_object * /* w */) { -#ifndef LEAN_LLVM - lean_always_assert( - false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " - "the LLVM backend function.")); -#else - int is_error = LLVMRunPassManager(lean_to_PassManager(pm), lean_to_Module(mod)); - return lean_io_result_mk_ok(lean_box(0)); -#endif // LEAN_LLVM -} - -extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_pass_manager(size_t ctx, size_t pm, - lean_object * /* w */) { -#ifndef LEAN_LLVM - lean_always_assert( - false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " - "the LLVM backend function.")); -#else - LLVMDisposePassManager(lean_to_PassManager(pm)); - return lean_io_result_mk_ok(lean_box(0)); -#endif // LEAN_LLVM -} - -extern "C" LEAN_EXPORT lean_object *lean_llvm_create_pass_manager_builder(size_t ctx, - lean_object * /* w */) { -#ifndef LEAN_LLVM - lean_always_assert( - false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " - "the LLVM backend function.")); -#else - return lean_io_result_mk_ok(lean_box_usize(PassManagerBuilder_to_lean(LLVMPassManagerBuilderCreate()))); -#endif // LEAN_LLVM -} - - -extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_pass_manager_builder(size_t ctx, size_t pmb, - lean_object * /* w */) { -#ifndef LEAN_LLVM - lean_always_assert( - false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " - "the LLVM backend function.")); -#else - LLVMPassManagerBuilderDispose(lean_to_PassManagerBuilder(pmb)); - return lean_io_result_mk_ok(lean_box(0)); -#endif // LEAN_LLVM -} - - -extern "C" LEAN_EXPORT lean_object *lean_llvm_pass_manager_builder_set_opt_level(size_t ctx, size_t pmb, unsigned opt_level, - lean_object * /* w */) { -#ifndef LEAN_LLVM - lean_always_assert( - false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " - "the LLVM backend function.")); -#else - LLVMPassManagerBuilderSetOptLevel(lean_to_PassManagerBuilder(pmb), opt_level); - return lean_io_result_mk_ok(lean_box(0)); -#endif // LEAN_LLVM -} - - -extern "C" LEAN_EXPORT lean_object *lean_llvm_pass_manager_builder_populate_module_pass_manager(size_t ctx, size_t pmb, size_t pm, - lean_object * /* w */) { -#ifndef LEAN_LLVM - lean_always_assert( - false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " - "the LLVM backend function.")); -#else - LLVMPassManagerBuilderPopulateModulePassManager(lean_to_PassManagerBuilder(pmb), lean_to_PassManager(pm)); - return lean_io_result_mk_ok(lean_box(0)); -#endif // LEAN_LLVM -} +//extern "C" LEAN_EXPORT lean_object *lean_llvm_create_pass_manager(size_t ctx, +// lean_object * /* w */) { +//#ifndef LEAN_LLVM +// lean_always_assert( +// false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " +// "the LLVM backend function.")); +//#else +// return lean_io_result_mk_ok(lean_box_usize(PassManager_to_lean(LLVMCreatePassManager()))); +//#endif // LEAN_LLVM +//} +// +//extern "C" LEAN_EXPORT lean_object *lean_llvm_run_pass_manager(size_t ctx, size_t pm, size_t mod, +// lean_object * /* w */) { +//#ifndef LEAN_LLVM +// lean_always_assert( +// false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " +// "the LLVM backend function.")); +//#else +// int is_error = LLVMRunPassManager(lean_to_PassManager(pm), lean_to_Module(mod)); +// return lean_io_result_mk_ok(lean_box(0)); +//#endif // LEAN_LLVM +//} +// +//extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_pass_manager(size_t ctx, size_t pm, +// lean_object * /* w */) { +//#ifndef LEAN_LLVM +// lean_always_assert( +// false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " +// "the LLVM backend function.")); +//#else +// LLVMDisposePassManager(lean_to_PassManager(pm)); +// return lean_io_result_mk_ok(lean_box(0)); +//#endif // LEAN_LLVM +//} +// +//extern "C" LEAN_EXPORT lean_object *lean_llvm_create_pass_manager_builder(size_t ctx, +// lean_object * /* w */) { +//#ifndef LEAN_LLVM +// lean_always_assert( +// false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " +// "the LLVM backend function.")); +//#else +// return lean_io_result_mk_ok(lean_box_usize(PassManagerBuilder_to_lean(LLVMPassManagerBuilderCreate()))); +//#endif // LEAN_LLVM +//} +// +// +//extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_pass_manager_builder(size_t ctx, size_t pmb, +// lean_object * /* w */) { +//#ifndef LEAN_LLVM +// lean_always_assert( +// false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " +// "the LLVM backend function.")); +//#else +// LLVMPassManagerBuilderDispose(lean_to_PassManagerBuilder(pmb)); +// return lean_io_result_mk_ok(lean_box(0)); +//#endif // LEAN_LLVM +//} +// +// +//extern "C" LEAN_EXPORT lean_object *lean_llvm_pass_manager_builder_set_opt_level(size_t ctx, size_t pmb, unsigned opt_level, +// lean_object * /* w */) { +//#ifndef LEAN_LLVM +// lean_always_assert( +// false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " +// "the LLVM backend function.")); +//#else +// LLVMPassManagerBuilderSetOptLevel(lean_to_PassManagerBuilder(pmb), opt_level); +// return lean_io_result_mk_ok(lean_box(0)); +//#endif // LEAN_LLVM +//} +// +// +//extern "C" LEAN_EXPORT lean_object *lean_llvm_pass_manager_builder_populate_module_pass_manager(size_t ctx, size_t pmb, size_t pm, +// lean_object * /* w */) { +//#ifndef LEAN_LLVM +// lean_always_assert( +// false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " +// "the LLVM backend function.")); +//#else +// LLVMPassManagerBuilderPopulateModulePassManager(lean_to_PassManagerBuilder(pmb), lean_to_PassManager(pm)); +// return lean_io_result_mk_ok(lean_box(0)); +//#endif // LEAN_LLVM +//} extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_target_machine(size_t ctx, size_t tm, lean_object * /* w */) {