From a4d52834afa95f4003c7a825dcbee4ed8abc5c11 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 12 Jan 2026 09:59:40 +0100
Subject: [PATCH] rocqPackages.mathcomp: init at 2.5.0

---
 .../coq-modules/mathcomp/default.nix          |  58 ++++++--
 .../rocq-modules/mathcomp/default.nix         | 138 ++++++++++++++++++
 pkgs/top-level/rocq-packages.nix              |   8 +
 3 files changed, 193 insertions(+), 11 deletions(-)
 create mode 100644 pkgs/development/rocq-modules/mathcomp/default.nix

diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index e126fcf65481..f89d9bbae9e5 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -99,6 +99,15 @@ let
     "character" = [ "field" ];
     "all" = [ "character" ];
   };
+  meta = {
+    homepage = "https://math-comp.github.io/";
+    license = lib.licenses.cecill-b;
+    maintainers = with lib.maintainers; [
+      vbgl
+      jwiegley
+      cohencyril
+    ];
+  };
 
   mathcomp_ =
     package:
@@ -121,6 +130,7 @@ let
             releaseRev
             repo
             owner
+            meta
             ;
 
           mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
@@ -147,16 +157,6 @@ let
             cd ${pkgpath} || cd ssreflect  # before 2.5, boot didn't exist, make it behave as ssreflect
           ''
           + lib.optionalString (package == "all") pkgallMake;
-
-          meta = {
-            homepage = "https://math-comp.github.io/";
-            license = lib.licenses.cecill-b;
-            maintainers = with lib.maintainers; [
-              vbgl
-              jwiegley
-              cohencyril
-            ];
-          };
         }
         // lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }
         // lib.optionalAttrs withDoc {
@@ -244,4 +244,40 @@ let
     in
     patched-derivation5;
 in
-mathcomp_ (if single then "single" else "all")
+# this is just a wrapper for rocqPackages.mathcomp for Rocq >= 9.0
+if coq.rocqPackages ? mathcomp && version != "2.3.0" && version != "2.4.0" then
+  let
+    mc = coq.rocqPackages.mathcomp.override {
+      inherit version withDoc single;
+      inherit
+        ncurses
+        graphviz
+        lua
+        fetchzip
+        hierarchy-builder
+        ;
+      inherit (coq.rocqPackages) rocq-core;
+    };
+  in
+  mc
+  // {
+    ssreflect = mkCoqDerivation {
+      inherit
+        version
+        defaultVersion
+        release
+        releaseRev
+        repo
+        owner
+        meta
+        ;
+      pname = "mathcomp-ssreflect";
+      propagatedBuildInputs = [
+        mc.boot
+        mc.order
+      ];
+      preBuild = "cd ssreflect";
+    };
+  }
+else
+  mathcomp_ (if single then "single" else "all")
diff --git a/pkgs/development/rocq-modules/mathcomp/default.nix b/pkgs/development/rocq-modules/mathcomp/default.nix
new file mode 100644
index 000000000000..160febe58cb6
--- /dev/null
+++ b/pkgs/development/rocq-modules/mathcomp/default.nix
@@ -0,0 +1,138 @@
+############################################################################
+# This file mainly provides the `mathcomp` derivation, which is            #
+# essentially a meta-package containing all core mathcomp libraries        #
+# (boot order fingroup algebra solvable field character). They can be      #
+# accessed individually through the passthrough attributes of mathcomp     #
+# bearing the same names (mathcomp.boot, etc).                             #
+############################################################################
+# Compiling a custom version of mathcomp using `mathcomp.override`.        #
+# This is the replacement for the former `mathcomp_ config` function.      #
+# See the documentation at doc/languages-frameworks/coq.section.md.        #
+############################################################################
+
+{
+  lib,
+  ncurses,
+  graphviz,
+  lua,
+  fetchzip,
+  mkRocqDerivation,
+  withDoc ? false,
+  single ? false,
+  rocq-core,
+  hierarchy-builder,
+  version ? null,
+}@args:
+
+let
+  repo = "mathcomp";
+  owner = "math-comp";
+  withDoc = single && (args.withDoc or false);
+  defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+      inherit (lib.versions) range;
+    in
+    lib.switch rocq-core.rocq-version [
+      (case (range "9.0" "9.1") "2.5.0")
+    ] null;
+  release = {
+    "2.5.0".sha256 = "sha256-M/6IP4WhTQ4j2Bc8nXBXjSjWO08QzNIYI+a2owfOh+8=";
+  };
+  releaseRev = v: "mathcomp-${v}";
+
+  # list of core mathcomp packages sorted by dependency order
+  packages = {
+    "boot" = [ ];
+    "order" = [ "boot" ];
+    "fingroup" = [ "boot" ];
+    "algebra" = [
+      "order"
+      "fingroup"
+    ];
+    "solvable" = [ "algebra" ];
+    "field" = [ "solvable" ];
+    "character" = [ "field" ];
+    "all" = [ "character" ];
+  };
+
+  mathcomp_ =
+    package:
+    let
+      mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
+      pkgpath = if package == "single" then "." else package;
+      pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
+      pkgallMake = ''
+        echo "all.v"  > Make
+        echo "-I ." >>   Make
+        echo "-R . mathcomp.all" >> Make
+      '';
+      derivation = mkRocqDerivation (
+        {
+          inherit
+            version
+            pname
+            defaultVersion
+            release
+            releaseRev
+            repo
+            owner
+            ;
+
+          nativeBuildInputs = lib.optionals withDoc [
+            graphviz
+            lua
+          ];
+          buildInputs = [ ncurses ];
+          propagatedBuildInputs = mathcomp-deps ++ [ hierarchy-builder ];
+
+          buildFlags = lib.optional withDoc "doc";
+
+          preBuild = ''
+            if [[ -f etc/buildlibgraph ]]
+            then patchShebangs etc/buildlibgraph
+            fi
+          ''
+          + ''
+            cd ${pkgpath}
+          ''
+          + lib.optionalString (package == "all") pkgallMake;
+
+          meta = {
+            homepage = "https://math-comp.github.io/";
+            license = lib.licenses.cecill-b;
+            maintainers = with lib.maintainers; [
+              vbgl
+              jwiegley
+              cohencyril
+            ];
+          };
+        }
+        // lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }
+        // lib.optionalAttrs withDoc {
+          htmldoc_template = fetchzip {
+            url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
+            sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";
+          };
+          postBuild = ''
+            cp -rf _build_doc/* .
+            rm -r _build_doc
+          '';
+          postInstall =
+            let
+              tgt = "$out/share/coq/${rocq-core.rocq-version}/";
+            in
+            lib.optionalString withDoc ''
+              mkdir -p ${tgt}
+              cp -r htmldoc ${tgt}
+              cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
+            '';
+          buildTargets = "doc";
+          extraInstallFlags = [ "-f Makefile.coq" ];
+        }
+      );
+      # patched-derivation1 = derivation.overrideAttrs ...
+    in
+    derivation;
+in
+mathcomp_ (if single then "single" else "all")
diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix
index 0b1497f48821..84f6f26bb8c4 100644
--- a/pkgs/top-level/rocq-packages.nix
+++ b/pkgs/top-level/rocq-packages.nix
@@ -37,6 +37,14 @@ let
 
       bignums = callPackage ../development/rocq-modules/bignums { };
       hierarchy-builder = callPackage ../development/rocq-modules/hierarchy-builder { };
+      mathcomp = callPackage ../development/rocq-modules/mathcomp { };
+      mathcomp-boot = self.mathcomp.boot;
+      mathcomp-order = self.mathcomp.order;
+      mathcomp-fingroup = self.mathcomp.fingroup;
+      mathcomp-algebra = self.mathcomp.algebra;
+      mathcomp-solvable = self.mathcomp.solvable;
+      mathcomp-field = self.mathcomp.field;
+      mathcomp-character = self.mathcomp.character;
       parseque = callPackage ../development/rocq-modules/parseque { };
       rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };
       stdlib = callPackage ../development/rocq-modules/stdlib { };