diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7ca819cef21a4006f0c2bb31c939aac505353bc1..0da7cb8d103c08e31b433e145826ddff1a428b7c 100644
--- a/.gitlab-ci.yml
+++ b/.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
diff --git a/nix/alt-ergo.nix b/nix/alt-ergo.nix
index 75288b5ff80bfb9a250f48bf2fd1964af1188222..0bdce24403b1564fbe1e4ca9972665643a4cba9d 100644
--- a/nix/alt-ergo.nix
+++ b/nix/alt-ergo.nix
@@ -1,4 +1,18 @@
-{ 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";
diff --git a/nix/frama-c-checkers-shell.nix b/nix/frama-c-checkers-shell.nix
index 1456c7a6e92c47759ec74d112db5ef7ec9bee7aa..356f25ed92e76e4dbf3920f7376a23a7958e6531 100644
--- a/nix/frama-c-checkers-shell.nix
+++ b/nix/frama-c-checkers-shell.nix
@@ -1,7 +1,7 @@
 { 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
diff --git a/nix/headache.nix b/nix/headache.nix
deleted file mode 100644
index 258016810ddcf07992f3c430e46afd05c8b05135..0000000000000000000000000000000000000000
--- a/nix/headache.nix
+++ /dev/null
@@ -1,32 +0,0 @@
-{ 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 = [ ];
-  };
-}
diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix
index bef1ffdc48e296581309ef715d9f971583fdf197..48e04ae1ac9118583330ef6b08b856f875d7ac2c 100644
--- a/nix/internal-tests.nix
+++ b/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
   '';
diff --git a/nix/mk_plugin.nix b/nix/mk_plugin.nix
index 4cb2f5f666e6cf5b48e160315a1a765849643c01..dbf03c6ba483b3692831c64dec7588863aea1803 100644
--- a/nix/mk_plugin.nix
+++ b/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
   '';
 
diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix
index 4d35f6a6a678191b21d4f63da3969eb28169a327..9d71cbf776d6cb7f4c005b4d14be62c03abce397 100644
--- a/nix/mk_tests.nix
+++ b/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
diff --git a/nix/ocaml-versions.txt b/nix/ocaml-versions.txt
index 9f34af85f44d5d266c12eb6ae0431f6be61a58db..641cb6bc2e393abad444454a7f66179bbc21ebbd 100644
--- a/nix/ocaml-versions.txt
+++ b/nix/ocaml-versions.txt
@@ -1,2 +1,3 @@
 4.13.1
 4.14.1
+5.1.1
diff --git a/nix/ocplib-simplex.nix b/nix/ocplib-simplex.nix
index 474f69546d1a10929c579a3bf0366fed1f392414..0e1226479dc2ddc1711afe6ab00695898c4608ba 100644
--- a/nix/ocplib-simplex.nix
+++ b/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 ];
diff --git a/nix/odoc-parser.nix b/nix/odoc-parser.nix
new file mode 100644
index 0000000000000000000000000000000000000000..805d7ce87c36fa388e41dde9bdf45c57d3a55978
--- /dev/null
+++ b/nix/odoc-parser.nix
@@ -0,0 +1,23 @@
+{ 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";
+  };
+}
diff --git a/nix/odoc.nix b/nix/odoc.nix
new file mode 100644
index 0000000000000000000000000000000000000000..88cb8669a4b0a073e4e1416cfc091cbf5bfc99c7
--- /dev/null
+++ b/nix/odoc.nix
@@ -0,0 +1,27 @@
+{ 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";
+  };
+}
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index 5e313453a1d3197210c2ab33b4c32445228ca169..2f44490542624d697cdbba9787863e8e8b550e53 100644
--- a/nix/pkgs.nix
+++ b/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;
diff --git a/nix/plugin-checkers-shell.nix b/nix/plugin-checkers-shell.nix
index d64816338da7d7eac446892378de4787df1d1d90..cc1d340f645b600ff7866b883cbbf6927d686804 100644
--- a/nix/plugin-checkers-shell.nix
+++ b/nix/plugin-checkers-shell.nix
@@ -1,6 +1,6 @@
 { 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
diff --git a/nix/ppxlib.nix b/nix/ppxlib.nix
new file mode 100644
index 0000000000000000000000000000000000000000..03b1aaee58165d13e3345b84e772466a36ca0094
--- /dev/null
+++ b/nix/ppxlib.nix
@@ -0,0 +1,29 @@
+{ 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";
+  };
+}
diff --git a/nix/sources.json b/nix/sources.json
index cb4337bbbcbea7ea7b46ef3304ea1af627b0eb28..3619413b613e0e82ab0567486afc34865891c6d4 100644
--- a/nix/sources.json
+++ b/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": {
diff --git a/nix/src-distrib.nix b/nix/src-distrib.nix
deleted file mode 100644
index 053764b047c9969dca16a2dd0b715c3bd300399b..0000000000000000000000000000000000000000
--- a/nix/src-distrib.nix
+++ /dev/null
@@ -1,35 +0,0 @@
-{ 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
-  '';
-}
diff --git a/nix/wp-cache.nix.sh b/nix/wp-cache.nix.sh
index d633e7332bdf09a1cacce6dea479c35e6ce5b846..0130917c1d86739e019ffd66683a9ecbcdb5d634 100755
--- a/nix/wp-cache.nix.sh
+++ b/nix/wp-cache.nix.sh
@@ -32,5 +32,6 @@ stdenv.mkDerivation rec {
            rev = "$commit" ;
            shallow = true ;
          };
+  installPhase = "touch \$out";
 }
 EOL