gador/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

rocqPackages.mathcomp: rename fingroup -> finite-group and character -> group-representation

Browse Source
This commit is contained in:
Pierre Roux
2026-05-05 14:11:16 +02:00
parent c76cd16798
commit 96af9f8acf
4 changed files with 25 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/development/coq-modules/mathcomp/default.nix
+2
View File
@@ -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")
pkgs/development/rocq-modules/mathcomp/default.nix
+17 -9
View File
@@ -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;
pkgs/top-level/coq-packages.nix
+2
View File
@@ -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 { };
pkgs/top-level/rocq-packages.nix
+4 -2
View File
@@ -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 { };