diff --git a/pkgs/applications/science/logic/alt-ergo/default.nix b/pkgs/applications/science/logic/alt-ergo/default.nix
index 73dcd6596008..2f58141c3281 100644
--- a/pkgs/applications/science/logic/alt-ergo/default.nix
+++ b/pkgs/applications/science/logic/alt-ergo/default.nix
@@ -2,11 +2,11 @@
 
 let
   pname = "alt-ergo";
-  version = "2.5.4";
+  version = "2.6.0";
 
   src = fetchurl {
     url = "https://github.com/OCamlPro/alt-ergo/releases/download/v${version}/alt-ergo-${version}.tbz";
-    hash = "sha256-AsHok5i62vqJ5hK8XRiD8hM6JQaFv3dMxZAcVYEim6w=";
+    hash = "sha256-EmkxGvJSeKRmiSuoeMyIi6WfF39T3QPxKixiOwP8834=";
   };
 in
 
@@ -14,7 +14,17 @@ let alt-ergo-lib = ocamlPackages.buildDunePackage rec {
   pname = "alt-ergo-lib";
   inherit version src;
   buildInputs = with ocamlPackages; [ ppx_blob ];
-  propagatedBuildInputs = with ocamlPackages; [ camlzip dolmen_loop dune-build-info fmt ocplib-simplex seq stdlib-shims zarith ];
+  propagatedBuildInputs = with ocamlPackages; [
+    camlzip
+    dolmen_loop
+    dune-build-info
+    fmt
+    ocplib-simplex
+    ppx_deriving
+    seq
+    stdlib-shims
+    zarith
+  ];
 }; in
 
 let alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
@@ -29,7 +39,17 @@ ocamlPackages.buildDunePackage {
   inherit pname version src;
 
   nativeBuildInputs = [ ocamlPackages.menhir ] ++ lib.optionals stdenv.hostPlatform.isDarwin [ darwin.sigtool ];
-  buildInputs = [ alt-ergo-parsers ] ++ (with ocamlPackages; [ cmdliner dune-site ]);
+  propagatedBuildInputs = [ alt-ergo-parsers ] ++ (with ocamlPackages; [ cmdliner dune-site ppxlib ]);
+
+  outputs = [ "bin" "out" ];
+
+  installPhase = ''
+    runHook preInstall
+    dune install --prefix $bin ${pname}
+    mkdir -p $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib
+    mv $bin/lib/alt-ergo $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/
+    runHook postInstall
+  '';
 
   meta = {
     description = "High-performance theorem prover and SMT solver";
diff --git a/pkgs/development/ocaml-modules/dolmen/default.nix b/pkgs/development/ocaml-modules/dolmen/default.nix
index fede56388a77..ccecc8a33f76 100644
--- a/pkgs/development/ocaml-modules/dolmen/default.nix
+++ b/pkgs/development/ocaml-modules/dolmen/default.nix
@@ -1,22 +1,23 @@
 { lib, fetchurl, buildDunePackage
 , menhir, menhirLib
 , fmt
+, hmap
 , qcheck
 }:
 
 buildDunePackage rec {
   pname = "dolmen";
-  version = "0.9";
+  version = "0.10";
 
   minimalOCamlVersion = "4.08";
 
   src = fetchurl {
     url = "https://github.com/Gbury/dolmen/releases/download/v${version}/dolmen-${version}.tbz";
-    hash = "sha256-AD21OFS6zDoz+lXtac95gXwQNppPfGvpRK8dzDZXigo=";
+    hash = "sha256-xchfd+OSTzeOjYLxZu7+QTG04EG/nN7KRnQQ8zxx+mE=";
   };
 
   nativeBuildInputs = [ menhir ];
-  propagatedBuildInputs = [ menhirLib fmt ];
+  propagatedBuildInputs = [ menhirLib fmt hmap ];
 
   doCheck = true;
 
diff --git a/pkgs/development/ocaml-modules/dolmen/loop.nix b/pkgs/development/ocaml-modules/dolmen/loop.nix
index 19349bcb6e6a..572c161edc49 100644
--- a/pkgs/development/ocaml-modules/dolmen/loop.nix
+++ b/pkgs/development/ocaml-modules/dolmen/loop.nix
@@ -1,6 +1,7 @@
 { buildDunePackage, dolmen, dolmen_type
 , gen
 , pp_loc
+, mdx
 }:
 
 buildDunePackage {
@@ -9,6 +10,10 @@ buildDunePackage {
 
   propagatedBuildInputs = [ dolmen dolmen_type gen pp_loc ];
 
+  doCheck = true;
+  nativeCheckInputs = [ mdx.bin ];
+  checkInputs = [ mdx ];
+
   meta = dolmen.meta // {
     description = "Tool library for automated deduction tools";
   };