From df99a6a469584532daa57d986e795dd559bee57c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 31 Oct 2020 23:47:44 +0100
Subject: [PATCH] fix: Nix: tests (almost, apart from leanmake & server tests)

---
 flake.nix |  2 ++
 new.nix   | 25 ++++++++++++-------------
 2 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/flake.nix b/flake.nix
index 0545ff1fd9..075de5d161 100644
--- a/flake.nix
+++ b/flake.nix
@@ -27,5 +27,7 @@ export CCACHE_BASE_DIR=$NIX_BUILD_TOP
 
     defaultPackage.x86_64-linux = self.packages.x86_64-linux.lean;
 
+    checks.x86_64-linux.lean = self.packages.x86_64-linux.lean.test;
+
   };
 }
diff --git a/new.nix b/new.nix
index dbc42ee49b..c044362bb4 100644
--- a/new.nix
+++ b/new.nix
@@ -141,26 +141,25 @@ ar rcs $out/lib${name}.a ${lib.concatStringsSep " " (map (drv: "${drv}/out.o") (
         name = "lean-${desc}";
         buildCommand = ''
           mkdir -p $out/bin $out/lib/lean
-          ln -s ${leancpp}/lib/lean/* ${Init.staticLib}/* ${Std.staticLib}/* ${Lean.staticLib}/* ${Lean.modRoot}/* $out/lib/lean
-          ${leancpp}/bin/leanc -x none -L${gmp}/lib -L$out/lib/lean ${leancpp}/lib/lean/* -o $out/bin/lean
+          ln -sf ${leancpp}/lib/lean/* ${Init.staticLib}/* ${Init.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* $out/lib/lean
+          ${leancpp}/bin/leanc -x none -rdynamic -L${gmp}/lib -L$out/lib/lean ${leancpp}/lib/lean/* -o $out/bin/lean
           ln -s ${leancpp}/bin/{leanc,lean-gdb.py} $out/bin/
+          ln -s ${leancpp}/include $out/include
         '';
       };
-      test = stdenv.mkDerivation {
+      test = buildCMake {
         name = "lean-test-${desc}";
-
-        inherit src;
-        nativeBuildInputs = leanBin.nativeBuildInputs ++ leanBin.buildInputs ++ [ bash ];
-
+        realSrc = lib.sourceByRegex ./. [ "src.*" "tests.*" ];
+        preConfigure = ''
+          cd src
+        '';
         postConfigure = ''
-          patchShebangs tests
-          #ln -s ${install}/bin ../../bin
-          #ln -s ${install}/bin/lean shell/lean
-          #rm -r ../../library
-          #ln -s ${install}/lib/lean/library ../../library
+          patchShebangs ../../tests
+          rm -r bin lib include
+          ln -sf ${lean}/* .
         '';
         buildPhase = ''
-          ctest --output-on-failure -E style_check -j$NIX_BUILD_CORES
+          ctest --output-on-failure -E leancomptest_foreign -j$NIX_BUILD_CORES
         '';
       };
     };