From 96af9f8acf9c0efede30e85a4706db1082f4e9ba Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 21 Apr 2026 08:28:20 +0200
Subject: [PATCH] rocqPackages.mathcomp: rename fingroup -> finite-group and
 character -> group-representation

---
 .../coq-modules/mathcomp/default.nix          |  2 ++
 .../rocq-modules/mathcomp/default.nix         | 26 ++++++++++++-------
 pkgs/top-level/coq-packages.nix               |  2 ++
 pkgs/top-level/rocq-packages.nix              |  6 +++--
 4 files changed, 25 insertions(+), 11 deletions(-)

diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index f89d9bbae9e5..943d4b67a418 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -278,6 +278,8 @@ if coq.rocqPackages ? mathcomp && version != "2.3.0" && version != "2.4.0" then
       ];
       preBuild = "cd ssreflect";
     };
+    fingroup = mc.finite-group;
+    character = mc.group-representation;
   }
 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
index 5285a277c810..32669add7037 100644
--- a/pkgs/development/rocq-modules/mathcomp/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp/default.nix
@@ -1,9 +1,9 @@
 ############################################################################
 # 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).                             #
+# (boot order finite-group algebra solvable field group-representation).   #
+# 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.      #
@@ -45,22 +45,30 @@ let
   packages = {
     "boot" = [ ];
     "order" = [ "boot" ];
-    "fingroup" = [ "boot" ];
+    "finite-group" = [ "boot" ];
     "algebra" = [
       "order"
-      "fingroup"
+      "finite-group"
     ];
     "solvable" = [ "algebra" ];
     "field" = [ "solvable" ];
-    "character" = [ "field" ];
-    "all" = [ "character" ];
+    "group-representation" = [ "field" ];
+    "all" = [ "group-representation" ];
   };
 
   mathcomp_ =
     package:
     let
       mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
-      pkgpath = if package == "single" then "." else package;
+      cdpkg =
+        if package == "single" then
+          "cd ."
+        else if package == "group-representation" then
+          "cd group_representation || cd character"
+        else if package == "finite-group" then
+          "cd finite_group || cd fingroup"
+        else
+          "cd ${package}";
       pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
       pkgallMake = ''
         echo "all.v"  > Make
@@ -94,7 +102,7 @@ let
             fi
           ''
           + ''
-            cd ${pkgpath}
+            ${cdpkg}
           ''
           + lib.optionalString (package == "all") pkgallMake;
 
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index ed7bfa5626d9..995f14930b8e 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -152,10 +152,12 @@ let
       mathcomp-boot = self.mathcomp.boot;
       mathcomp-order = self.mathcomp.order;
       mathcomp-ssreflect = self.mathcomp.ssreflect;
+      mathcomp-finite-group = self.mathcomp.fingroup;
       mathcomp-fingroup = self.mathcomp.fingroup;
       mathcomp-algebra = self.mathcomp.algebra;
       mathcomp-solvable = self.mathcomp.solvable;
       mathcomp-field = self.mathcomp.field;
+      mathcomp-group-representation = self.mathcomp.character;
       mathcomp-character = self.mathcomp.character;
       mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel { };
       mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics { };
diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix
index b5efdf4b6c56..a6ca3f9b04c9 100644
--- a/pkgs/top-level/rocq-packages.nix
+++ b/pkgs/top-level/rocq-packages.nix
@@ -42,11 +42,13 @@ let
       mathcomp = callPackage ../development/rocq-modules/mathcomp { };
       mathcomp-boot = self.mathcomp.boot;
       mathcomp-order = self.mathcomp.order;
-      mathcomp-fingroup = self.mathcomp.fingroup;
+      mathcomp-finite-group = self.mathcomp.finite-group;
+      mathcomp-fingroup = self.mathcomp-finite-group;
       mathcomp-algebra = self.mathcomp.algebra;
       mathcomp-solvable = self.mathcomp.solvable;
       mathcomp-field = self.mathcomp.field;
-      mathcomp-character = self.mathcomp.character;
+      mathcomp-group-representation = self.mathcomp.group-representation;
+      mathcomp-character = self.mathcomp-group-representation;
       mathcomp-analysis = callPackage ../development/rocq-modules/mathcomp-analysis { };
       mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib;
       mathcomp-bigenough = callPackage ../development/rocq-modules/mathcomp-bigenough { };