From dabd36da96e9591715bfc5838aa4a926f19afe17 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 22 Apr 2022 16:04:42 +0200
Subject: [PATCH] [ci] 4.13 CI

---
 .gitlab-ci.yml               | 30 +++++++++++++++++--------
 build-distrib.sh             | 20 +++++++++++++++++
 nix/default-config-tests.nix | 43 ++++++++++++++++++++++++++++++++++++
 nix/pkgs.nix                 |  1 +
 4 files changed, 85 insertions(+), 9 deletions(-)
 create mode 100755 build-distrib.sh
 create mode 100644 nix/default-config-tests.nix

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f7637e3d1d8..a28262407bb 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -9,9 +9,9 @@ stages:
 
 variables:
      DEFAULT: "feature/bobot/jbuilder"
+     OCAML: "4_12"
 #     CURRENT: $CI_COMMIT_REF_NAME
 #     FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
-#     OCAML: "4_08"
 
 ################################################################################
 ### BUILD
@@ -27,7 +27,7 @@ check-no-old-frama-c:
 frama-c:
   stage: build
   script:
-    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.frama-c
+    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.frama-c
   artifacts:
     when: on_failure
     paths:
@@ -40,7 +40,7 @@ frama-c:
 lint:
   stage: build
   script:
-   - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.lint
+   - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.lint
   coverage: '/lint coverage: \d+\.\d+/'
   tags:
    - nix
@@ -79,21 +79,21 @@ genassigns:
 e-acsl-tests:
   stage: tests
   script:
-    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.e-acsl-tests
+    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.e-acsl-tests
   tags:
     - nix
 
 eva-tests:
   stage: tests
   script:
-    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.eva-tests
+    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.eva-tests
   tags:
     - nix
 
 kernel-tests:
   stage: tests
   script:
-    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.kernel-tests
+    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.kernel-tests
   tags:
     - nix
 
@@ -114,7 +114,7 @@ mthread:
 plugins-tests:
   stage: tests
   script:
-    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.plugins-tests
+    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.plugins-tests
   tags:
     - nix
 
@@ -135,7 +135,7 @@ volatile:
 wp-tests:
   stage: tests
   script:
-    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.wp-tests
+    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.wp-tests
   tags:
     - nix
 
@@ -146,7 +146,7 @@ wp-tests:
 manuals: # TODO: restore doc companions
   stage: distrib_and_compatibility
   script:
-    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.manuals
+    - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.manuals
   tags:
     - nix
   when: manual
@@ -166,6 +166,18 @@ manuals: # TODO: restore doc companions
       - result/user-manual.pdf
       - result/wp-manual.pdf
 
+.build_template: &frama-c-ocaml
+  stage: distrib_and_compatibility
+  script:
+   - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.default-config-tests
+  tags:
+   - nix
+
+frama-c-ocaml-4.13:
+  variables:
+    OCAML: "4_13"
+  <<: *frama-c-ocaml
+
 ################################################################################
 ### PUBLIC
 
diff --git a/build-distrib.sh b/build-distrib.sh
new file mode 100755
index 00000000000..750b7a006c3
--- /dev/null
+++ b/build-distrib.sh
@@ -0,0 +1,20 @@
+#! /usr/bin/bash
+
+if   [[ $# > 1 ]] ; then
+  echo "usage: $0 [ configuration_file ]"
+  exit 1
+elif [[ $# = 1 ]] ; then
+  source $1
+fi
+
+VERSION=${VERSION:-$(cat VERSION)}
+CODENAME=${CODENAME:-$(cat VERSION_CODENAME)}
+
+FRAMAC=frama-c-$VERSION-$CODENAME
+
+FPATH=$FRAMAC/
+
+git archive --format=tar --prefix $FPATH HEAD > $FRAMAC.tar
+
+TRANSFO="s,^,$FPATH,"
+tar rf $FRAMAC.tar configure --transform $TRANSFO
diff --git a/nix/default-config-tests.nix b/nix/default-config-tests.nix
new file mode 100644
index 00000000000..d8b317c3a55
--- /dev/null
+++ b/nix/default-config-tests.nix
@@ -0,0 +1,43 @@
+{ lib
+, stdenv
+, frama-c
+, perl
+, time
+, which
+}:
+
+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 = ''
+    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/pkgs.nix b/nix/pkgs.nix
index 1b45e6fe5ee..66c0e63724c 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -12,6 +12,7 @@ let
     frama-c = oself.callPackage ./frama-c.nix {};
     lint = oself.callPackage ./lint.nix {};
     # Tests
+    default-config-tests = oself.callPackage ./default-config-tests.nix {};
     e-acsl-tests = oself.callPackage ./e-acsl-tests.nix {};
     eva-tests = oself.callPackage ./eva-tests.nix {};
     kernel-tests = oself.callPackage ./kernel-tests.nix {};
-- 
GitLab