feat: bundling LLVM on Linux

2021-09-08 18:56:19 +02:00 · 2021-09-08 18:56:19 +02:00 · d2a1e20dd0
commit d2a1e20dd0
parent 978e94272c
8 changed files with 90 additions and 37 deletions
--- 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
--- 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"
    '';
--- a/script/prepare-llvm-linux.sh
+++ 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:-}'"
--- 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"
    '';
--- 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()
--- 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 }
--- 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
--- 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")