[ci] Cleaner nix packages

nix/default-config-tests.nix

-{ 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
-  '';
 }

nix/e-acsl-tests.nix

-{ 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
-  '';
 }

nix/eva-tests.nix

-{ 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
-  '';
 }

nix/full-tests.nix

-{ 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 ;
 }

nix/kernel-tests.nix

-{ 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
-  '';
 }

nix/mk_tests.nix

+{ 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
+  '';
+}

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 {};

nix/plugins-tests.nix

-{ 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 ;
 }

nix/wp-tests.nix

-{ 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 ;
 }