Merge pull request #188766 from cdepillabout/overrideCoqDerivation

coqPackages.mkCoqDerivation: add a lib.overrideCoqDerivation function

pkgs/build-support/coq/extra-lib.nix

@@ -142,4 +142,52 @@ with builtins; with lib; recursiveUpdate lib (rec {
         if cl?case then compare cl.case var
         else all (equal true) (zipListsWith compare cl.cases var); in
     switch-if (map (cl: { cond = combine cl var; inherit (cl) out; }) clauses) default;
+
+  /* Override arguments to mkCoqDerivation for a Coq library.
+
+     This function allows you to easily override arguments to mkCoqDerivation,
+     even when they are not exposed by the Coq library directly.
+
+     Type: overrideCoqDerivation :: AttrSet -> CoqLibraryDerivation -> CoqLibraryDerivation
+
+     Example:
+
+     ```nix
+     coqPackages.lib.overrideCoqDerivation
+       {
+         defaultVersion = "9999";
+         release."9999".sha256 = "1lq8x86vd3vqqh2yq6hvyagpnhfq5wmk5pg2z0xq7b7dbbbhyfkw";
+       }
+       coqPackages.QuickChick;
+     ```
+
+     This example overrides the `defaultVersion` and `release` arguments that
+     are passed to `mkCoqDerivation` in the QuickChick derivation.
+
+     Note that there is a difference between using `.override` on a Coq
+     library vs this `overrideCoqDerivation` function. `.override` allows you
+     to modify arguments to the derivation itself, for instance by passing
+     different versions of dependencies:
+
+     ```nix
+     coqPackages.QuickChick.override { ssreflect = my-cool-ssreflect; }
+     ```
+
+     whereas `overrideCoqDerivation` allows you to override arguments to the
+     call to `mkCoqDerivation` in the Coq library.
+
+     Note that all Coq libraries in Nixpkgs have a `version` argument for
+     easily using a different version.  So if all you want to do is use a
+     different version, and the derivation for the Coq library already has
+     support for the version you want, you likely only need to update the
+     `version` argument on the library derivation.  This is done with
+     `.override`:
+
+     ```nix
+     coqPackages.QuickChick.override { version = "1.4.0"; }
+     ```
+  */
+  overrideCoqDerivation = f: drv: (drv.override (args: {
+    mkCoqDerivation = drv_: (args.mkCoqDerivation drv_).override f;
+  }));
 })

pkgs/test/coq/default.nix

@@ -0,0 +1,6 @@
+{ lib, callPackage }:
+
+lib.recurseIntoAttrs {
+  overrideCoqDerivation = callPackage ./overrideCoqDerivation { };
+}
+

pkgs/test/coq/overrideCoqDerivation/default.nix

@@ -0,0 +1,40 @@
+{ lib, coq, mkCoqPackages, runCommand }:
+
+let
+
+  # This is just coq, but with dontFilter set to true. We need to set
+  # dontFilter to true here so that _all_ packages are visibile in coqPackages.
+  # There may be some versions of the top-level coq and coqPackages that don't
+  # build QuickChick, which is what we are using for this test below.
+  coqWithAllPackages = coq // { dontFilter = true; };
+
+  coqPackages = mkCoqPackages coqWithAllPackages;
+
+  # This is the main test.  This uses overrideCoqDerivation to
+  # override arguments to mkCoqDerivation.
+  #
+  # Here, we override the defaultVersion and release arguments to
+  # mkCoqDerivation.
+  overriddenQuickChick =
+    coqPackages.lib.overrideCoqDerivation
+      {
+        defaultVersion = "9999";
+        release."9999".sha256 = lib.fakeSha256;
+      }
+      coqPackages.QuickChick;
+in
+
+runCommand
+  "coq-overrideCoqDerivation-test-0.1"
+  { meta.maintainers = with lib.maintainers; [cdepillabout]; }
+  ''
+    # Confirm that the computed version number for the overridden QuickChick does
+    # actually become 9999, as set above.
+    if [ "${overriddenQuickChick.version}" -eq "9999" ]; then
+      echo "overriddenQuickChick version was successfully set to 9999"
+      touch $out
+    else
+      echo "ERROR: overriddenQuickChick version was supposed to be 9999, but was actually: ${overriddenQuickChick.version}"
+      exit 1
+    fi
+  ''

pkgs/test/default.nix

@@ -75,6 +75,8 @@ with pkgs;
 
   dhall = callPackage ./dhall { };
 
+  coq = callPackage ./coq {};
+
   makeWrapper = callPackage ./make-wrapper { };
   makeBinaryWrapper = callPackage ./make-binary-wrapper {
     makeBinaryWrapper = pkgs.makeBinaryWrapper.override {

pkgs/top-level/coq-packages.nix

@@ -11,7 +11,7 @@ let
 
       metaFetch = import ../build-support/coq/meta-fetch/default.nix
         {inherit lib stdenv fetchzip; };
-      mkCoqDerivation = callPackage ../build-support/coq {};
+      mkCoqDerivation = lib.makeOverridable (callPackage ../build-support/coq {});
 
       contribs = recurseIntoAttrs
         (callPackage ../development/coq-modules/contribs {});