Merge branch 'feature/dune/header-check' into 'feature/bobot/jbuilder'

Dune - Add check-headers to CI

See merge request frama-c/frama-c!3788

.gitlab-ci.yml

@@ -44,6 +44,15 @@ frama-c:
   tags:
     - nix
 
+header-check:
+  stage: build
+  script:
+    - ls -la
+    - nix-shell nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.frama-c-checkers-shell
+        --run 'FRAMAC_HDRCK="" make -f share/Makefile.headers check-headers'
+  tags:
+    - nix
+
 # ivette:
 #   stage: build
 #   image: node:lts-gallium

nix/frama-c-checkers-shell.nix

+{ lib
+, stdenv
+, frama-c-hdrck
+, git
+, gnumake
+, headache
+, ocp-indent
+} :
+stdenv.mkDerivation rec {
+  name = "frama-c-checkers-shell";
+  buildInputs = [
+    frama-c-hdrck
+    git
+    gnumake
+    headache
+    ocp-indent
+  ];
+}

nix/frama-c-hdrck.nix

+{ lib
+, stdenv
+, dune_3
+, gitignoreSource
+, ocaml
+} :
+
+stdenv.mkDerivation rec {
+  pname = "frama-c-hdrck";
+  version =
+    lib.strings.replaceStrings ["~"] ["-"]
+      (lib.strings.removeSuffix "\n"
+        (builtins.readFile ../VERSION));
+  slang = lib.strings.removeSuffix "\n" (builtins.readFile ../VERSION_CODENAME);
+
+  src = gitignoreSource ./../headers ;
+
+  buildInputs = [
+    dune_3
+    ocaml
+  ];
+
+  configurePhase = ''
+    true
+  '';
+
+  buildPhase = ''
+    dune build --root .
+  '';
+
+  installPhase = ''
+    dune install --prefix $out --root .
+  '';
+}

nix/pkgs.nix

@@ -10,12 +10,21 @@ let
     odoc = oself.callPackage ./odoc.nix {};
     psmt2-frontend = oself.callPackage ./psmt2-frontend.nix {};
     why3 = oself.callPackage ./why3.nix {};
+
     # Helpers
     mk_tests = oself.callPackage ./mk_tests.nix {};
     mk_plugin = oself.callPackage ./mk_plugin.nix {};
+
+    # Shell containing checkers (hdrck, ocp-indent)
+    frama-c-checkers-shell = oself.callPackage ./frama-c-checkers-shell.nix {
+      git = pkgs.git ;
+    };
+
     # Builds
     frama-c = oself.callPackage ./frama-c.nix {};
+    frama-c-hdrck = oself.callPackage ./frama-c-hdrck.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 {};
@@ -24,8 +33,10 @@ let
     kernel-tests = oself.callPackage ./kernel-tests.nix {};
     plugins-tests = oself.callPackage ./plugins-tests.nix {};
     wp-tests = oself.callPackage ./wp-tests.nix {};
+
     # Internal tests
     internal-tests = oself.callPackage ./internal-tests.nix {};
+
     # Release
     api-doc = oself.callPackage ./api-doc.nix {};
     manuals = oself.callPackage ./manuals.nix {};

share/Makefile.headers

@@ -67,7 +67,7 @@ HDRCK_EXTRA?=
 ## Command used to execute hdrck
 
 # Note: the public name of hdrck.exe is frama-c-hdrck
-ifeq ($(FRAMAC_HDRCK),"")
+ifeq ($(FRAMAC_HDRCK),)
 
 # HDRCK is external
 HDRCK:= frama-c-hdrck
@@ -101,7 +101,7 @@ $(error "Please set HEADER_SPEC variable to a file containing the header specifi
 
 endif # HEADER_HAS_GIT_FILE
 
-HDRCK_OPTS+= -z 
+HDRCK_OPTS+= -z
 
 else
 
@@ -185,4 +185,3 @@ headers.info:
 # Local Variables:
 # compile-command: "make"
 # End:
-