diff --git a/nix/camlp5.nix b/nix/camlp5.nix
index 9f6055677e84c26d767479d9b72a452582a511f9..1c4a65efddf40548883fea00dbfba8b5e2b8e14c 100644
--- a/nix/camlp5.nix
+++ b/nix/camlp5.nix
@@ -10,13 +10,13 @@ else
 let params =
   if lib.versionAtLeast ocaml.version "4.12" && !legacy
   then rec {
-    version = "8.03.00";
+    version = "8.03.01";
 
     src = fetchFromGitHub {
       owner = "camlp5";
       repo = "camlp5";
       rev = version;
-      hash = "sha256-hu/279gBvUc7Z4jM6EHiar6Wm4vjkGXl+7bxowj+vlM=";
+      hash = "sha256-GnNSCfnizazMT5kgib7u5PIb2kWsnqpL33RsPEK4JvM=";
     };
 
     nativeBuildInputs = [ makeWrapper ocaml findlib perl ];
diff --git a/nix/dolmen.nix b/nix/dolmen.nix
new file mode 100644
index 0000000000000000000000000000000000000000..1586474f3910bd5879537ae562a7841c5779a1da
--- /dev/null
+++ b/nix/dolmen.nix
@@ -0,0 +1,31 @@
+{ lib, fetchurl, buildDunePackage
+, menhir, menhirLib
+, fmt
+, qcheck
+}:
+
+buildDunePackage rec {
+  pname = "dolmen";
+  version = "0.9";
+
+  minimalOCamlVersion = "4.08";
+
+  src = fetchurl {
+    url = "https://github.com/Gbury/dolmen/releases/download/v${version}/dolmen-${version}.tbz";
+    hash = "sha256-AD21OFS6zDoz+lXtac95gXwQNppPfGvpRK8dzDZXigo=";
+  };
+
+  nativeBuildInputs = [ menhir ];
+  propagatedBuildInputs = [ menhirLib fmt ];
+
+  doCheck = true;
+
+  checkInputs = [ qcheck ];
+
+  meta = {
+    description = "An OCaml library providing clean and flexible parsers for input languages";
+    license = lib.licenses.bsd2;
+    maintainers = [ lib.maintainers.vbgl ];
+    homepage = "https://github.com/Gbury/dolmen";
+  };
+}
diff --git a/nix/mlmpfr.nix b/nix/mlmpfr.nix
index ba0bd209fc19d893906ab433e839ecd60030b037..a7415486b973a09e88d4150ec33a5269a07b597c 100644
--- a/nix/mlmpfr.nix
+++ b/nix/mlmpfr.nix
@@ -4,11 +4,12 @@
 , gmp
 , mpfr
 , buildDunePackage
+, dune-configurator
 }:
 
 buildDunePackage rec {
   pname = "mlmpfr";
-  version = "4.1.0-bugfix2";
+  version = "4.2.1";
 
   minimumOCamlVersion = "4.04";
 
@@ -16,9 +17,11 @@ buildDunePackage rec {
     owner = "thvnx";
     repo = pname;
     rev = pname+"."+version;
-    sha256 = "19g26jv6cjinpl5pcjif1ldyaagxlandp3qjajsy8srqg4a5rg0d";
+    sha256 = "1pr1kl50r4s03z3biwhwvbg6pplwsgbdh2mg60r316hij1fdvkvg";
   };
 
+  patches = [ ./mlmpfr.patch ];
+  buildInputs = [ dune-configurator ];
   propagatedBuildInputs = [ gmp mpfr ];
 
   meta = {
diff --git a/nix/mlmpfr.patch b/nix/mlmpfr.patch
new file mode 100644
index 0000000000000000000000000000000000000000..0c1bb3b910e110038721d4accfda263a01ae160c
--- /dev/null
+++ b/nix/mlmpfr.patch
@@ -0,0 +1,26 @@
+From f810ca8cd5690d76367d6031796850828a7162b8 Mon Sep 17 00:00:00 2001
+From: Allan Blanchard <allan.blanchard@cea.fr>
+Date: Thu, 23 Jan 2025 13:37:11 +0100
+Subject: [PATCH] be sure that the warning on implicit declaration is never an
+ error
+
+---
+ src/dune | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/src/dune b/src/dune
+index 5158d05..ab698c1 100644
+--- a/src/dune
++++ b/src/dune
+@@ -7,7 +7,7 @@
+   (language c)
+   (names mlmpfr_stubs)
+   (flags
+-   (:include c_flags.sexp)))
++   (:include c_flags.sexp) -Wno-error=implicit-function-declaration))
+  (c_library_flags
+   (:include c_library_flags.sexp)))
+ 
+-- 
+2.34.1
+
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index b54ca50e900d38be8acea69f26f782e920394db0..1374a37bd96f197dc91c9f3d909c68d72384c26d 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -5,7 +5,10 @@ let
     alt-ergo = oself.callPackage ./alt-ergo.nix {};
     camlp5 = oself.callPackage ./camlp5.nix {};
     combinetura = oself.callPackage ./combinetura.nix {};
+    dolmen = oself.callPackage ./dolmen.nix {};
     mlmpfr = oself.callPackage ./mlmpfr.nix {};
+    ppxlib = oself.callPackage ./ppxlib.nix {};
+    ppxlib_jane = oself.callPackage ./ppxlib_jane.nix {};
     why3 = oself.callPackage ./why3.nix {};
 
     # Helpers
diff --git a/nix/ppxlib.nix b/nix/ppxlib.nix
new file mode 100644
index 0000000000000000000000000000000000000000..1ef83fce8041a51346d1daf70696427eaf434834
--- /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.34.0";
+
+  duneVersion = "3";
+
+  src = fetchurl {
+    url = "https://github.com/ocaml-ppx/ppxlib/releases/download/${version}/ppxlib-${version}.tbz";
+    sha256 = "sha256-132XFloVjXrla3wDh80E6ZJ9fn55fKEDn/tbsXpmYac=";
+  };
+
+  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/ppxlib_jane.nix b/nix/ppxlib_jane.nix
new file mode 100644
index 0000000000000000000000000000000000000000..2d9a2cad76e5968a444427f6098b6fb32a43b3d6
--- /dev/null
+++ b/nix/ppxlib_jane.nix
@@ -0,0 +1,20 @@
+{ lib, ocaml, janePackage, ppxlib }:
+janePackage (
+  {
+    pname = "ppxlib_jane";
+    meta.description = "A library for use in ppxes for constructing and matching on ASTs corresponding to the augmented parsetree";
+    propagatedBuildInputs = [ ppxlib ];
+  }
+  // (
+  if lib.versionAtLeast ocaml.version "5.3" then
+    {
+      version = "0.17.2";
+      hash = "sha256-AQJSdKtF6p/aG5Lx8VHVEOsisH8ep+iiml6DtW+Hdik=";
+    }
+  else
+    {
+      version = "0.17.0";
+      hash = "sha256-8NC8CHh3pSdFuRDQCuuhc2xxU+84UAsGFJbbJoKwd0U=";
+    }
+  )
+)