From 039e82c0a2f022e05614de95ea837035d02d1ad8 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 4 May 2022 11:07:01 +0200
Subject: [PATCH] [ci] Cleaner nix packages
---
nix/default-config-tests.nix | 42 +++-------------------
nix/e-acsl-tests.nix | 46 +++---------------------
nix/eva-tests.nix | 42 +++-------------------
nix/full-tests.nix | 53 ++++------------------------
nix/kernel-tests.nix | 42 +++-------------------
nix/mk_tests.nix | 68 ++++++++++++++++++++++++++++++++++++
nix/pkgs.nix | 2 ++
nix/plugins-tests.nix | 50 +++-----------------------
nix/wp-tests.nix | 48 +++----------------------
9 files changed, 103 insertions(+), 290 deletions(-)
create mode 100644 nix/mk_tests.nix
diff --git a/nix/default-config-tests.nix b/nix/default-config-tests.nix
index d8b317c3a55..5ba96c479ab 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 98edfa6fcae..7128d8d4a33 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 1cd5aef5490..ba94821a3d2 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 f69d97f8909..511d04ce19e 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 5d85217fb0e..03b05e9c2ab 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 00000000000..413a24321b4
--- /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 192b7af7b85..950ec9e361a 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 aab6e9d288c..6a051fe20ed 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 4dbd1d86275..c431e8fe807 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 ;
}
--
GitLab