From d2a1e20dd0a5aa437c1688d2934bc01dc41bbd06 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 8 Sep 2021 18:56:19 +0200 Subject: [PATCH] feat: bundling LLVM on Linux --- .github/workflows/ci.yml | 14 +++++++++---- nix/bootstrap.nix | 4 ++-- script/prepare-llvm-linux.sh | 35 +++++++++++++++++++++++++++++++++ shell.nix | 4 ++++ src/CMakeLists.txt | 7 ++++--- src/Leanc.lean | 16 ++++++++------- src/bin/leanc.in | 9 ++++++--- src/shell/CMakeLists.txt | 38 +++++++++++++++++++----------------- 8 files changed, 90 insertions(+), 37 deletions(-) create mode 100755 script/prepare-llvm-linux.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cb8c5302ff..3d8deaab0c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -22,11 +22,12 @@ jobs: strategy: matrix: include: - # portable release build: link most libraries statically and use channel with older glibc (2.27; LLVM 7) + # portable release build: use channel with older glibc (2.27) - name: Linux release os: ubuntu-latest release: true shell: nix-shell --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}" + llvm-url: https://github.com/llvm/llvm-project/releases/download/llvmorg-13.0.0/clang+llvm-13.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz - name: Linux os: ubuntu-latest check-stage3: true @@ -100,18 +101,23 @@ jobs: run: | mkdir build cd build - OPTIONS= + OPTIONS=() + if [[ '${{ matrix.llvm-url }}' && "${{ matrix.name }}" == "Linux release" ]]; then + wget -q ${{ matrix.llvm-url }} + eval "OPTIONS+=($(../script/prepare-llvm-linux.sh clang*.tar.*))" + fi if [[ $GITHUB_EVENT_NAME == 'schedule' && -n '${{ matrix.release }}' && -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git git fetch nightly --tags LEAN_VERSION_STRING="nightly-$(date -u +%F)" # do nothing if commit already has a different tag if [[ $(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo $LEAN_VERSION_STRING) == $LEAN_VERSION_STRING ]]; then - OPTIONS=-DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING + OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING) echo "LEAN_VERSION_STRING=$LEAN_VERSION_STRING" >> $GITHUB_ENV fi fi - cmake .. ${{ matrix.CMAKE_OPTIONS }} $OPTIONS + # contortion to support empty OPTIONS with old macOS bash + cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} make -j4 # de-Nix-ify binaries - name: Patch diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 7fafcf4085..a951b97305 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -1,5 +1,5 @@ { debug ? false, stage0debug ? false, extraCMakeFlags ? [], - stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, + stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, ... } @ args: with builtins; rec { @@ -36,7 +36,7 @@ rec { mv bin/ include/ share/ $out/ mv leanc.sh $out/bin/leanc mv leanc/Leanc.lean $leanc_src/ - substituteInPlace $out/bin/leanc --replace '$root' "$out" + substituteInPlace $out/bin/leanc --replace '$root' "$out" --replace " sed " " ${gnused}/bin/sed " substituteInPlace $out/bin/leanmake --replace "make" "${gnumake}/bin/make" substituteInPlace $out/share/lean/lean.mk --replace "/usr/bin/env bash" "${bash}/bin/bash" ''; diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh new file mode 100755 index 0000000000..74f1ee7276 --- /dev/null +++ b/script/prepare-llvm-linux.sh @@ -0,0 +1,35 @@ +#!/usr/bin/env bash +set -uo pipefail + +# run from root build directory (from inside nix-shell or otherwise defining GLIBC/GCC_DEV/GCC_LIBS/GMP) as in +# ``` +# eval cmake ../.. $(../../script/prepare-llvm-linux.sh ~/Downloads/clang+llvm-13.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz) +# ``` + +# use full LLVM release for compiling C++ code, but subset for compiling C code and distribution + +[[ -d llvm ]] || (mkdir llvm; tar xf $1 --strip-components 1 --directory llvm) +mkdir -p stage1/{bin,lib,lib/glibc,include/clang} +CP="cp -d" # preserve symlinks +# a C compiler! +$CP $(realpath llvm/bin/clang) stage1/bin/clang +# a linker! +$CP llvm/bin/{lld,ld.lld} stage1/bin/ +# lean.h dependencies +$CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang +# ELF dependencies, must be put there for `--sysroot` +$CP $GLIBC/lib/crt* llvm/lib/ +$CP $GLIBC/lib/crt* stage1/lib/ +# further dependencies +# note that official LLVM releases are not built against compiler-rt, thus the GCC deps +$CP $GCC_ROOT/lib/gcc/*/*/libgcc.a $GCC_ROOT/lib/gcc/*/*/crt{begin,end}{,S}.o $GCC_LIBS/lib/libatomic.so* llvm/lib/libc++* $GMP/lib/libgmp.* stage1/lib/ +# 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/lib{c_nonshared,gcc_s}* 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 +OPTIONS=() +echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++ -DLEAN_USE_LIBCXX=ON" +# allow C++ code to include /usr since it needs quite a few more headers +echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm --stdlib=libc++ -I/usr/include -I/usr/include/x86_64-linux-gnu'" +echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -I ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang" +echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -fuse-ld=ROOT/bin/ld.lld'" +echo -n " -DLEAN_TEST_VARS='LD_LIBRARY_PATH=$PWD/stage1/lib:\${LD_LIBRARY_PATH:-}'" diff --git a/shell.nix b/shell.nix index 470d6a82ce..09d220f089 100644 --- a/shell.nix +++ b/shell.nix @@ -13,6 +13,10 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }: hardeningDisable = [ "all" ]; # more convenient `ctest` output CTEST_OUTPUT_ON_FAILURE = 1; + GMP = pkgs.gmp; + GLIBC = pkgs.glibc; + GCC_ROOT = pkgs.gcc.cc; + GCC_LIBS = pkgs.gcc.cc.lib; shellHook = '' export LEAN_SRC_PATH="$PWD/src" ''; diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0763b479da..3b65cb61e5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -20,6 +20,7 @@ endif() set(LEAN_EXTRA_LINKER_FLAGS "" CACHE STRING "Additional flags used by the linker") set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler") +set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests") if (NOT CMAKE_BUILD_TYPE) message(STATUS "No build type selected, default to Release") @@ -276,7 +277,7 @@ else() set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group") endif() -if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") +if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin" OR "${LEAN_USE_LIBCXX}") set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lc++") set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lc++") else() @@ -303,7 +304,7 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") endif() if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") - set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_LINKER_FLAGS} -ldl") + set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -ldl") endif() if(NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) @@ -387,7 +388,7 @@ include_directories(${CMAKE_BINARY_DIR}/include) # config.h etc., "public" head string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) # These are used in lean.mk (and libleanrt) and passed through by stdlib.make # They are not embedded into `leanc` since they are build profile/machine specific -set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") +set(LEANC_OPTS "${LEANC_OPTS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") if(CMAKE_OSX_SYSROOT) string(APPEND LEANC_OPTS " ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}") endif() diff --git a/src/Leanc.lean b/src/Leanc.lean index 16c2b84bcb..34469aba41 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -17,10 +17,14 @@ Beware of the licensing consequences since GMP is LGPL." let root ← match (← IO.getEnv "LEAN_SYSROOT") with | some root => System.FilePath.mk root | none => (← IO.appDir).parent.get! + let rootify s := s.replace "ROOT" root.toString + -- We assume that the CMake variables do not contain escaped spaces let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn + let cflagsHidden := "@LEANC_INTERNAL_FLAGS@".trim.splitOn let mut ldflags := ["-L", (root / "lib").toString, "-L", (root / "lib" / "lean").toString, (← IO.getEnv "LEANC_GMP").getD "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn + let ldflagsHidden := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn for arg in args do match arg with @@ -31,18 +35,16 @@ Beware of the licensing consequences since GMP is LGPL." ldflags := [] ldflagsExt := [] | "--print-cflags" => - IO.println <| " ".intercalate cflags + IO.println <| " ".intercalate (cflags.map rootify) return 0 | "--print-ldflags" => - IO.println <| " ".intercalate (cflags ++ ldflagsExt ++ ldflags) + IO.println <| " ".intercalate ((cflags ++ ldflagsExt ++ ldflags).map rootify) return 0 | _ => () - let mut cc := (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@" - if cc.startsWith "." then - cc := (root / "bin" / cc).toString - - let args := cflags ++ args ++ ldflagsExt ++ ldflags ++ ["-Wno-unused-command-line-argument"] + let cc := rootify <| (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@" + let args := cflags ++ cflagsHidden ++ args ++ ldflagsExt ++ ldflags ++ ldflagsHidden ++ ["-Wno-unused-command-line-argument"] + let args := args.map rootify if args.contains "-v" then IO.eprintln s!"{cc} {" ".intercalate args}" let child ← IO.Process.spawn { cmd := cc, args := args.toArray } diff --git a/src/bin/leanc.in b/src/bin/leanc.in index e6bb09797a..cc7a6158b3 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -1,10 +1,13 @@ #!/usr/bin/env bash # used only for building Lean itself root=$(dirname $0) -ldflags=("-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) +ldflags=("-L$root/lib" "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@ @LEANC_INTERNAL_LINKER_FLAGS@) for arg in "$@"; do # ccache doesn't like linker flags being passed here [[ "$arg" = "-c" ]] && ldflags=() - [[ "$arg" = "-v" ]] && set -x + [[ "$arg" = "-v" ]] && v=1 done -exec ${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument +cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument) +cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g") +[[ $v == 1 ]] && printf '%q ' $cmd +eval $cmd diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c904abe999..85f33616e8 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -46,6 +46,8 @@ add_test(lean_ghash2 "${CMAKE_BINARY_DIR}/bin/lean" --githash) add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean") +set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS}") + # LEAN TESTS file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") FOREACH(T ${LEANTESTS}) @@ -53,7 +55,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leantest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -64,7 +66,7 @@ FOREACH(T ${LEANRUNTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanruntest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -74,7 +76,7 @@ FOREACH(T ${LEANCOMPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leancomptest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T) add_test(NAME leancomptest_foreign @@ -82,7 +84,7 @@ add_test(NAME leancomptest_foreign COMMAND bash -c "${LEAN_BIN}/leanmake --always-make CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'") add_test(NAME leancomptest_doc_example WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler" - COMMAND bash -c "${LEAN_BIN}/leanmake --always-make bin && ./build/bin/test hello world") + COMMAND bash -c "export ${TEST_VARS}; leanmake --always-make bin && ./build/bin/test hello world") # LEAN INTERPRETER TESTS file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean") @@ -91,7 +93,7 @@ FOREACH(T ${LEANINTERPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leaninterptest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single_interpret.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single_interpret.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -103,7 +105,7 @@ FOREACH(T_OUT ${LEANBENCHTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanbenchtest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T_OUT) file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean") @@ -111,7 +113,7 @@ FOREACH(T ${LEANINTERPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanplugintest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T) # LEAN TESTS using --trust=0 @@ -120,7 +122,7 @@ FOREACH(T ${LEANT0TESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leant0test_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T) # LEAN SERVER TESTS @@ -130,7 +132,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanservertest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/server" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -141,7 +143,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leaninteractivetest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -149,7 +151,7 @@ add_test(NAME leanpkgtest WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/b" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} leanpkg build # linking requires some manual steps (cd ../a; leanpkg build lib) @@ -160,14 +162,14 @@ add_test(NAME leanpkgtest_cyclic WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/cyclic" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} leanpkg build 2>&1 | grep 'import cycle'") add_test(NAME leanpkgtest_user_ext WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_ext" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake | grep 'world, hello, test'") @@ -175,7 +177,7 @@ add_test(NAME leanpkgtest_user_attr WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake") @@ -183,7 +185,7 @@ add_test(NAME leanpkgtest_user_opt WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_opt" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake") @@ -191,7 +193,7 @@ add_test(NAME leanpkgtest_prv WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/prv" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake 2>&1 | grep 'error: field.*private'") @@ -199,7 +201,7 @@ add_test(NAME leanpkgtest_user_attr_app WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr_app" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake bin LINK_OPTS='${LEAN_DYN_EXE_LINKER_FLAGS}' && build/bin/UserAttr") @@ -215,5 +217,5 @@ add_test(NAME laketest WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/lake/examples" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} make LAKE=lake test")