mkCoqDerivation: make a wrapper on top of mkRocqDerivation

2026-07-21 08:01:31 +00:00 · 2026-07-02 14:53:10 +02:00
parent ba7822a8d0
commit 0235b9517e
10 changed files with 38 additions and 263 deletions
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -79,7 +79,7 @@ let
  };
  releaseRev = v: "V${v}";
  fetched =
-    import ../../../../build-support/coq/meta-fetch/default.nix
+    import ../../../../build-support/rocq/meta-fetch/default.nix
      {
        inherit
          lib
--- a/pkgs/applications/science/logic/rocq-core/default.nix
+++ b/pkgs/applications/science/logic/rocq-core/default.nix
@@ -32,7 +32,7 @@ let
  };
  releaseRev = v: "V${v}";
  fetched =
-    import ../../../../build-support/coq/meta-fetch/default.nix
+    import ../../../../build-support/rocq/meta-fetch/default.nix
      {
        inherit
          lib
--- a/pkgs/build-support/coq/default.nix
+++ b/pkgs/build-support/coq/default.nix
@@ -1,246 +0,0 @@
-{
-  lib,
-  stdenv,
-  coqPackages,
-  coq,
-  which,
-  fetchzip,
-  fetchurl,
-  dune,
-}@args:
-
-let
-  lib = import ./extra-lib.nix {
-    inherit (args) lib;
-  };
-
-  inherit (lib)
-    concatStringsSep
-    flip
-    foldl
-    isFunction
-    isString
-    optional
-    optionalAttrs
-    optionals
-    optionalString
-    pred
-    remove
-    switch
-    versions
-    ;
-
-  inherit (lib.attrsets) removeAttrs;
-  inherit (lib.strings) match;
-
-  isGitHubDomain = d: match "^github.*" d != null;
-  isGitLabDomain = d: match "^gitlab.*" d != null;
-in
-
-{
-  pname,
-  version ? null,
-  fetcher ? null,
-  owner ? "rocq-community",
-  domain ? "github.com",
-  repo ? pname,
-  defaultVersion ? null,
-  releaseRev ? (v: v),
-  displayVersion ? { },
-  release ? { },
-  buildInputs ? [ ],
-  nativeBuildInputs ? [ ],
-  extraBuildInputs ? [ ],
-  extraNativeBuildInputs ? [ ],
-  overrideBuildInputs ? [ ],
-  overrideNativeBuildInputs ? [ ],
-  namePrefix ? [ "coq" ],
-  enableParallelBuilding ? true,
-  extraInstallFlags ? [ ],
-  setCOQBIN ? true,
-  mlPlugin ? false,
-  useMelquiondRemake ? null,
-  dropAttrs ? [ ],
-  keepAttrs ? [ ],
-  dropDerivationAttrs ? [ ],
-  useDuneifVersion ? (x: false),
-  useDune ? false,
-  opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])),
-  ...
-}@args:
-let
-  args-to-remove = foldl (flip remove) (
-    [
-      "version"
-      "fetcher"
-      "repo"
-      "owner"
-      "domain"
-      "releaseRev"
-      "displayVersion"
-      "defaultVersion"
-      "useMelquiondRemake"
-      "release"
-      "buildInputs"
-      "nativeBuildInputs"
-      "extraBuildInputs"
-      "extraNativeBuildInputs"
-      "overrideBuildInputs"
-      "overrideNativeBuildInputs"
-      "namePrefix"
-      "meta"
-      "useDuneifVersion"
-      "useDune"
-      "opam-name"
-      "extraInstallFlags"
-      "setCOQBIN"
-      "mlPlugin"
-      "dropAttrs"
-      "dropDerivationAttrs"
-      "keepAttrs"
-      "env"
-    ]
-    ++ dropAttrs
-  ) keepAttrs;
-  fetch =
-    import ../coq/meta-fetch/default.nix
-      {
-        inherit
-          lib
-          stdenv
-          fetchzip
-          fetchurl
-          ;
-      }
-      (
-        {
-          inherit release releaseRev;
-          location = { inherit domain owner repo; };
-        }
-        // optionalAttrs (args ? fetcher) { inherit fetcher; }
-      );
-  fetched = fetch (if version != null then version else defaultVersion);
-  display-pkg =
-    n: sep: v:
-    let
-      d = displayVersion.${n} or (if sep == "" then ".." else true);
-    in
-    n
-    + optionalString (v != "" && v != null) (
-      switch d [
-        {
-          case = true;
-          out = sep + v;
-        }
-        {
-          case = ".";
-          out = sep + versions.major v;
-        }
-        {
-          case = "..";
-          out = sep + versions.majorMinor v;
-        }
-        {
-          case = "...";
-          out = sep + versions.majorMinorPatch v;
-        }
-        {
-          case = isFunction;
-          out = optionalString (d v != "") (sep + d v);
-        }
-        {
-          case = isString;
-          out = optionalString (d != "") (sep + d);
-        }
-      ] ""
-    )
-    + optionalString (v == null) "-broken";
-  append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-";
-  prefix-name = foldl append-version "" namePrefix;
-  useDune = args.useDune or (useDuneifVersion fetched.version);
-  coqlib-flags = [
-    "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib"
-    "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)"
-  ];
-  docdir-flags = [ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ];
-  COQUSERCONTRIB = "$out/lib/coq/${coq.coq-version}/user-contrib";
-in
-stdenv.mkDerivation (
-  removeAttrs (
-    {
-
-      name = prefix-name + (display-pkg pname "-" fetched.version);
-
-      inherit (fetched) version src;
-
-      nativeBuildInputs =
-        args.overrideNativeBuildInputs or (
-          [ which ]
-          ++ optional useDune dune
-          ++ optionals (useDune || mlPlugin) [
-            coq.ocamlPackages.ocaml
-            coq.ocamlPackages.findlib
-          ]
-          ++ (args.nativeBuildInputs or [ ])
-          ++ extraNativeBuildInputs
-        );
-      buildInputs =
-        args.overrideBuildInputs or ([ coq ] ++ (args.buildInputs or [ ]) ++ extraBuildInputs);
-      inherit enableParallelBuilding;
-
-      env =
-        optionalAttrs setCOQBIN {
-          COQBIN = "${coq}/bin/";
-        }
-        // optionalAttrs (args ? useMelquiondRemake) {
-          inherit COQUSERCONTRIB;
-        }
-        // (args.env or { });
-
-      meta =
-        (
-          {
-            platforms = coq.meta.platforms;
-          }
-          // (switch domain [
-            {
-              case = pred.union isGitHubDomain isGitLabDomain;
-              out = {
-                homepage = "https://${domain}/${owner}/${repo}";
-              };
-            }
-          ] { })
-          // optionalAttrs (fetched.broken or false) {
-            coqFilter = true;
-            broken = true;
-          }
-        )
-        // (args.meta or { });
-
-    }
-    // (optionalAttrs (!args ? installPhase && !args ? useMelquiondRemake) {
-      installFlags = coqlib-flags ++ docdir-flags ++ extraInstallFlags;
-    })
-    // (optionalAttrs useDune {
-      buildPhase = ''
-        runHook preBuild
-        dune build -p ${opam-name} ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
-        runHook postBuild
-      '';
-      installPhase = ''
-        runHook preInstall
-        dune install --prefix=$out --libdir $OCAMLFIND_DESTDIR ${opam-name}
-        mkdir $out/lib/coq/
-        mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
-        runHook postInstall
-      '';
-    })
-    // (optionalAttrs (args ? useMelquiondRemake) {
-      preConfigurePhases = [ "autoconf" ];
-      configureFlags = [ "--libdir=${COQUSERCONTRIB}/${useMelquiondRemake.logpath or ""}" ];
-      buildPhase = "./remake -j$NIX_BUILD_CORES";
-      installPhase = "./remake install";
-    })
-    // (removeAttrs args args-to-remove)
-  ) dropDerivationAttrs
-)
--- a/pkgs/build-support/rocq/default.nix
+++ b/pkgs/build-support/rocq/default.nix
@@ -3,15 +3,16 @@
  stdenv,
  rocqPackages,
  rocq-core,
+  coq,
  which,
  fetchzip,
  fetchurl,
  dune,
-}@args:
+}@args0:

 let
  lib = import ./extra-lib.nix {
-    inherit (args) lib;
+    inherit (args0) lib;
  };

  inherit (lib)
@@ -66,6 +67,8 @@ in
  useDuneifVersion ? (x: false),
  useDune ? false,
  opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])),
+  useCoq ? false,
+  useCoqifVersion ? (x: false),
  ...
 }@args:
 let
@@ -99,11 +102,13 @@ let
      "dropDerivationAttrs"
      "keepAttrs"
      "env"
+      "useCoq"
+      "useCoqifVersion"
    ]
    ++ dropAttrs
  ) keepAttrs;
  fetch =
-    import ../coq/meta-fetch/default.nix
+    import ../rocq/meta-fetch/default.nix
      {
        inherit
          lib
@@ -158,6 +163,8 @@ let
  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);
+  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"
    "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)"
@@ -190,9 +197,10 @@ stdenv.mkDerivation (
      inherit enableParallelBuilding;

      env =
-        optionalAttrs setROCQBIN {
+        optionalAttrs (setROCQBIN && !useCoq) {
          ROCQBIN = "${rocq-core}/bin/";
        }
+        // optionalAttrs (setROCQBIN && useCoq) { COQBIN = "${rocq-core}/bin/"; }
        // optionalAttrs (args ? useMelquiondRemake) {
          inherit COQUSERCONTRIB;
        }
--- a/pkgs/build-support/rocq/meta-fetch/default.nix
+++ b/pkgs/build-support/rocq/meta-fetch/default.nix
--- a/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/pkgs/development/coq-modules/coq-elpi/default.nix
@@ -1,6 +1,6 @@
 {
  lib,
-  mkCoqDerivation,
+  mkRocqDerivation,
  which,
  dune,
  coq,
@@ -34,7 +34,9 @@ let
  propagatedBuildInputs_wo_elpi = [
    coq.ocamlPackages.findlib
  ];
-  derivation = mkCoqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
+  derivation = mkRocqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
+    useCoq = true;
+    namePrefix = [ "coq" ];
    pname = "elpi";
    repo = "coq-elpi";
    owner = "LPCIC";
--- a/pkgs/development/coq-modules/stalmarck/default.nix
+++ b/pkgs/development/coq-modules/stalmarck/default.nix
@@ -1,6 +1,6 @@
 {
  lib,
-  mkCoqDerivation,
+  mkRocqDerivation,
  dune,
  coq,
  stdlib,
@@ -39,7 +39,9 @@ let
        else
          "A two-level approach to prove tautologies using Stålmarck's algorithm in Coq.";
    in
-    mkCoqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
+    mkRocqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
+      useCoq = true;
+      namePrefix = [ "coq" ];
      inherit
        version
        pname
--- a/pkgs/development/coq-modules/vscoq-language-server/default.nix
+++ b/pkgs/development/coq-modules/vscoq-language-server/default.nix
@@ -82,7 +82,7 @@ ocamlPackages.buildDunePackage {
    license = lib.licenses.mit;
  }
  // lib.optionalAttrs (fetched.broken or false) {
-    coqFilter = true;
+    rocqFilter = true;
    broken = true;
  };
 }
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -27,14 +27,14 @@ let
    self: coq:
    let
      callPackage = self.callPackage;
-      coqPackages = self // {
+      rocqPackages = self // {
        recurseForDerivations = false;
      };
    in
    {
-      inherit coqPackages lib;
+      inherit rocqPackages lib;

-      metaFetch = import ../build-support/coq/meta-fetch/default.nix {
+      metaFetch = import ../build-support/rocq/meta-fetch/default.nix {
        inherit
          lib
          stdenv
@@ -42,7 +42,16 @@ let
          fetchurl
          ;
      };
-      mkCoqDerivation = lib.makeOverridable (callPackage ../build-support/coq { });
+      mkRocqDerivation = lib.makeOverridable (callPackage ../build-support/rocq { });
+      mkCoqDerivation =
+        args:
+        self.mkRocqDerivation (
+          {
+            useCoq = true;
+            namePrefix = [ "coq" ];
+          }
+          // args
+        );

      coq = coq.overrideAttrs (oldAttrs: {
        passthru = (oldAttrs.passthru or { }) // {
@@ -286,7 +295,7 @@ let
        let
          v = set.${name} or null;
        in
-        lib.optional (!v.meta.coqFilter or false) (
+        lib.optional (!v.meta.rocqFilter or false) (
          lib.nameValuePair name (
            if lib.isAttrs v && v.recurseForDerivations or false then filterCoqPackages v else v
          )
--- a/pkgs/top-level/rocq-packages.nix
+++ b/pkgs/top-level/rocq-packages.nix
@@ -26,7 +26,7 @@ let
        recurseForDerivations = false;
      };

-      metaFetch = import ../build-support/coq/meta-fetch/default.nix {
+      metaFetch = import ../build-support/rocq/meta-fetch/default.nix {
        inherit
          lib
          stdenv