Change default Rocq packages' name prefix (#541801)

doc/languages-frameworks/rocq.section.md

@@ -59,7 +59,7 @@ The recommended way of defining a derivation for a Rocq library, is to use the `
 * `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags,
 * `releaseArtifact` (optional, defaults to `(v: null)`), provides a default mapping from release names to artifact names (only works for github artifact for now),
 * `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers,
-* `namePrefix` (optional, defaults to `[ "rocq-core" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
+* `namePrefix` (optional, defaults to `[ "rocq" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
 * `nativeBuildInputs` (optional), is a list of executables that are required to build the current derivation, in addition to the default ones (namely `which`, `dune` and `ocaml` depending on whether `useDune`, `useDuneifVersion` and `mlPlugin` are set).
 * `extraNativeBuildInputs` (optional, deprecated), an additional list of derivation to add to `nativeBuildInputs`,
 * `overrideNativeBuildInputs` (optional) replaces the default list of derivation to which `nativeBuildInputs` and `extraNativeBuildInputs` adds extra elements,

pkgs/build-support/rocq/default.nix

@@ -55,7 +55,7 @@ in
   extraNativeBuildInputs ? [ ],
   overrideBuildInputs ? [ ],
   overrideNativeBuildInputs ? [ ],
-  namePrefix ? [ "rocq-core" ],
+  namePrefix ? null,
   enableParallelBuilding ? true,
   extraInstallFlags ? [ ],
   setROCQBIN ? true,
@@ -66,7 +66,7 @@ in
   dropDerivationAttrs ? [ ],
   useDuneifVersion ? (x: false),
   useDune ? false,
-  opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])),
+  opam-name ? null,
   useCoq ? false,
   useCoqifVersion ? (x: false),
   ...
@@ -160,10 +160,17 @@ let
       ] ""
     )
     + optionalString (v == null) "-broken";
-  append-version = p: n: p + display-pkg n "" rocqPackages.${n}.version + "-";
-  prefix-name = foldl append-version "" namePrefix;
   useDune = args.useDune or (useDuneifVersion fetched.version);
   useCoq = args.useCoq or (useCoqifVersion fetched.version);
+  namePrefix = args.namePrefix or [ (if useCoq then "coq" else "rocq") ];
+  append-version =
+    p: n:
+    let
+      version = if n == "rocq" then rocqPackages.rocq-core.version else rocqPackages.${n}.version;
+    in
+    p + display-pkg n "" version + "-";
+  prefix-name = foldl append-version "" namePrefix;
+  opam-name = args.opam-name or (concatStringsSep "-" (namePrefix ++ [ pname ]));
   rocq-core = if useCoq then coq // { rocq-version = coq.coq-version; } else args0.rocq-core;
   rocqlib-flags = [
     "COQLIBINSTALL=$(out)/lib/coq/${rocq-core.rocq-version}/user-contrib"

pkgs/development/rocq-modules/mathcomp-analysis/default.nix

@@ -85,7 +85,7 @@ let
           ;
 
         namePrefix = [
-          "rocq-core"
+          "rocq"
           "mathcomp"
         ];
 

pkgs/development/rocq-modules/mathcomp-bigenough/default.nix

@@ -9,7 +9,7 @@
 mkRocqDerivation {
 
   namePrefix = [
-    "rocq-core"
+    "rocq"
     "mathcomp"
   ];
   pname = "bigenough";

pkgs/development/rocq-modules/mathcomp-finmap/default.nix

@@ -9,7 +9,7 @@
 mkRocqDerivation {
 
   namePrefix = [
-    "rocq-core"
+    "rocq"
     "mathcomp"
   ];
   pname = "finmap";

pkgs/development/rocq-modules/mathcomp-real-closed/default.nix

@@ -10,7 +10,7 @@
 mkRocqDerivation {
 
   namePrefix = [
-    "rocq-core"
+    "rocq"
     "mathcomp"
   ];
   pname = "real-closed";