From e8ec89d76f69364bc3cb3c33568fc75641ebb6f6 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 23 Jul 2026 15:06:34 +0200
Subject: [PATCH] rocqPackages.stdlib: merge with coqPackages.stdlib

---
 .../coq-modules/stdlib/default.nix            | 55 --------------
 .../rocq-modules/stdlib/default.nix           | 75 ++++++++++++-------
 pkgs/top-level/coq-packages.nix               |  2 +-
 3 files changed, 50 insertions(+), 82 deletions(-)
 delete mode 100644 pkgs/development/coq-modules/stdlib/default.nix

diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix
deleted file mode 100644
index 2871b536e839..000000000000
--- a/pkgs/development/coq-modules/stdlib/default.nix
+++ /dev/null
@@ -1,55 +0,0 @@
-{
-  coq,
-  mkCoqDerivation,
-  lib,
-  version ? null,
-}:
-
-let
-  derivation = mkCoqDerivation {
-
-    pname = "stdlib";
-    repo = "stdlib";
-    owner = "coq";
-    opam-name = "coq-stdlib";
-
-    inherit version;
-    defaultVersion =
-      let
-        case = case: out: { inherit case out; };
-      in
-      with lib.versions;
-      lib.switch coq.coq-version [
-        (case (isLe "9.1") "9.0.0")
-        # the < 9.0 above is artificial as stdlib was included in Coq before
-      ] null;
-    releaseRev = v: "V${v}";
-
-    release."9.0.0".hash = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
-
-    configurePhase = ''
-      echo no configuration
-    '';
-    buildPhase = ''
-      echo building nothing
-    '';
-    installPhase = ''
-      echo installing nothing
-      # Make an output directory rather than a file, so this is more friendly to buildEnv
-      mkdir $out
-    '';
-
-    meta = {
-      description = "Compatibility metapackage for Coq Stdlib library after the Rocq renaming";
-      license = lib.licenses.lgpl21Only;
-    };
-  };
-in
-# this is just a wrapper for rocqPackages.stdlib for Rocq >= 9.0
-if coq.rocqPackages ? stdlib then
-  coq.rocqPackages.stdlib.override {
-    inherit version;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  derivation
diff --git a/pkgs/development/rocq-modules/stdlib/default.nix b/pkgs/development/rocq-modules/stdlib/default.nix
index b16f2903937f..7e97327c69a4 100644
--- a/pkgs/development/rocq-modules/stdlib/default.nix
+++ b/pkgs/development/rocq-modules/stdlib/default.nix
@@ -4,35 +4,58 @@
   lib,
   version ? null,
 }:
-mkRocqDerivation {
 
-  pname = "stdlib";
-  repo = "stdlib";
-  owner = "rocq-prover";
-  opam-name = "rocq-stdlib";
+let
+  derivation = mkRocqDerivation {
 
-  inherit version;
-  defaultVersion =
-    let
-      case = case: out: { inherit case out; };
-    in
-    with lib.versions;
-    lib.switch rocq-core.version [
-      (case (range "9.3" "9.3") "9.2.0")
-      (case (range "9.2" "9.2") "9.1.0")
-      (case (range "9.0" "9.1") "9.0.0")
-    ] null;
-  releaseRev = v: "V${v}";
+    pname = "stdlib";
+    repo = "stdlib";
+    owner = "rocq-prover";
+    opam-name = "rocq-stdlib";
 
-  release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
-  release."9.1.0".sha256 = "sha256-D/kCMsJDg5OnP37GhvXIr2Fi/xCbgCCzoikKx5rL6p4=";
-  release."9.2.0".sha256 = "sha256-ySNY8XUQOH6B1B2p+39jdJ7UjIMrRDl499JJwpLEHuM=";
+    inherit version;
+    defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
+      with lib.versions;
+      lib.switch rocq-core.version [
+        (case (range "9.3" "9.3") "9.2.0")
+        (case (range "9.2" "9.2") "9.1.0")
+        (case (isLe "9.1") "9.0.0")
+      ] null;
+    releaseRev = v: "V${v}";
 
-  mlPlugin = true;
+    release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
+    release."9.1.0".sha256 = "sha256-D/kCMsJDg5OnP37GhvXIr2Fi/xCbgCCzoikKx5rL6p4=";
+    release."9.2.0".sha256 = "sha256-ySNY8XUQOH6B1B2p+39jdJ7UjIMrRDl499JJwpLEHuM=";
+
+    mlPlugin = true;
+
+    meta = {
+      description = "Rocq Proof Assistant -- Standard Library";
+      license = lib.licenses.lgpl21Only;
+    };
 
-  meta = {
-    description = "Rocq Proof Assistant -- Standard Library";
-    license = lib.licenses.lgpl21Only;
   };
-
-}
+  # the < 9.0 above is artificial as stdlib was included in Coq before
+  patched-derivation = derivation.overrideAttrs (
+    o:
+    lib.optionalAttrs
+      (rocq-core.rocq-version != "dev" && lib.versions.isLe "8.20" rocq-core.rocq-version)
+      {
+        configurePhase = ''
+          echo no configuration
+        '';
+        buildPhase = ''
+          echo building nothing
+        '';
+        installPhase = ''
+          echo installing nothing
+          # Make an output directory rather than a file, so this is more friendly to buildEnv
+          mkdir $out
+        '';
+      }
+  );
+in
+patched-derivation
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index c2b915f0e33c..247c9e09a455 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -230,7 +230,7 @@ let
       ssprove = callPackage ../development/coq-modules/ssprove { };
       stalmarck-tactic = callPackage ../development/coq-modules/stalmarck { };
       stalmarck = self.stalmarck-tactic.stalmarck;
-      stdlib = callPackage ../development/coq-modules/stdlib { };
+      stdlib = callPackage ../development/rocq-modules/stdlib { };
       stdpp = callPackage ../development/coq-modules/stdpp { };
       StructTact = callPackage ../development/coq-modules/StructTact { };
       tlc = callPackage ../development/coq-modules/tlc { };