From 44e4eed2ccf8a4b1da1d66557e07cae43c8ea2b6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Wed, 29 Jul 2026 09:11:54 +0200
Subject: [PATCH 1/3] ocamlPackages.elpi: fix typo

---
 pkgs/top-level/ocaml-packages.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index ba3abf469dce..171e217a2bc7 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -589,7 +589,7 @@ let
               };
           in
           {
-            ppx_deriving_0_15 = ppx_deriving_ "0.15";
+            ppx_deriving_0_15 = ppx_deriving_ "0.15.0";
             ppx_deriving_0_33 = ppx_deriving_ "0.33.0";
           }
         );

From eb037b56fd57ffbe6e4e80b8b33aecabca590d2d Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Wed, 29 Jul 2026 09:12:11 +0200
Subject: [PATCH 2/3] coqPackages.QuickChick: disable broken versions

---
 pkgs/development/coq-modules/QuickChick/default.nix | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
index a3b185f54d13..5862733207f0 100644
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -25,8 +25,8 @@
     lib.switch
       [ coq.coq-version mathcomp-boot.version ]
       [
-        (case (lib.versions.range "8.15" "9.1") lib.pred.true "2.1.1")
-        (case (lib.versions.range "8.13" "8.17") lib.pred.true "1.6.5")
+        (case (lib.versions.range "8.20" "9.1") lib.pred.true "2.1.1")
+        (case (lib.versions.range "8.13" "8.16") lib.pred.true "1.6.5")
         (case "8.13" lib.pred.true "1.5.0")
         (case "8.12" lib.pred.true "1.4.0")
         (case "8.11" lib.pred.true "1.3.2")

From 69904f2e6a80969ceafb4aabcd6e84bc516f42c6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Wed, 29 Jul 2026 09:44:59 +0200
Subject: [PATCH 3/3] coqPackages.simple-io: disable broken versions

Fix for Coq 8.20 by pinning dune to version 3.21.
---
 .../coq-modules/simple-io/default.nix         | 88 ++++++++++---------
 1 file changed, 47 insertions(+), 41 deletions(-)

diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/coq-modules/simple-io/default.nix
index 1aeaa3e7293a..4a92feef93c1 100644
--- a/pkgs/development/coq-modules/simple-io/default.nix
+++ b/pkgs/development/coq-modules/simple-io/default.nix
@@ -1,56 +1,62 @@
 {
   lib,
   callPackage,
-  mkCoqDerivation,
+  mkRocqDerivation,
   coq,
+  dune,
   ExtLib,
   version ? null,
 }:
 
-(mkCoqDerivation {
-  pname = "simple-io";
-  owner = "Lysxia";
-  repo = "coq-simple-io";
-  inherit version;
-  defaultVersion =
-    let
-      case = case: out: { inherit case out; };
-    in
-    with lib.versions;
-    lib.switch coq.coq-version [
-      (case (range "8.17" "9.1") "1.11.0")
-      (case (range "8.11" "8.19") "1.8.0")
-      (case (range "8.7" "8.13") "1.3.0")
-    ] null;
-  release."1.11.0".hash = "sha256-sgbH7eI4TPHOQ5qBvM6x7G3j8B40HSEMEzFaN1G9VEw=";
-  release."1.10.0".hash = "sha256-67cBhLvRMWLWBL7NXK1zZTQC4PtSKu9qtesU4SqKkOw=";
-  release."1.8.0".hash = "sha256-3ADNeXrBIpYRlfUW+LkLHUWV1w1HFrVc/TZISMuwvRY=";
-  release."1.7.0".hash = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci";
-  release."1.3.0".hash = "sha256:1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax";
-  mlPlugin = true;
-  nativeBuildInputs = [ coq.ocamlPackages.cppo ];
-  propagatedBuildInputs = [
-    ExtLib
-  ]
-  ++ (with coq.ocamlPackages; [
-    ocaml
-    findlib
-    ocamlbuild
-  ]);
+(mkRocqDerivation.override
+  (lib.optionalAttrs (coq.coq-version == "8.20") { dune = dune.override { version = "3.21.1"; }; })
+  {
+    useCoq = true;
+    namePrefix = [ "coq" ];
+    pname = "simple-io";
+    owner = "Lysxia";
+    repo = "coq-simple-io";
+    inherit version;
+    defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
+      with lib.versions;
+      lib.switch coq.coq-version [
+        (case (range "8.20" "9.1") "1.11.0")
+        (case (range "8.11" "8.16") "1.8.0")
+        (case (range "8.10" "8.13") "1.3.0")
+      ] null;
+    release."1.11.0".hash = "sha256-sgbH7eI4TPHOQ5qBvM6x7G3j8B40HSEMEzFaN1G9VEw=";
+    release."1.10.0".hash = "sha256-67cBhLvRMWLWBL7NXK1zZTQC4PtSKu9qtesU4SqKkOw=";
+    release."1.8.0".hash = "sha256-3ADNeXrBIpYRlfUW+LkLHUWV1w1HFrVc/TZISMuwvRY=";
+    release."1.7.0".hash = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci";
+    release."1.3.0".hash = "sha256:1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax";
+    mlPlugin = true;
+    nativeBuildInputs = [ coq.ocamlPackages.cppo ];
+    propagatedBuildInputs = [
+      ExtLib
+    ]
+    ++ (with coq.ocamlPackages; [
+      ocaml
+      findlib
+      ocamlbuild
+    ]);
 
-  doCheck = true;
-  checkTarget = "test";
+    doCheck = true;
+    checkTarget = "test";
 
-  useDuneifVersion = v: (lib.versionAtLeast v "1.10.0" || v == "dev");
+    useDuneifVersion = v: (lib.versionAtLeast v "1.10.0" || v == "dev");
 
-  passthru.tests.HelloWorld = callPackage ./test.nix { };
+    passthru.tests.HelloWorld = callPackage ./test.nix { };
 
-  meta = {
-    description = "Purely functional IO for Coq";
-    license = lib.licenses.mit;
-    maintainers = [ lib.maintainers.vbgl ];
-  };
-}).overrideAttrs
+    meta = {
+      description = "Purely functional IO for Coq";
+      license = lib.licenses.mit;
+      maintainers = [ lib.maintainers.vbgl ];
+    };
+  }
+).overrideAttrs
   (
     o:
     lib.optionalAttrs (lib.versionAtLeast o.version "1.8.0" || o.version == "dev") {