Merge branch 'feature/blanchard/ci/update' into 'master'

[nix] update commit

Closes #1316

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

.gitlab-ci.yml

@@ -433,6 +433,7 @@ internal-nightly:
 .build_template: &additional_arch_template
   stage: compatibility
   script:
+    - opam update
     - opam switch create --empty .
     - eval $(opam env --switch=. --set-switch)
     # Note: we use this to get an exact version corresponding to a minor version
@@ -471,14 +472,14 @@ additional-arch-release:
 .build_template: &ocaml_always_additional_versions_template
   parallel:
     matrix:
-      - OCAML: ["4.14"]
+      - OCAML: ["5.1"]
 
 # Uncomment this block when there are intermediate versions to check manully
-#.build_template: &ocaml_manual_additional_versions_template
-#  parallel:
-#    matrix:
-#      - OCAML: ["4.14"]
-#  when: manual
+.build_template: &ocaml_manual_additional_versions_template
+  parallel:
+    matrix:
+      - OCAML: ["4.14"]
+  when: manual
 
 .build_template: &ocaml_versions_template
   stage: compatibility
@@ -493,14 +494,14 @@ ocaml-versions:
     - schedules
 
 # Uncomment this section when there are additional versions of OCaml to test
-# ocaml-versions-more:
-#   <<: *ocaml_versions_template
-#   <<: *ocaml_manual_additional_versions_template
+ocaml-versions-more:
+  <<: *ocaml_versions_template
+  <<: *ocaml_manual_additional_versions_template
 
 ocaml-versions-nightly:
   <<: *ocaml_versions_template
   <<: *ocaml_always_additional_versions_template
-  # we still check them for the publisher pipeline job
+  # in publish schedule, we still check additional versions of OCaml
   <<: *when_publish
 
 # Opam pin

nix/alt-ergo.nix

-{ fetchFromGitHub, fetchpatch, lib, which, ocamlPackages }:
+{ lib
+, buildDunePackage
+, fetchFromGitHub
+, camlzip
+, cmdliner
+, dune-configurator
+, menhir
+, num
+, ocplib-simplex
+, psmt2-frontend
+, seq
+, stdlib-shims
+, which
+, zarith
+}:
 
 let
   pname = "alt-ergo";
@@ -14,34 +28,34 @@ let
   };
 in
 
-let alt-ergo-lib = ocamlPackages.buildDunePackage rec {
+let alt-ergo-lib = buildDunePackage rec {
   pname = "alt-ergo-lib";
   inherit version src configureScript;
   configureFlags = [ pname ];
   nativeBuildInputs = [ which ];
-  buildInputs = with ocamlPackages; [ dune-configurator ];
-  propagatedBuildInputs = with ocamlPackages; [ num ocplib-simplex seq stdlib-shims zarith ];
+  buildInputs = [ dune-configurator ];
+  propagatedBuildInputs = [ num ocplib-simplex seq stdlib-shims zarith ];
   preBuild = ''
     substituteInPlace src/lib/util/version.ml --replace 'version="dev"' 'version="${version}"'
   '';
 }; in
 
-let alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
+let alt-ergo-parsers = buildDunePackage rec {
   pname = "alt-ergo-parsers";
   inherit version src configureScript;
   configureFlags = [ pname ];
-  nativeBuildInputs = [ which ocamlPackages.menhir ];
-  propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]);
+  nativeBuildInputs = [ which menhir ];
+  propagatedBuildInputs = [ alt-ergo-lib camlzip psmt2-frontend ];
 }; in
 
-ocamlPackages.buildDunePackage {
+buildDunePackage {
 
   inherit pname version src configureScript;
 
   configureFlags = [ pname ];
 
-  nativeBuildInputs = [ which ocamlPackages.menhir ];
-  buildInputs = [ alt-ergo-parsers ocamlPackages.cmdliner ];
+  nativeBuildInputs = [ which menhir ];
+  buildInputs = [ alt-ergo-parsers cmdliner ];
 
   meta = {
     description = "High-performance theorem prover and SMT solver";

nix/frama-c-checkers-shell.nix

 { lib
 , stdenv
 , black
-, clang_10
+, clang_11
 , combinetura
 , frama-c-hdrck
 , frama-c-lint
@@ -16,7 +16,7 @@ stdenv.mkDerivation rec {
   name = "frama-c-checkers-shell";
   buildInputs = [
     black
-    clang_10
+    clang_11
     combinetura
     frama-c-hdrck
     frama-c-lint

nix/headache.nix

-{ lib
-, camomile
-, fetchFromGitHub
-, buildDunePackage
-, cmdliner
-}:
-
-buildDunePackage rec {
-  version = "v1.05";
-  pname = "headache";
-
-  src = fetchFromGitHub {
-    owner = "Frama-C";
-    repo = pname;
-    rev = version;
-    sha256 = "036lrcxh23j2rrj91wlgq9piyyv1vh82wjy63z1l1ggkkhfs7d8r";
-  };
-
-  useDune2 = true;
-
-  buildInputs = [
-    cmdliner
-    camomile
-  ];
-
-  meta = with lib; {
-    homepage = https://github.com/Frama-C/headache/;
-    description = "Automatic generation of files headers";
-    license = licenses.gpl2;
-    maintainers = [ ];
-  };
-}

nix/internal-tests.nix

@@ -145,8 +145,12 @@ stdenvNoCC.mkDerivation rec {
     export FRAMAC_WP_CACHEDIR=$wp_cache
   '';
 
+  # The export NIX_GCC_DONT_MANGLE_PREFIX_MAP is meant to disable the
+  # transformation of the path of Frama-C into uppercase when using the
+  # __FILE__ macro.
   checkPhase = ''
     runHook preCheck
+    export NIX_GCC_DONT_MANGLE_PREFIX_MAP=
     dune exec -- frama-c-ptests -never-disabled tests src/plugins/*/tests
     dune build -j1 --display short @ptests_config
   '';

nix/mk_plugin.nix

@@ -106,9 +106,13 @@ stdenv.mkDerivation {
     ''
   else "") ;
 
+  # The export NIX_GCC_DONT_MANGLE_PREFIX_MAP is meant to disable the
+  # transformation of the path of Frama-C into uppercase when using the
+  # __FILE__ macro.
   checkPhase = ''
     runHook preCheck
     make run-ptests
+    export NIX_GCC_DONT_MANGLE_PREFIX_MAP=
     dune build -j1 --display short @tests/ptests
   '';
 

nix/mk_tests.nix

@@ -103,8 +103,12 @@ stdenvNoCC.mkDerivation {
     ''
     else "" ;
 
+  # The export NIX_GCC_DONT_MANGLE_PREFIX_MAP is meant to disable the
+  # transformation of the path of Frama-C into uppercase when using the
+  # __FILE__ macro.
   buildPhase = ''
     runHook preBuild
+    export NIX_GCC_DONT_MANGLE_PREFIX_MAP=
   '' +
   tests-command + ''
     runHook postBuild

nix/ocaml-versions.txt

 4.13.1
 4.14.1
+5.1.1

nix/ocplib-simplex.nix

@@ -2,7 +2,7 @@
 
 let
   pname = "ocplib-simplex";
-  version = "0.4";
+  version = "0.4.1";
 in
 
 stdenv.mkDerivation {
@@ -12,7 +12,7 @@ stdenv.mkDerivation {
     owner = "OCamlPro-Iguernlala";
     repo = pname;
     rev = "v${version}";
-    sha256 = "09niyidrjzrj8g1qwx4wgsdf5m6cwrnzg7zsgala36jliic4di60";
+    sha256 = "sha256-bhlTBpJg031x2lUjwuVrhQgOGmDLW/+0naN8wRjv6i4=";
   };
 
   nativeBuildInputs = [ autoreconfHook ocaml findlib ];

nix/odoc-parser.nix

+{ lib, fetchurl, buildDunePackage, ocaml, astring, result, camlp-streams }:
+
+buildDunePackage rec {
+  pname = "odoc-parser";
+  version = "2.4.1";
+
+  minimalOCamlVersion = "4.02";
+
+  src = fetchurl {
+    url = "https://github.com/ocaml/odoc/releases/download/${version}/odoc-${version}.tbz";
+    sha256 = "sha256-uBSguQILUD62fxfR2alp0FK2PYzcfN+l+3k7E3VYzts=";
+  };
+
+  propagatedBuildInputs = [ astring result camlp-streams ];
+
+  meta = {
+    description = "Parser for Ocaml documentation comments";
+    license = lib.licenses.isc;
+    maintainers = [ lib.maintainers.marsam ];
+    homepage = "https://github.com/ocaml-doc/odoc-parser";
+    changelog = "https://github.com/ocaml-doc/odoc-parser/raw/${version}/CHANGES.md";
+  };
+}

nix/odoc.nix

+{ lib, fetchurl, buildDunePackage, ocaml
+, astring, cmdliner, cppo, fpath, result, tyxml
+, odoc-parser, fmt, crunch
+}:
+
+buildDunePackage rec {
+  pname = "odoc";
+  version = "2.4.1";
+
+  src = fetchurl {
+    url = "https://github.com/ocaml/odoc/releases/download/${version}/odoc-${version}.tbz";
+    sha256 = "sha256-uBSguQILUD62fxfR2alp0FK2PYzcfN+l+3k7E3VYzts=";
+  };
+
+  nativeBuildInputs = [ cppo crunch ];
+  buildInputs = [ astring cmdliner fpath result tyxml odoc-parser fmt ];
+
+  doCheck = false;
+
+  meta = {
+    description = "A documentation generator for OCaml";
+    license = lib.licenses.isc;
+    maintainers = [ lib.maintainers.vbgl ];
+    homepage = "https://github.com/ocaml/odoc";
+    changelog = "https://github.com/ocaml/odoc/blob/${version}/CHANGES.md";
+  };
+}

nix/pkgs.nix

@@ -4,9 +4,11 @@ let
     # External Packages
     alt-ergo = oself.callPackage ./alt-ergo.nix {};
     combinetura = oself.callPackage ./combinetura.nix {};
-    headache = oself.callPackage ./headache.nix {};
     mlmpfr = oself.callPackage ./mlmpfr.nix {};
     ocplib-simplex = oself.callPackage ./ocplib-simplex.nix {};
+    odoc = oself.callPackage ./odoc.nix {};
+    odoc-parser = oself.callPackage ./odoc-parser.nix {};
+    ppxlib = oself.callPackage ./ppxlib.nix {};
     why3 = oself.callPackage ./why3.nix {};
 
     # Helpers
@@ -68,8 +70,8 @@ let
     niv = (import sources.niv {}).niv;
     ocaml-ng = super.lib.mapAttrs (
       name: value:
-        if builtins.hasAttr "overrideScope'" value
-        then value.overrideScope' ocamlOverlay
+        if builtins.hasAttr "overrideScope" value
+        then value.overrideScope ocamlOverlay
         else value
     ) super.ocaml-ng;
     inherit (super.callPackage sources."gitignore.nix" {}) gitignoreSource;

nix/plugin-checkers-shell.nix

 { lib
 , stdenv
-, clang_10
+, clang_11
 , frama-c
 , frama-c-hdrck
 , frama-c-lint
@@ -12,7 +12,7 @@
 stdenv.mkDerivation rec {
   name = "plugin-checkers-shell";
   buildInputs = [
-    clang_10
+    clang_11
     frama-c
     frama-c-hdrck
     frama-c-lint

nix/ppxlib.nix

+{ lib, fetchurl, buildDunePackage, ocaml,
+  stdlib-shims, ocaml-compiler-libs, ppx_derivers, stdio
+}:
+
+buildDunePackage rec {
+  pname = "ppxlib";
+  version = "0.32.0";
+
+  duneVersion = "3";
+
+  src = fetchurl {
+    url = "https://github.com/ocaml-ppx/ppxlib/releases/download/${version}/ppxlib-${version}.tbz";
+    sha256 = "sha256-UHzHPM+JXyLutSV6IkODjBijigkQX8/1Xu75FIVVQis=";
+  };
+
+  propagatedBuildInputs = [
+    ocaml-compiler-libs
+    ppx_derivers
+    stdio
+    stdlib-shims
+  ];
+
+  meta = {
+    description = "Comprehensive ppx tool set";
+    license = lib.licenses.mit;
+    maintainers = [ lib.maintainers.vbgl ];
+    homepage = "https://github.com/ocaml-ppx/ppxlib";
+  };
+}

nix/sources.json

@@ -29,10 +29,10 @@
         "homepage": "https://github.com/NixOS/nixpkgs",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "fdd898f8f79e8d2f99ed2ab6b3751811ef683242",
-        "sha256": "05i97acjry4pk1br8glwl97gbfjafq058kblpfpd39r0qr8j6x4s",
+        "rev": "3030f185ba6a4bf4f18b87f345f104e6a6961f34",
+        "sha256": "0v5q4zadnmdiv8hwcsx804l8radx562aqdw0r5nld127c8f7jzz8",
         "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fdd898f8f79e8d2f99ed2ab6b3751811ef683242.tar.gz",
+        "url": "https://github.com/NixOS/nixpkgs/archive/3030f185ba6a4bf4f18b87f345f104e6a6961f34.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
     },
     "why3": {

nix/src-distrib.nix

-{ lib
-, stdenv
-, frama-c
-# , headache
-, git
-} :
-
-stdenv.mkDerivation rec {
-  pname = "src-distrib";
-  version = frama-c.version;
-  slang = frama-c.slang;
-
-  src = ./.. ;
-
-  nativeBuildInputs = frama-c.nativeBuildInputs;
-
-  buildInputs = frama-c.buildInputs ++ [
-    # headache
-    git
-  ];
-
-  preBuild = ''
-    patchShebangs ./devel_tools/make-distrib.sh
-  '';
-
-  buildPhase = ''
-    runHook preBuild
-    ./devel_tools/make-distrib.sh
-  '';
-
-  installPhase = ''
-    mkdir -p $out
-    cp frama-c.tar.gz $out
-  '';
-}

nix/wp-cache.nix.sh

@@ -32,5 +32,6 @@ stdenv.mkDerivation rec {
            rev = "$commit" ;
            shallow = true ;
          };
+  installPhase = "touch \$out";
 }
 EOL