diff --git a/nix/default-config-tests.nix b/nix/default-config-tests.nix
index d8b317c3a55625d36e777247e5093033734c05a4..5ba96c479ab83caf4cfae47b0318d0e517544c78 100644
--- a/nix/default-config-tests.nix
+++ b/nix/default-config-tests.nix
@@ -1,43 +1,9 @@
-{ lib
-, stdenv
-, frama-c
-, perl
-, time
-, which
-}:
+{ mk_tests } :
 
-stdenv.mkDerivation rec {
-  pname = "default-config-tests";
-  version = frama-c.version;
-  slang = frama-c.slang;
-
-  build_dir = frama-c.build_dir;
-  src = build_dir + "/dir.tar";
-  sourceRoot = ".";
-
-  buildInputs = frama-c.buildInputs ++ [
-    frama-c
-    perl
-    time
-    which
-  ];
-
-  postPatch = ''
-    patchShebangs .
-  '' ;
-
-  # Keep main configuration
-  configurePhase = ''
-    true
-  '';
-
-  buildPhase = ''
+mk_tests {
+  tests-name = "default-config-tests";
+  tests-command = ''
     dune exec -- frama-c-ptests tests src/plugins/*/tests
     dune build -j1 --display short @ptests_config
   '';
-
-  # No installation required
-  installPhase = ''
-    touch $out
-  '';
 }
diff --git a/nix/e-acsl-tests.nix b/nix/e-acsl-tests.nix
index 98edfa6fcaeb17653ec2da9774e5ff22a26307a0..7128d8d4a33a0b740c9fc78be436b4db41c10ae5 100644
--- a/nix/e-acsl-tests.nix
+++ b/nix/e-acsl-tests.nix
@@ -1,45 +1,9 @@
-{ lib
-, stdenvNoCC
-, frama-c
-, perl
-, pkgs
-, time
-, which
-}:
+{ mk_tests } :
 
-stdenvNoCC.mkDerivation rec {
-  pname = "e-acsl-tests";
-  version = frama-c.version;
-  slang = frama-c.slang;
-
-  build_dir = frama-c.build_dir;
-  src = build_dir + "/dir.tar";
-  sourceRoot = ".";
-
-  buildInputs = frama-c.buildInputs ++ [
-    frama-c
-    perl
-    pkgs.getopt
-    time
-    which
-  ];
-
-  postPatch = ''
-    patchShebangs .
-  '' ;
-
-  # Keep main configuration
-  configurePhase = ''
-    true
-  '';
-
-  buildPhase = ''
-    dune exec -- frama-c-ptests tests src/plugins/*/tests
+mk_tests {
+  tests-name = "e-acsl-tests";
+  tests-command = ''
+    dune exec -- frama-c-ptests tests src/plugins/e-acsl/tests
     dune build -j1 --display short @src/plugins/e-acsl/tests/ptests
   '';
-
-  # No installation required
-  installPhase = ''
-    touch $out
-  '';
 }
diff --git a/nix/eva-tests.nix b/nix/eva-tests.nix
index 1cd5aef54907ba9612eb3fa6ebd4cec922636e17..ba94821a3d2d6346ebc9df002fd1782848d8660b 100644
--- a/nix/eva-tests.nix
+++ b/nix/eva-tests.nix
@@ -1,37 +1,8 @@
-{ lib
-, stdenvNoCC # for E-ACSL
-, frama-c
-, perl
-, time
-, which
-}:
+{ mk_tests } :
 
-stdenvNoCC.mkDerivation rec {
-  pname = "eva-tests";
-  version = frama-c.version;
-  slang = frama-c.slang;
-
-  build_dir = frama-c.build_dir;
-  src = build_dir + "/dir.tar";
-  sourceRoot = ".";
-
-  buildInputs = frama-c.buildInputs ++ [
-    frama-c
-    perl
-    time
-    which
-  ];
-
-  postPatch = ''
-    patchShebangs .
-  '' ;
-
-  # Keep main configuration
-  configurePhase = ''
-    true
-  '';
-
-  buildPhase = ''
+mk_tests {
+  tests-name = "eva-tests";
+  tests-command = ''
     dune exec -- frama-c-ptests tests
     dune build -j1 --display short \
       @tests/builtins/ptests \
@@ -39,9 +10,4 @@ stdenvNoCC.mkDerivation rec {
       @tests/idct/ptests \
       @tests/value/ptests
   '';
-
-  # No installation required
-  installPhase = ''
-    touch $out
-  '';
 }
diff --git a/nix/full-tests.nix b/nix/full-tests.nix
index f69d97f89091cf2a3bc99b55ff4a4b7dc29241f6..511d04ce19ef5fc2bff7198e2e1e4f8b7d19397a 100644
--- a/nix/full-tests.nix
+++ b/nix/full-tests.nix
@@ -1,53 +1,12 @@
-{ lib
-, stdenvNoCC
-, frama-c
-, alt-ergo
-, perl
-, pkgs
-, time
-, which
-}:
+# Not meant to be used in CI: uses maximum parallelism
 
-stdenvNoCC.mkDerivation rec {
-  pname = "full-tests";
-  version = frama-c.version;
-  slang = frama-c.slang;
+{ mk_tests } :
 
-  build_dir = frama-c.build_dir;
-  src = build_dir + "/dir.tar";
-  wp_cache = fetchGit "git@git.frama-c.com:frama-c/wp-cache.git";
-  sourceRoot = ".";
-
-  buildInputs = frama-c.buildInputs ++ [
-    alt-ergo
-    frama-c
-    perl
-    pkgs.getopt
-    time
-    which
-  ];
-
-  postPatch = ''
-    patchShebangs .
-  '' ;
-
-  # Keep main configuration
-  # But configure Why3
-  configurePhase = ''
-    mkdir home
-    HOME=$(pwd)/home
-    why3 config detect
-  '';
-
-
-  buildPhase = ''
-    export FRAMAC_WP_CACHEDIR=$wp_cache
+mk_tests {
+  tests-name = "full-tests";
+  tests-command = ''
     dune exec -- frama-c-ptests tests src/plugins/*/tests
     dune build @ptests
   '';
-
-  # No installation required
-  installPhase = ''
-    touch $out
-  '';
+  has-wp-proofs = true ;
 }
diff --git a/nix/kernel-tests.nix b/nix/kernel-tests.nix
index 5d85217fb0e8fc6cbf768f6e7f53927868d67c9c..03b05e9c2ab553a727c28a2e1badb52b57b21e7d 100644
--- a/nix/kernel-tests.nix
+++ b/nix/kernel-tests.nix
@@ -1,37 +1,8 @@
-{ lib
-, stdenv
-, frama-c
-, perl
-, time
-, which
-}:
+{ mk_tests } :
 
-stdenv.mkDerivation rec {
-  pname = "kernel-tests";
-  version = frama-c.version;
-  slang = frama-c.slang;
-
-  build_dir = frama-c.build_dir;
-  src = build_dir + "/dir.tar";
-  sourceRoot = ".";
-
-  buildInputs = frama-c.buildInputs ++ [
-    frama-c
-    perl
-    time
-    which
-  ];
-
-  postPatch = ''
-    patchShebangs .
-  '' ;
-
-  # Keep main configuration
-  configurePhase = ''
-    true
-  '';
-
-  buildPhase = ''
+mk_tests {
+  tests-name = "kernel-tests";
+  tests-command = ''
     dune exec -- frama-c-ptests tests
     dune build -j1 --display short \
       @tests/cil/ptests \
@@ -45,9 +16,4 @@ stdenv.mkDerivation rec {
       @tests/syntax/ptests \
       @tests/test/ptests
   '';
-
-  # No installation required
-  installPhase = ''
-    touch $out
-  '';
 }
diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix
new file mode 100644
index 0000000000000000000000000000000000000000..413a24321b4c2a7fd55e5b9310e1dcd75d4d20a8
--- /dev/null
+++ b/nix/mk_tests.nix
@@ -0,0 +1,68 @@
+{ lib
+, alt-ergo
+, frama-c
+, perl
+, pkgs
+, stdenvNoCC
+, time
+, which
+} :
+
+{ tests-name
+, tests-command
+, has-wp-proofs ? false
+} :
+
+stdenvNoCC.mkDerivation {
+  pname = tests-name ;
+  version = frama-c.version;
+  slang = frama-c.slang;
+
+  src = frama-c.build_dir + "/dir.tar";
+  sourceRoot = ".";
+
+  buildInputs = frama-c.buildInputs ++ [
+    frama-c
+    perl
+    pkgs.getopt
+    time
+    which
+  ] ++
+  (if has-wp-proofs then [ alt-ergo ] else []);
+
+  postPatch = ''
+    patchShebangs .
+  '' ;
+
+  # Keep main configuration
+  configurePhase = ''
+    true
+  '';
+
+  wp_cache =
+    if has-wp-proofs
+    then fetchGit "git@git.frama-c.com:frama-c/wp-cache.git"
+    else "" ;
+
+  preBuild =
+    if has-wp-proofs
+    then ''
+        mkdir home
+        HOME=$(pwd)/home
+        why3 config detect
+        export FRAMAC_WP_CACHEDIR=$wp_cache
+      ''
+    else "" ;
+
+  buildPhase = ''
+    runHook preBuild
+  '' +
+  tests-command + ''
+    runHook postBuild
+  '';
+
+  # No installation required
+  installPhase = ''
+    touch $out
+  '';
+}
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index 192b7af7b85fe13e1cc6ba28640c51edec813c90..950ec9e361a5acbac33f4dca1d2e80596e64b5c3 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -9,6 +9,8 @@ let
     ocp-indent = oself.callPackage ./ocp-indent.nix {};
     psmt2-frontend = oself.callPackage ./psmt2-frontend.nix {};
     why3 = oself.callPackage ./why3.nix {};
+    # Helpers
+    mk_tests = oself.callPackage ./mk_tests.nix {};
     # Builds
     frama-c = oself.callPackage ./frama-c.nix {};
     lint = oself.callPackage ./lint.nix {};
diff --git a/nix/plugins-tests.nix b/nix/plugins-tests.nix
index aab6e9d288c6082f37da2ff585fa730136701d3d..6a051fe20ed3ba227b800ac941733c932e9c505e 100644
--- a/nix/plugins-tests.nix
+++ b/nix/plugins-tests.nix
@@ -1,44 +1,8 @@
-{ lib
-, stdenvNoCC
-, frama-c
-, alt-ergo
-, perl
-, time
-, which
-}:
+{ mk_tests } :
 
-stdenvNoCC.mkDerivation rec {
-  pname = "plugins-tests";
-  version = frama-c.version;
-  slang = frama-c.slang;
-
-  build_dir = frama-c.build_dir;
-  src = build_dir + "/dir.tar";
-  wp_cache = fetchGit "git@git.frama-c.com:frama-c/wp-cache.git"; # for Aorai
-  sourceRoot = ".";
-
-  buildInputs = frama-c.buildInputs ++ [
-    alt-ergo # only for Aorai
-    frama-c
-    perl
-    time
-    which
-  ];
-
-  postPatch = ''
-    patchShebangs .
-  '' ;
-
-  # Keep main configuration
-  # But for Aorai, configure Why3
-  configurePhase = ''
-    mkdir home
-    HOME=$(pwd)/home
-    why3 config detect
-  '';
-
-  buildPhase = ''
-    export FRAMAC_WP_CACHEDIR=$wp_cache # for Aorai
+mk_tests {
+  tests-name = "plugins-tests";
+  tests-command = ''
     dune exec -- frama-c-ptests tests src/plugins/*/tests
     dune build -j1 --display short \
       @tests/callgraph/ptests \
@@ -62,9 +26,5 @@ stdenvNoCC.mkDerivation rec {
       @src/plugins/server/tests/ptests \
       @src/plugins/variadic/tests/ptests
   '';
-
-  # No installation required
-  installPhase = ''
-    touch $out
-  '';
+  has-wp-proofs = true ;
 }
diff --git a/nix/wp-tests.nix b/nix/wp-tests.nix
index 4dbd1d862751729de1ed95aa8fa13ed69b52bae5..c431e8fe8072f253db36402f1c2888d5ff6b2186 100644
--- a/nix/wp-tests.nix
+++ b/nix/wp-tests.nix
@@ -1,48 +1,10 @@
-{ lib
-, stdenv
-, frama-c
-, alt-ergo
-, perl
-, time
-, which
-}:
+{ mk_tests } :
 
-stdenv.mkDerivation rec {
-  pname = "wp-tests";
-  version = frama-c.version;
-  slang = frama-c.slang;
-
-  build_dir = frama-c.build_dir;
-  src = build_dir + "/dir.tar";
-  wp_cache = fetchGit "git@git.frama-c.com:frama-c/wp-cache.git";
-  sourceRoot = ".";
-
-  buildInputs = frama-c.buildInputs ++ [
-    alt-ergo
-    frama-c
-    perl
-    time
-    which
-  ];
-
-  postPatch = ''
-    patchShebangs .
-  '' ;
-
-  configurePhase = ''
-    mkdir home
-    HOME=$(pwd)/home
-    why3 config detect
-  '';
-
-  buildPhase = ''
-    export FRAMAC_WP_CACHEDIR=$wp_cache
+mk_tests {
+  tests-name = "wp-tests";
+  tests-command = ''
     dune exec -- frama-c-ptests src/plugins/wp/tests
     dune build -j1 --display short @src/plugins/wp/tests/ptests
   '';
-
-  # No installation required
-  installPhase = ''
-    touch $out
-  '';
+  has-wp-proofs = true ;
 }