From 72618038521eb9a97f44261443b4f006a917fc36 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 20 Oct 2025 06:26:48 +0200
Subject: [PATCH 1/2] ocamlPackages.dolmen_model: init at 0.10

---
 .../ocaml-modules/dolmen/model.nix            | 25 +++++++++++++++++++
 pkgs/top-level/ocaml-packages.nix             |  2 ++
 2 files changed, 27 insertions(+)
 create mode 100644 pkgs/development/ocaml-modules/dolmen/model.nix

diff --git a/pkgs/development/ocaml-modules/dolmen/model.nix b/pkgs/development/ocaml-modules/dolmen/model.nix
new file mode 100644
index 000000000000..7c299fbc7cfb
--- /dev/null
+++ b/pkgs/development/ocaml-modules/dolmen/model.nix
@@ -0,0 +1,25 @@
+{
+  buildDunePackage,
+  dolmen,
+  dolmen_loop,
+  farith,
+  ppx_deriving,
+  zarith,
+}:
+
+buildDunePackage {
+  pname = "dolmen_model";
+  inherit (dolmen) src version;
+
+  propagatedBuildInputs = [
+    dolmen
+    dolmen_loop
+    farith
+    ppx_deriving
+    zarith
+  ];
+
+  meta = dolmen.meta // {
+    description = "Dolmen library for verifying models generated by automated theorem provers and SMT solvers";
+  };
+}
diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index 86e4c306066e..290ed9741029 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -424,6 +424,8 @@ let
 
         dolmen_lsp = callPackage ../development/ocaml-modules/dolmen/lsp.nix { };
 
+        dolmen_model = callPackage ../development/ocaml-modules/dolmen/model.nix { };
+
         dolmen_type = callPackage ../development/ocaml-modules/dolmen/type.nix { };
 
         dolog = callPackage ../development/ocaml-modules/dolog { };

From 79fef7e3b56b4aa2946a46f0c3b1adc81e53cf56 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 20 Oct 2025 06:26:55 +0200
Subject: [PATCH 2/2] =?UTF-8?q?ocamlPackages.smtml:=200.10.0=20=E2=86=92?=
 =?UTF-8?q?=200.12.0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../ocaml-modules/smtml/default.nix           | 23 +++++++++++++------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/pkgs/development/ocaml-modules/smtml/default.nix b/pkgs/development/ocaml-modules/smtml/default.nix
index 2ec614fbb543..d8426a8fc52b 100644
--- a/pkgs/development/ocaml-modules/smtml/default.nix
+++ b/pkgs/development/ocaml-modules/smtml/default.nix
@@ -7,10 +7,12 @@
   menhir,
   bos,
   cmdliner,
+  dolmen_model,
   dolmen_type,
   fpath,
   hc,
   menhirLib,
+  mtime,
   # fix eval on legacy ocaml versions
   ocaml_intrinsics ? null,
   patricia-tree,
@@ -23,15 +25,15 @@
   ounit2,
 }:
 
-buildDunePackage rec {
+buildDunePackage (finalAttrs: {
   pname = "smtml";
-  version = "0.10.0";
+  version = "0.12.0";
 
   src = fetchFromGitHub {
     owner = "formalsec";
     repo = "smtml";
-    tag = "v${version}";
-    hash = "sha256-WXGYk/zJnW6QzHKCHl0lkmYb/pG90/sAOK40wYzK35U=";
+    tag = "v${finalAttrs.version}";
+    hash = "sha256-WETSvhy5OfztOTqJimym0OaZLo053nl8pcoQlyyP8I0=";
   };
 
   nativeBuildInputs = [
@@ -41,10 +43,12 @@ buildDunePackage rec {
   propagatedBuildInputs = [
     bos
     cmdliner
+    dolmen_model
     dolmen_type
     fpath
     hc
     menhirLib
+    mtime
     ocaml_intrinsics
     patricia-tree
     prelude
@@ -63,14 +67,19 @@ buildDunePackage rec {
     mdx.bin
   ];
 
-  doCheck = !(lib.versions.majorMinor ocaml.version == "5.0" || stdenv.hostPlatform.isDarwin);
+  doCheck =
+    !(
+      lib.versions.majorMinor ocaml.version == "5.0"
+      || lib.versions.majorMinor ocaml.version == "5.4"
+      || stdenv.hostPlatform.isDarwin
+    );
 
   meta = {
     description = "SMT solver frontend for OCaml";
     homepage = "https://formalsec.github.io/smtml/smtml/";
     downloadPage = "https://github.com/formalsec/smtml";
-    changelog = "https://github.com/formalsec/smtml/releases/tag/v${version}";
+    changelog = "https://github.com/formalsec/smtml/releases/tag/v${finalAttrs.version}";
     license = lib.licenses.mit;
     maintainers = [ lib.maintainers.ethancedwards8 ];
   };
-}
+})