From 1d5b338a702df84b5bca635b589a23ef88cbe4ae Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Thu, 4 Jun 2026 14:32:05 +0200
Subject: [PATCH] coqPackages_8_20.coq-elpi: fix build

coqPackages_8_20.stalmarck-tactic: fix build
---
 pkgs/applications/science/logic/coq/default.nix    | 14 ++++++++++++++
 pkgs/by-name/du/dune/package.nix                   |  1 +
 pkgs/development/coq-modules/coq-elpi/default.nix  |  3 ++-
 pkgs/development/coq-modules/stalmarck/default.nix |  3 ++-
 pkgs/top-level/coq-packages.nix                    |  1 +
 5 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index a5f7e9e861aa..cee47f70a062 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -105,11 +105,25 @@ let
     substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
     substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
   '';
+  dune =
+    if lib.versions.isEq coq-version "8.20" then
+      args.dune.override { version = "3.21.1"; }
+    else
+      args.dune;
   ocamlPackages =
     if customOCamlPackages != null then
       customOCamlPackages
     else
       lib.switch coq-version [
+        {
+          case = lib.versions.isEq "8.20";
+          out = ocamlPackages_4_14.overrideScope (
+            self: super: {
+              inherit dune;
+              dune_3 = dune;
+            }
+          );
+        }
         {
           case = lib.versions.range "8.16" "9.1";
           out = ocamlPackages_4_14;
diff --git a/pkgs/by-name/du/dune/package.nix b/pkgs/by-name/du/dune/package.nix
index e4aa233bf37b..0dfaf0a82ca8 100644
--- a/pkgs/by-name/du/dune/package.nix
+++ b/pkgs/by-name/du/dune/package.nix
@@ -22,6 +22,7 @@ stdenv.mkDerivation {
     hash =
       {
         "3.22.2" = "sha256-wsz4vGsXr6R8RQKXNXSWMDqnyGgOMpt52Yxo41AToRg=";
+        "3.21.1" = "sha256-hPeoLG2ApxJPOEfppInoDPvq+3vtNXOsAShu9W/QjZQ=";
         "2.9.3" = "sha256:1ml8bxym8sdfz25bx947al7cvsi2zg5lcv7x9w6xb01cmdryqr9y";
       }
       ."${version}";
diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix
index b0134851418b..0f8f15d72388 100644
--- a/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/pkgs/development/coq-modules/coq-elpi/default.nix
@@ -2,6 +2,7 @@
   lib,
   mkCoqDerivation,
   which,
+  dune,
   coq,
   stdlib,
   version ? null,
@@ -33,7 +34,7 @@ let
   propagatedBuildInputs_wo_elpi = [
     coq.ocamlPackages.findlib
   ];
-  derivation = mkCoqDerivation {
+  derivation = mkCoqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
     pname = "elpi";
     repo = "coq-elpi";
     owner = "LPCIC";
diff --git a/pkgs/development/coq-modules/stalmarck/default.nix b/pkgs/development/coq-modules/stalmarck/default.nix
index e493321d8a0a..369fea9639e3 100644
--- a/pkgs/development/coq-modules/stalmarck/default.nix
+++ b/pkgs/development/coq-modules/stalmarck/default.nix
@@ -1,6 +1,7 @@
 {
   lib,
   mkCoqDerivation,
+  dune,
   coq,
   stdlib,
   version ? null,
@@ -38,7 +39,7 @@ let
         else
           "A two-level approach to prove tautologies using Stålmarck's algorithm in Coq.";
     in
-    mkCoqDerivation {
+    mkCoqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
       inherit
         version
         pname
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index b2cd7f2ada19..a93fb26666c9 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -17,6 +17,7 @@
   fetchpatch,
   makeWrapper,
   coq2html,
+  dune,
 }@args:
 let
   lib = import ../build-support/coq/extra-lib.nix { inherit (args) lib; };