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
This commit is contained in:
Sebastian Ullrich
GitHub
parent
d6c30a8a0a
commit
791bba0091
5 changed files with 113 additions and 101 deletions
15
.github/workflows/ci.yml
vendored
15
.github/workflows/ci.yml
vendored
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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/<target-triple>/' and 'llvm/include/<target-triple>/'
|
||||
# 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/<target-triple>/' and 'llvm/include/<target-triple>/'
|
||||
# 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
|
||||
|
|
|
|||
|
|
@ -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")
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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<LLVMBasicBlockRef>(s);
|
||||
}
|
||||
|
||||
/* TODO: update to new pass manager
|
||||
|
||||
// == LLVM <-> Lean: PassManagerRef ==
|
||||
static inline size_t PassManager_to_lean(LLVMPassManagerRef s) {
|
||||
return reinterpret_cast<size_t>(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<LLVMPassManagerBuilderRef>(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 */) {
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue