max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: LLVM backend (#1837)

Browse source
This commit is contained in:
Siddharth 2022-12-30 11:45:30 +00:00 • committed by GitHub
parent d19033e443
commit b6eb780144
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
21 changed files with 2309 additions and 753 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
nix/bootstrap.nix
View file

@ -17,7 +17,7 @@ rec {
'';
} // args // {
src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DLLVM=ON" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
preConfigure = args.preConfigure or "" + ''
# ignore absence of submodule
sed -i 's!lake/Lake.lean!!' CMakeLists.txt
@ -45,12 +45,12 @@ rec {
leancpp = buildCMake {
name = "leancpp";
src = ../src;
buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" "runtime_bc" ];
buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" ];
installPhase = ''
mkdir -p $out
mv lib/ $out/
mv shell/CMakeFiles/shell.dir/lean.cpp.o $out/lib
mv runtime/libleanrt_initial-exec.a runtime/lean.h.bc $out/lib
mv runtime/libleanrt_initial-exec.a $out/lib
'';
};
stage0 = args.stage0 or (buildCMake {

17
src/CMakeLists.txt
View file

@ -264,10 +264,14 @@ if(LLVM)
endif()
# check that we have 'llvm-config' version.
message(STATUS "Executing 'llvm-config --version' at '${LLVM_CONFIG}' to check configuration.")
execute_process(COMMAND ${LLVM_CONFIG} --version COMMAND_ERROR_IS_FATAL ANY)
message(STATUS "Found 'llvm-config' as ${LLVM_CONFIG}")
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}'")
endif()
# -DLEAN_LLVM is used to conditionally compile Lean features that depend on LLVM
string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_LLVM")
string(APPEND CMAKE_CXX_FLAGS " -D LEAN_LLVM")
execute_process(COMMAND ${LLVM_CONFIG} --ldflags OUTPUT_VARIABLE LLVM_CONFIG_LDFLAGS OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND ${LLVM_CONFIG} --libs OUTPUT_VARIABLE LLVM_CONFIG_LIBS OUTPUT_STRIP_TRAILING_WHITESPACE)
@ -323,7 +327,7 @@ if(LLVM)
# we need the path to be `-Lllvm/lib/libLLVM`. Thus, we perform this replacement here.
string(APPEND LEANSHARED_LINKER_FLAGS " -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}")
string(REPLACE "llvm-host" "llvm" LEANSHARED_LINKER_FLAGS ${LEANSHARED_LINKER_FLAGS})
set(APPEND LEAN_EXTRA_CXX_FLAGS " -I${LLVM_CONFIG_INCLUDEDIR}")
string(APPEND CMAKE_CXX_FLAGS " -I${LLVM_CONFIG_INCLUDEDIR}")
string(REPLACE "llvm-host" "llvm" LEAN_EXTRA_CXX_FLAGS ${LEAN_EXTRA_CXX_FLAGS})
message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${LEAN_EXTR_CXX_FLAGS}'")
endif()
@ -461,6 +465,11 @@ if(${STAGE} GREATER 1)
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleanrt.a" "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleancpp.a" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
add_dependencies(leancpp copy-leancpp)
if(LLVM)
add_custom_target(copy-lean-h-bc
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/lean.h.bc" "${CMAKE_BINARY_DIR}/lib/lean/lean.h.bc")
add_dependencies(leancpp copy-lean-h-bc)
endif()
else()
add_subdirectory(runtime)

1
src/Lean/Compiler/IR.lean
View file

@ -19,7 +19,6 @@ import Lean.Compiler.IR.ExpandResetReuse
import Lean.Compiler.IR.UnboxResult
import Lean.Compiler.IR.ElimDeadBranches
import Lean.Compiler.IR.EmitC
import Lean.Compiler.IR.EmitLLVM
import Lean.Compiler.IR.CtorLayout
import Lean.Compiler.IR.Sorry

1511
src/Lean/Compiler/IR/EmitLLVM.lean
View file

File diff suppressed because it is too large Load diff

29
src/Lean/Compiler/IR/LLVMBindings.lean
View file

@ -73,6 +73,9 @@ structure Value (ctx : Context) where
private mk :: ptr : USize
instance : Nonempty (Value ctx) := ⟨{ ptr := default }⟩
@[extern "lean_llvm_initialize"]
opaque llvmInitialize : BaseIO (Unit)
@[extern "lean_llvm_create_context"]
opaque createContext : BaseIO (Context)
@ -112,6 +115,9 @@ opaque voidType (ctx : Context) : BaseIO (LLVMType ctx)
@[extern "lean_llvm_int_type_in_context"]
opaque intTypeInContext (ctx : Context) (width : UInt64) : BaseIO (LLVMType ctx)
@[extern "lean_llvm_opaque_pointer_type_in_context"]
opaque opaquePointerTypeInContext (ctx : Context) (addrspace: UInt64 := 0) : BaseIO (LLVMType ctx)
@[extern "lean_llvm_float_type_in_context"]
opaque floatTypeInContext (ctx : Context) : BaseIO (LLVMType ctx)
@ -146,8 +152,8 @@ opaque appendBasicBlockInContext (ctx : Context) (fn : Value ctx) (name : @&St
@[extern "lean_llvm_position_builder_at_end"]
opaque positionBuilderAtEnd (builder : Builder ctx) (bb : BasicBlock ctx) : BaseIO Unit
@[extern "lean_llvm_build_call"]
opaque buildCall (builder : Builder ctx) (fn : Value ctx) (args : @&Array (Value ctx)) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_call2"]
opaque buildCall2 (builder : Builder ctx) (ty: LLVMType ctx) (fn : Value ctx) (args : @&Array (Value ctx)) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_set_tail_call"]
opaque setTailCall (fn : Value ctx) (istail : Bool) : BaseIO Unit
@ -161,8 +167,8 @@ opaque buildBr (builder : Builder ctx) (bb : BasicBlock ctx) : BaseIO (Value ctx
@[extern "lean_llvm_build_alloca"]
opaque buildAlloca (builder : Builder ctx) (ty : LLVMType ctx) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_load"]
opaque buildLoad (builder : Builder ctx) (val : Value ctx) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_load2"]
opaque buildLoad2 (builder : Builder ctx) (ty: LLVMType ctx) (val : Value ctx) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_store"]
opaque buildStore (builder : Builder ctx) (val : Value ctx) (store_loc_ptr : Value ctx) : BaseIO Unit
@ -173,14 +179,11 @@ opaque buildRet (builder : Builder ctx) (val : Value ctx) : BaseIO (Value ctx)
@[extern "lean_llvm_build_unreachable"]
opaque buildUnreachable (builder : Builder ctx) : BaseIO (Value ctx)
@[extern "lean_llvm_build_gep"]
opaque buildGEP (builder : Builder ctx) (base : Value ctx) (ixs : @&Array (Value ctx)) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_gep2"]
opaque buildGEP2 (builder : Builder ctx) (ty: LLVMType ctx) (base : Value ctx) (ixs : @&Array (Value ctx)) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_inbounds_gep"]
opaque buildInBoundsGEP (builder : Builder ctx) (base : Value ctx) (ixs : @&Array (Value ctx)) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_pointer_cast"]
opaque buildPointerCast (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_inbounds_gep2"]
opaque buildInBoundsGEP2 (builder : Builder ctx) (ty: LLVMType ctx) (base : Value ctx) (ixs : @&Array (Value ctx)) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_sext"]
opaque buildSext (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : @&String := "") : BaseIO (Value ctx)
@ -198,10 +201,10 @@ opaque buildSwitch (builder : Builder ctx) (val : Value ctx) (elseBB : BasicBloc
opaque buildPtrToInt (builder : Builder ctx) (ptr : Value ctx) (destTy : LLVMType ctx) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_mul"]
opaque buildMul (builder : Builder ctx) (x y : Value ctx) (name : @&String) : BaseIO (Value ctx)
opaque buildMul (builder : Builder ctx) (x y : Value ctx) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_add"]
opaque buildAdd (builder : Builder ctx) (x y : Value ctx) (name : @&String) : BaseIO (Value ctx)
opaque buildAdd (builder : Builder ctx) (x y : Value ctx) (name : @&String := "") : BaseIO (Value ctx)
@[extern "lean_llvm_build_sub"]
opaque buildSub (builder : Builder ctx) (x y : Value ctx) (name : @&String := "") : BaseIO (Value ctx)

2
src/Lean/Data/HashMap.lean
View file

@ -31,7 +31,7 @@ namespace HashMapImp
variable {α : Type u} {β : Type v}
/- Remark: we use a C implementation because this function is performance critical. -/
@[extern c inline "(size_t)(#2) & (lean_unbox(#1) - 1)"]
@[extern "lean_data_hashmap_mk_idx"]
private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize // u.toNat < sz } :=
-- TODO: avoid `if` in the reference implementation
let u := hash.toUSize &&& (sz.toUSize - 1)

5
src/include/lean/lean.h
View file

@ -1922,6 +1922,11 @@ static inline uint8_t lean_float_decLe(double a, double b) { return a <= b; }
static inline uint8_t lean_float_decLt(double a, double b) { return a < b; }
static inline double lean_uint64_to_float(uint64_t a) { return (double) a; }
/* Efficient C implementations of defns used by the compiler */
static inline size_t lean_data_hashmap_mk_idx(lean_object* sz, uint64_t hash) {
return (size_t)(hash & (lean_unbox(sz) - 1));
}
#ifdef __cplusplus
}
#endif

1
src/library/compiler/ir.h
View file

@ -37,6 +37,7 @@ void test(decl const & d);
environment compile(environment const & env, options const & opts, comp_decls const & decls);
environment add_extern(environment const & env, name const & fn);
string_ref emit_c(environment const & env, name const & mod_name);
void emit_llvm(environment const & env, name const & mod_name, std::string const &filepath);
}
void initialize_ir();
void finalize_ir();

1368
src/library/compiler/llvm.cpp
View file

File diff suppressed because it is too large Load diff

7
src/runtime/CMakeLists.txt
View file

@ -25,10 +25,11 @@ if(LLVM)
# generate LLVM IR for `static inline` definitions in lean.h for the LLVM backend
string(REPLACE "static inline" "__attribute__((always_inline))" LEAN_H "${LEAN_H}")
file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c" "${LEAN_H}")
message("Generating LLVM bitcode file for Lean runtime at '${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/lean.h.bc'")
add_custom_command(
OUTPUT lean.h.bc
OUTPUT ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/lean.h.bc
DEPENDS ${RUNTIME_OBJS} ${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c
COMMAND bash -ec "${CMAKE_BINARY_DIR}/leanc.sh ${LEANC_OPTS} -I$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -I> -c ${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c -emit-llvm -o ${CMAKE_CURRENT_BINARY_DIR}/lean.h.bc"
COMMAND bash -ec "${CMAKE_BINARY_DIR}/leanc.sh ${LEANC_OPTS} -I$<JOIN:$<TARGET_PROPERTY:leanrt_initial-exec,INCLUDE_DIRECTORIES>, -I> -c ${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c -emit-llvm -o ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/lean.h.bc"
VERBATIM)
add_custom_target(runtime_bc DEPENDS lean.h.bc)
add_custom_target(runtime_bc DEPENDS ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/lean.h.bc)
endif()

42
src/util/shell.cpp
View file

@ -56,10 +56,6 @@ Author: Leonardo de Moura
#include <dlfcn.h>
#endif
#if defined(LEAN_LLVM)
#include <llvm/Support/TargetSelect.h>
#endif
#ifdef _MSC_VER
// extremely simple implementation of getopt.h
enum arg_opt { no_argument, required_argument, optional_argument };
@ -173,20 +169,35 @@ using namespace lean; // NOLINT
#define LEAN_SERVER_DEFAULT_MAX_HEARTBEAT 100000
#endif
extern "C" void *initialize_Lean_Compiler_IR_EmitLLVM(uint8_t builtin,
lean_object *);
extern "C" object *lean_ir_emit_llvm(object *env, object *mod_name,
object *filepath, object *w);
static void display_header(std::ostream & out) {
out << "Lean (version " << get_version_string() << ", " << LEAN_STR(LEAN_BUILD_TYPE) << ")\n";
}
static void display_features(std::ostream & out) {
out << "[";
#if defined(LEAN_LLVM)
out << "LLVM";
#endif
out << "]\n";
}
static void display_help(std::ostream & out) {
display_header(out);
std::cout << "Miscellaneous:\n";
std::cout << " --help -h display this message\n";
std::cout << " --features -f display features compiler provides (eg. LLVM support)\n";
std::cout << " --version -v display version number\n";
std::cout << " --githash display the git commit hash number used to build this binary\n";
std::cout << " --run call the 'main' definition in a file with the remaining arguments\n";
std::cout << " --o=oname -o create olean file\n";
std::cout << " --i=iname -i create ilean file\n";
std::cout << " --c=fname -c name of the C output file\n";
std::cout << " --bc=fname -b name of the LLVM bitcode file\n";
std::cout << " --stdin take input from stdin\n";
std::cout << " --root=dir set package root directory from which the module name of the input file is calculated\n"
<< " (default: current working directory)\n";
@ -237,6 +248,8 @@ static struct option g_long_options[] = {
{"deps-json", no_argument, 0, 'J'},
{"timeout", optional_argument, 0, 'T'},
{"c", optional_argument, 0, 'c'},
{"bc", optional_argument, 0, 'b'},
{"features", optional_argument, 0, 'f'},
{"exitOnPanic", no_argument, 0, 'e'},
#if defined(LEAN_MULTI_THREAD)
{"threads", required_argument, 0, 'j'},
@ -458,10 +471,6 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
#if defined(LEAN_MULTI_THREAD)
num_threads = hardware_concurrency();
#endif
#if defined(LEAN_LLVM)
// Initialize LLVM backends for native code generation.
llvm::InitializeNativeTarget();
#endif
try {
// Remark: This currently runs under `IO.initializing = true`.
@ -476,6 +485,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
optional<std::string> server_in;
std::string native_output;
optional<std::string> c_output;
optional<std::string> llvm_output;
optional<std::string> root_dir;
buffer<string_ref> forwarded_args;
@ -502,10 +512,17 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
case 'h':
display_help(std::cout);
return 0;
case 'f':
display_features(std::cout);
return 0;
case 'c':
check_optarg("c");
c_output = optarg;
break;
case 'b':
check_optarg("b");
llvm_output = optarg;
break;
case 's':
lean::lthread::set_thread_stack_size(
static_cast<size_t>((atoi(optarg) / 4) * 4) * static_cast<size_t>(1024));
@ -727,6 +744,15 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
out.close();
}
if (llvm_output && ok) {
initialize_Lean_Compiler_IR_EmitLLVM(/*builtin*/ false,
lean_io_mk_world());
time_task _("LLVM code generation", opts);
lean::consume_io_result(lean_ir_emit_llvm(
env.to_obj_arg(), (*main_module_name).to_obj_arg(),
lean::string_ref(*llvm_output).to_obj_arg(), lean_io_mk_world()));
}
display_cumulative_profiling_times(std::cerr);
#ifdef LEAN_SMALL_ALLOCATOR

2
tests/bench/.gitignore vendored
View file

@ -1,5 +1,7 @@
*.out
*.lean.c
*.lean.linked.bc
*.lean.linked.bc.o
*.cmi
*.cmx
*.o

7
tests/bench/compile.sh
View file

@ -1,4 +1,9 @@
#!/usr/bin/env bash
source ../common.sh
compile_lean
compile_lean_c_backend
# Then check the LLVM version
if lean_has_llvm_support; then
echo "running LLVM program..."
compile_lean_llvm_backend
fi

12
tests/bench/test_single.sh
View file

@ -1,6 +1,16 @@
#!/usr/bin/env bash
source ../common.sh
compile_lean
# First check the C version actually works...
compile_lean_c_backend
exec_check "./$f.out" $(cat "$f.args")
diff_produced
# Then check the LLVM version
if lean_has_llvm_support; then
echo "running LLVM program..."
rm "./$f.out" || true
compile_lean_llvm_backend
exec_check "./$f.out" $(cat "$f.args")
diff_produced
fi

18
tests/common.sh
View file

@ -20,11 +20,25 @@ f="$1"
shift
[ $# -eq 0 ] || fail "Usage: test_single.sh [-i] test-file.lean"
function compile_lean {
function lean_has_llvm_support {
lean --features | grep -q "LLVM"
}
function compile_lean_c_backend {
lean --c="$f.c" "$f" || fail "Failed to compile $f into C file"
leanc -O3 -DNDEBUG -o "$f.out" "$@" "$f.c" || fail "Failed to compile C file $f.c"
}
function compile_lean_llvm_backend {
set -o xtrace
rm "*.ll" || true # remove debugging files.
rm "*.bc" || true # remove bitcode files
rm "*.o" || true # remove object files
lean --bc="$f.linked.bc" "$f" || fail "Failed to compile $f into bitcode file"
leanc -o "$f.out" "$@" "$f.linked.bc.o" || fail "Failed to link object file '$f.linked.bc.o'"
set +o xtrace
}
function exec_capture {
# mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them
LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g' > "$f.produced.out"
@ -46,7 +60,7 @@ function exec_check {
function diff_produced {
if test -f "$f.expected.out"; then
if $DIFF -au --strip-trailing-cr -I "executing external script" "$f.expected.out" "$f.produced.out"; then
exit 0
:
else
echo "ERROR: file $f.produced.out does not match $f.expected.out"
if [ $INTERACTIVE == "yes" ]; then

4
tests/compiler/.gitignore vendored
View file

@ -1,3 +1,5 @@
*.lean.out
*.lean.c
test_flags.sh
*.lean.linked.bc
*.lean.linked.bc.o
test_flags.sh

12
tests/compiler/computedFieldsExtern.lean
View file

@ -1,12 +0,0 @@
inductive Exp
| var (i : Nat)
| app (a b : Exp)
with
@[computed_field, extern c inline "(lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*)) + 40)"]
hash : Exp → UInt64
| .var i => Hashable.hash i
| .app a b => a.hash + b.hash
def main : IO Unit := do
-- should be 30 + 3*40 = 150
IO.println <| Exp.hash (.app (.var 10) (.var 20))

1
tests/compiler/computedFieldsExtern.lean.expected.out
View file

@ -1 +0,0 @@
150

1
tests/compiler/lazylist.lean
View file

@ -11,7 +11,6 @@ inductive LazyList (α : Type u) where
| cons (hd : α) (tl : LazyList α) : LazyList α
| delayed (t : Thunk $ LazyList α) : LazyList α
@[extern c inline "#2"]
def List.toLazy {α : Type u} : List α → LazyList α
| [] => LazyList.nil
| h::t => LazyList.cons h (toLazy t)

14
tests/compiler/test_single.sh
View file

@ -1,6 +1,18 @@
#!/usr/bin/env bash
source ../common.sh
compile_lean
# First check the C version actually works...
echo "running C program..."
rm "./$f.out" || true
compile_lean_c_backend
exec_check "./$f.out"
diff_produced
# Then check the LLVM version
if lean_has_llvm_support; then
echo "running LLVM program..."
rm "./$f.out" || true
compile_lean_llvm_backend
exec_check "./$f.out"
diff_produced
fi

2
tests/plugin/test_single.sh
View file

@ -1,7 +1,7 @@
#!/usr/bin/env bash
source ../common.sh
compile_lean -shared -o "${f%.lean}.so"
compile_lean_c_backend -shared -o "${f%.lean}.so"
expected_ret=1
exec_check lean -Dlinter.all=false --plugin="${f%.lean}.so" "$f"
diff_produced