coqPackages: etc

- put `findlib` in `buildInputs` of `mkCoqDerivation` to make sure `coq` packages find their ocaml plugin dependencies,
- use `propagatedBuildInputs` to make sure ocaml plugin dependencies are in path,
- updated `coqPackage.heq` (broken url),
- fixed use of `DESTDIR` and `COQMF_COQLIB` in mkCoqDerivation,
- adding `COQCORELIB` environement variable to put ocaml plugin files in the right place,
- make `metaFetch` available from `coqPackages`

doc/languages-frameworks/coq.section.md

···
 * `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags,
 * `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers,
 * `namePrefix` (optional, defaults to `[ "coq" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
-* `extraNativeBuildInputs` (optional), by default `nativeBuildInputs` just contains `coq`, this allows to add more native build inputs, `nativeBuildInputs` are executables and `buildInputs` are libraries and dependencies,
-* `extraBuildInputs` (optional), this allows to add more build inputs,
-* `mlPlugin` (optional, defaults to `false`). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to `true`. For a finer grain control, the `coq.ocamlPackages` attribute can be used in `extraBuildInputs` to depend on the same package set Coq was built against.
-* `useDune2ifVersion` (optional, default to `(x: false)` uses Dune2 to build the package if the provided predicate evaluates to true on the version, e.g. `useDune2if = versions.isGe "1.1"`  will use dune if the version of the package is greater or equal to `"1.1"`,
+* `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 `useDune2`, `useDune2ifVersion` 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,
+* `buildInputs` (optional), is a list of libraries and dependencies that are required to build and run the current derivation, in addition to the default one `[ coq ]`,
+* `extraBuildInputs` (optional, deprecated), an additional list of derivation to add to `buildInputs`,
+* `overrideBuildInputs` (optional) replaces the default list of derivation to which `buildInputs` and `extraBuildInputs` adds extras elements,
+* `propagatedBuildInputs` (optional) is passed as is to `mkDerivation`, we recommend to use this for Coq libraries and Coq plugin dependencies, as this makes sure the paths of the compiled libraries and plugins will always be added to the build environements of subsequent derivation, which is necessary for Coq packages to work correctly,
+* `mlPlugin` (optional, defaults to `false`). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to `true`. For a finer grain control, the `coq.ocamlPackages` attribute can be used in `nativeBuildInputs`, `buildInputs`, and `propagatedBuildInputs` to depend on the same package set Coq was built against.
+* `useDune2ifVersion` (optional, default to `(x: false)` uses Dune2 to build the package if the provided predicate evaluates to true on the version, e.g. `useDune2ifVersion = versions.isGe "1.1"`  will use dune if the version of the package is greater or equal to `"1.1"`,
 * `useDune2` (optional, defaults to `false`) uses Dune2 to build the package if set to true, the presence of this attribute overrides the behavior of the previous one.
 * `opam-name` (optional, defaults to concatenating with a dash separator the components of `namePrefix` and `pname`), name of the Dune package to build.
 * `enableParallelBuilding` (optional, defaults to `true`), since it is activated by default, we provide a way to disable it.
-* `extraInstallFlags` (optional), allows to extend `installFlags` which initializes the variable `COQMF_COQLIB` so as to install in the proper subdirectory. Indeed Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation.
+* `extraInstallFlags` (optional), allows to extend `installFlags` which initializes the variables `DESTDIR` and `COQMF_COQLIB` so as to install in the proper subdirectory. Indeed Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation.
 * `setCOQBIN` (optional, defaults to `true`), by default, the environment variable `$COQBIN` is set to the current Coq's binary, but one can disable this behavior by setting it to `false`,
 * `useMelquiondRemake` (optional, default to `null`) is an attribute set, which, if given, overloads the `preConfigurePhases`, `configureFlags`, `buildPhase`, and `installPhase` attributes of the derivation for a specific use in libraries using `remake` as set up by Guillaume Melquiond for `flocq`, `gappalib`, `interval`, and `coquelicot` (see the corresponding derivation for concrete examples of use of this option). For backward compatibility, the attribute `useMelquiondRemake.logpath` must be set to the logical root of the library (otherwise, one can pass `useMelquiondRemake = {}` to activate this without backward compatibility).
 * `dropAttrs`, `keepAttrs`, `dropDerivationAttrs` are all optional and allow to tune which attribute is added or removed from the final call to `mkDerivation`.

pkgs/applications/science/logic/coq/default.nix

···
       { case = range "8.7" "8.10";  out = ocamlPackages_4_09; }
       { case = range "8.5" "8.6";   out = ocamlPackages_4_05; }
     ] ocamlPackages_4_12;
-  ocamlNativeBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ]
-    ++ optional (coqAtLeast "8.14") ocamlPackages.dune_2;
-  ocamlBuildInputs = []
+  ocamlNativeBuildInputs = with ocamlPackages; [ ocaml findlib ]
+    ++ optional (coqAtLeast "8.14") dune_2;
+  ocamlPropagatedBuildInputs = [ ]
     ++ optional (!coqAtLeast "8.10") ocamlPackages.camlp5
     ++ optional (!coqAtLeast "8.13") ocamlPackages.num
     ++ optional (coqAtLeast "8.13") ocamlPackages.zarith;
···
 
   passthru = {
     inherit coq-version;
-    inherit ocamlPackages ocamlBuildInputs ocamlNativeBuildInputs;
+    inherit ocamlPackages ocamlNativeNuildInputs;
+    inherit ocamlPropagatedBuildInputs ocamlPropagatedNativeBuildInputs;
     # For compatibility
     inherit (ocamlPackages) ocaml camlp5 findlib num ;
     emacsBufferSetup = pkgs: ''
···
     ++ optional buildIde copyDesktopItems
     ++ optional (buildIde && coqAtLeast "8.10") wrapGAppsHook
     ++ optional (!coqAtLeast "8.6") gnumake42;
-  buildInputs = [ ncurses ] ++ ocamlBuildInputs
+  buildInputs = [ ncurses ]
     ++ optionals buildIde
       (if coqAtLeast "8.10"
        then [ ocamlPackages.lablgtk3-sourceview3 glib gnome.adwaita-icon-theme ]
        else [ ocamlPackages.lablgtk ])
   ;
+
+  propagatedBuildInputs = ocamlPropagatedBuildInputs;
 
   postPatch = ''
     UNAME=$(type -tp uname)

pkgs/applications/science/logic/why3/default.nix

···
     # WebIDE
     js_of_ocaml js_of_ocaml-ppx
     # S-expression output for why3pp
-    ppx_deriving ppx_sexp_conv
+    ppx_deriving ppx_sexp_conv ]
+    ++
     # Coq Support
-    coqPackages.coq coqPackages.flocq
-  ];
+    (with coqPackages; [ coq flocq ])
+  ;
 
   propagatedBuildInputs = with ocamlPackages; [ camlzip menhirLib num re sexplib ];
 

pkgs/build-support/coq/default.nix

···
-{ lib, stdenv, coqPackages, coq, fetchzip }@args:
+{ lib, stdenv, coqPackages, coq, which, fetchzip }@args:
 let lib = import ./extra-lib.nix {inherit (args) lib;}; in
 with builtins; with lib;
 let
···
   releaseRev ? (v: v),
   displayVersion ? {},
   release ? {},
+  buildInputs ? [],
+  nativeBuildInputs ? [],
   extraBuildInputs ? [],
   extraNativeBuildInputs ? [],
+  overrideBuildInputs ? [],
+  overrideNativeBuildInputs ? [],
   namePrefix ? [ "coq" ],
   enableParallelBuilding ? true,
   extraInstallFlags ? [],
···
   args-to-remove = foldl (flip remove) ([
     "version" "fetcher" "repo" "owner" "domain" "releaseRev"
     "displayVersion" "defaultVersion" "useMelquiondRemake"
-    "release" "extraBuildInputs" "extraNativeBuildInputs" "extraPropagatedBuildInputs" "namePrefix"
+    "release"
+    "buildInputs" "nativeBuildInputs"
+    "extraBuildInputs" "extraNativeBuildInputs"
+    "overrideBuildInputs" "overrideNativeBuildInputs"
+    "namePrefix"
     "meta" "useDune2ifVersion" "useDune2" "opam-name"
     "extraInstallFlags" "setCOQBIN" "mlPlugin"
     "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
···
     ] "") + optionalString (v == null) "-broken";
   append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-";
   prefix-name = foldl append-version "" namePrefix;
-  var-coqlib-install =
-    (optionalString (versions.isGe "8.7" coq.coq-version || coq.coq-version == "dev") "COQMF_") + "COQLIB";
   useDune2 = args.useDune2 or (useDune2ifVersion fetched.version);
+  coqlib-flags = switch coq.coq-version [
+    { case = v: versions.isLe "8.6" v && v != "dev" ;
+      out = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; }
+  ] [ "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib"
+      "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" ];
+  docdir-flags = switch coq.coq-version [
+    { case = v: versions.isLe "8.6" v && v != "dev";
+      out = [ "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ]; }
+  ] [ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ];
 in
 
 stdenv.mkDerivation (removeAttrs ({
···
 
   inherit (fetched) version src;
 
-  nativeBuildInputs = [ coq ]
-    ++ optionals useDune2 [coq.ocaml coq.ocamlPackages.dune_2]
-    ++ optionals mlPlugin coq.ocamlNativeBuildInputs
-    ++ extraNativeBuildInputs;
-  buildInputs = optionals mlPlugin coq.ocamlBuildInputs
-    ++ extraBuildInputs;
+  nativeBuildInputs = args.overrideNativeBuildInputs
+    or ([ which coq.ocamlPackages.findlib ]
+        ++ optional useDune2 coq.ocamlPackages.dune_2
+        ++ optional (useDune2 || mlPlugin) coq.ocaml
+        ++ (args.nativeBuildInputs or []) ++ extraNativeBuildInputs);
+  buildInputs = args.overrideBuildInputs
+    or ([ coq ] ++ (args.buildInputs or []) ++ extraBuildInputs);
   inherit enableParallelBuilding;
 
   meta = ({ platforms = coq.meta.platforms; } //
···
 // (optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; })
 // (optionalAttrs (!args?installPhase && !args?useMelquiondRemake) {
   installFlags =
-    [ "${var-coqlib-install}=$(out)/lib/coq/${coq.coq-version}/" ] ++
-    optional (match ".*doc$" (args.installTargets or "") != null)
-      "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ++
+    [ "DESTDIR=$(out)" ] ++ coqlib-flags ++ docdir-flags ++
     extraInstallFlags;
 })
 // (optionalAttrs useDune2 {

pkgs/development/coq-modules/CoLoR/default.nix

···
   release."1.4.0".rev    = "168c6b86c7d3f87ee51791f795a8828b1521589a";
   release."1.4.0".sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm";
 
-  extraBuildInputs = [ bignums ];
+  propagatedBuildInputs = [ bignums ];
   enableParallelBuilding = false;
 
   meta = {

pkgs/development/coq-modules/HoTT/default.nix

···
   release."20170921".rev    = "e3557740a699167e6adb1a65855509d55a392fa1";
   release."20170921".sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v";
 
-  extraBuildInputs = [ autoconf automake ];
+  nativeBuildInputs = [ autoconf automake ];
 
   preConfigure = ''
     patchShebangs ./autogen.sh

pkgs/development/coq-modules/QuickChick/default.nix

···
     "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native";
 
   mlPlugin = true;
-  extraNativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild;
-  extraBuildInputs = lib.optional recent coq.ocamlPackages.num;
+  nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild;
   propagatedBuildInputs = [ ssreflect ]
     ++ lib.optionals recent [ coq-ext-lib simple-io ];
   extraInstallFlags = [ "-f Makefile.coq" ];

pkgs/development/coq-modules/VST/default.nix

···
   release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf";
   release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0=";
   releaseRev = v: "v${v}";
-  extraBuildInputs = [ ITree ];
+  buildInputs = [ ITree ];
   propagatedBuildInputs = [ compcert ];
 
   preConfigure = ''

pkgs/development/coq-modules/bignums/default.nix

···
   owner = "coq";
   displayVersion = { bignums = ""; };
   inherit version;
-  defaultVersion = if versions.isGe "8.5" coq.coq-version
+  defaultVersion = if versions.isGe "8.6" coq.coq-version
     then "${coq.coq-version}.0" else null;
 
   release."8.15.0".sha256 = "093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns";

pkgs/development/coq-modules/compcert/default.nix

···
-{ lib, fetchzip, mkCoqDerivation, coq, flocq, compcert
+{ lib, fetchzip, mkCoqDerivation
+, coq, flocq, compcert
 , ocamlPackages, fetchpatch, makeWrapper, coq2html
 , stdenv, tools ? stdenv.cc
 , version ? null
···
   releaseRev = v: "v${v}";
 
   defaultVersion =  with versions; switch coq.version [
-      { case = range "8.8" "8.11"; out = "3.8"; }
+      { case = range "8.13" "8.15"; out = "3.10"; }
       { case = isEq "8.12"       ; out = "3.9"; }
-      { case = range "8.12" "8.15"; out = "3.10"; }
+      { case = range "8.8" "8.11"; out = "3.8"; }
     ] null;
 
   release = {
···
   '';
 
   installTargets = "documentation install";
+  installFlags = []; # trust ./configure
+  preInstall = ''
+    mkdir -p $out/share/man
+    mkdir -p $man/share
+  '';
   postInstall = ''
     # move man into place
-    mkdir -p $man/share
     mv $out/share/man/ $man/share/
 
     # move docs into place

pkgs/development/coq-modules/coq-bits/default.nix

···
-{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
+{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
 
 with lib; mkCoqDerivation {
   pname = "coq-bits";
   repo = "bits";
   inherit version;
-  defaultVersion =
-    if versions.isGe "8.10" coq.version
-    then "1.1.0"
-    else if versions.isGe "8.7" coq.version
-    then "1.0.0"
-    else null;
-
-  release = {
-    "1.0.0" = {
-      rev = "1.0.0";
-      sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";
-    };
-    "1.1.0" = {
-      rev = "1.1.0";
-      sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE=";
-    };
-  };
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.10"; out = "1.1.0"; }
+    { case = isGe "8.7";  out = "1.0.0"; }
+  ] null;
 
-  extraBuildInputs = [ mathcomp.ssreflect mathcomp.fingroup ];
-  propagatedBuildInputs = [ mathcomp.algebra ];
+  release."1.1.0".sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE=";
+  release."1.0.0".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";
 
-  installPhase = ''
-    make -f Makefile CoqMakefile
-    make -f CoqMakefile COQLIB=$out/lib/coq/${coq.coq-version}/ install
-  '';
+  propagatedBuildInputs = [ mathcomp-algebra ];
 
   meta = {
     description = "A formalization of bitset operations in Coq";

pkgs/development/coq-modules/coq-elpi/default.nix

···
     { case = "8.13"; out = { version = "1.13.7"; };}
     { case = "8.14"; out = { version = "1.13.7"; };}
     { case = "8.15"; out = { version = "1.14.1"; };}
-  ] {});
+  ] { version = "1.14.1"; } );
 in mkCoqDerivation {
   pname = "elpi";
   repo  = "coq-elpi";
···
   release."1.6.0".sha256      = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
   releaseRev = v: "v${v}";
 
-  extraNativeBuildInputs = [ which elpi ];
   mlPlugin = true;
+  propagatedBuildInputs = [ elpi ];
 
   meta = {
     description = "Coq plugin embedding ELPI.";

pkgs/development/coq-modules/coqeal/default.nix

···
 { coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials,
   mathcomp-real-closed,
-  lib, which, version ? null }:
+  lib, version ? null }:
 
 with lib;
 
···
   release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk";
   release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
 
-  extraBuildInputs = [ which ];
   propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ];
 
   meta = {

pkgs/development/coq-modules/coqhammer/default.nix

···
   release."1.3-coq8.12".sha256   = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8";
   release."1.3-coq8.11".sha256   = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b";
   release."1.3-coq8.10".sha256   = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd";
-  release."1.1.1-coq8.9".sha256  = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9";
-  release."1.1-coq8.8".sha256    = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h";
+  release."1.1.1-coq8.9" = { sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9";
+                             rev    = "f8b4d81a213aa1f25afbe53c7c9ca1b15e3d42bc"; };
+  release."1.1-coq8.8" =   { sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h";
+                             rev    = "c3cb54b4d5f33fab372d33c7189861368a08fa22"; };
 
   release."1.3.1-coq8.13".version  = "1.3.1";
   release."1.3.1-coq8.12".version  = "1.3.1";

pkgs/development/coq-modules/coqprime/default.nix

···
   release."8.7.2".sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k";
   releaseRev = v: "v${v}";
 
-  extraBuildInputs = [ which ];
   propagatedBuildInputs = [ bignums ];
 
   meta = with lib; {

pkgs/development/coq-modules/coqtail-math/default.nix

···
   release."8.14".sha256 = "sha256:1k8f8idjnx0mf4z479vcx55iz42rjxrbplbznv80m2famxakq03c";
   release."20201124".rev    = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e";
   release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ=";
-
-  extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml findlib ];
-
+  mlPlugin = true;
   meta = {
     license = licenses.lgpl3Only;
     maintainers = [ maintainers.siraben ];

pkgs/development/coq-modules/coquelicot/default.nix

···
-{ lib, mkCoqDerivation, which, autoconf,
+{ lib, mkCoqDerivation, autoconf,
   coq, ssreflect, version ? null }:
 
 with lib; mkCoqDerivation {
···
   release."3.0.2".sha256 = "1rqfbbskgz7b1bcpva8wh3v3456sq2364y804f94sc8y5sij23nl";
   releaseRev = v: "coquelicot-${v}";
 
-  extraNativeBuildInputs = [ which autoconf ];
+  nativeBuildInputs = [ autoconf ];
   propagatedBuildInputs = [ ssreflect ];
   useMelquiondRemake.logpath = "Coquelicot";
 

pkgs/development/coq-modules/dpdgraph/default.nix

···
   release."0.6".sha256   = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n";
   releaseRev = v: "v${v}";
 
-  extraNativeBuildInputs = [ autoreconfHook ];
+  nativeBuildInputs = [ autoreconfHook ];
   mlPlugin = true;
-  extraBuildInputs = [ coq.ocamlPackages.ocamlgraph ];
+  buildInputs = [ coq.ocamlPackages.ocamlgraph ];
 
   # dpd_compute.ml uses deprecated Pervasives.compare
   # Versions prior to 0.6.5 do not have the WARN_ERR build flag

pkgs/development/coq-modules/fiat/HEAD.nix

···
   inherit version;
   defaultVersion = if coq.coq-version == "8.5" then "2016-10-24" else null;
   release."2016-10-24".rev    = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a";
-  release."2016-10-24".sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64";
+  release."2016-10-24".sha256 = "16y57vibq3f5i5avgj80f4i3aw46wdwzx36k5d3pf3qk17qrlrdi";
 
   mlPlugin = true;
-  extraBuildInputs = [ python27 ];
+  buildInputs = [ python27 ];
 
   prePatch = "patchShebangs etc/coq-scripts";
 

pkgs/development/coq-modules/flocq/default.nix

···
-{ lib, which, autoconf, automake,
+{ lib, bash, autoconf, automake,
   mkCoqDerivation, coq, version ? null }:
 
 with lib; mkCoqDerivation {
···
   release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj";
   releaseRev = v: "flocq-${v}";
 
-  nativeBuildInputs = [ which autoconf ];
+  nativeBuildInputs = [ bash autoconf ];
   mlPlugin = true;
   useMelquiondRemake.logpath = "Flocq";
 

pkgs/development/coq-modules/gappalib/default.nix

···
   release."1.4.4".sha256 = "114q2hgw64j6kqa9mg3qcp1nlf0ia46z2xadq81fnkxqm856ml7l";
   releaseRev = v: "gappalib-coq-${v}";
 
-  extraNativeBuildInputs = [ which autoconf ];
+  nativeBuildInputs = [ autoconf ];
   mlPlugin = true;
   propagatedBuildInputs = [ flocq ];
   useMelquiondRemake.logpath = "Gappa";

pkgs/development/coq-modules/heq/default.nix

···
 {lib, fetchzip, mkCoqDerivation, coq, version ? null }:
 
+let fetcher = {rev, repo, owner, sha256, domain, ...}:
+  fetchzip {
+    url = "https://${domain}/${owner}/${repo}/download/${repo}-${rev}.zip";
+    inherit sha256;
+   }; in
 with lib; mkCoqDerivation {
   pname = "heq";
   repo = "Heq";
-  owner = "gil";
-  domain = "mpi-sws.org";
+  owner = "gil.hur";
+  domain = "sf.snu.ac.kr";
   inherit version fetcher;
   defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null;
   release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74";
 
   mlPlugin = true;
-  propagatedBuildInputs = [ coq ];
-
-  extraInstallFlags = [ "COQLIB=$out/lib/coq/${coq.coq-version}" ];
   preBuild = "cd src";
 
+  extraInstallFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+
   meta = {
-    homepage = "https://www.mpi-sws.org/~gil/Heq/";
+    homepage = "https://ropas.snu.ac.kr/~gil.hur/Heq/";
     description = "Heq : a Coq library for Heterogeneous Equality";
     maintainers = with maintainers; [ jwiegley ];
   };

pkgs/development/coq-modules/hierarchy-builder/default.nix

···
-{ lib, mkCoqDerivation, which, coq, coq-elpi, version ? null }:
+{ lib, mkCoqDerivation, coq, coq-elpi, version ? null }:
 
 with lib; let hb = mkCoqDerivation {
   pname = "hierarchy-builder";
···
   release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
   releaseRev = v: "v${v}";
 
-  extraNativeBuildInputs = [ which ];
-
   propagatedBuildInputs = [ coq-elpi ];
 
   mlPlugin = true;
 
-  installFlags = [ "DESTDIR=$(out)" "COQMF_COQLIB=lib/coq/${coq.coq-version}" ];
   extraInstallFlags = [ "VFILES=structures.v" ];
 
   meta = {

pkgs/development/coq-modules/interval/default.nix

···
-{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, mathcomp-ssreflect, mathcomp-fingroup, bignums ? null, gnuplot_qt, version ? null }:
+{ lib, mkCoqDerivation, autoconf, coq, coquelicot, flocq,
+  mathcomp-ssreflect, mathcomp-fingroup, bignums ? null, gnuplot_qt, version ? null }:
 
 mkCoqDerivation rec {
   pname = "interval";
···
   release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz";
   releaseRev = v: "interval-${v}";
 
-  extraNativeBuildInputs = [ which autoconf ];
-  propagatedBuildInputs = [ bignums coquelicot flocq mathcomp-ssreflect mathcomp-fingroup ]
+  nativeBuildInputs = [ autoconf ];
+  propagatedBuildInputs = lib.optional (lib.versions.isGe "8.6" coq.coq-version) bignums
+    ++ [ coquelicot flocq mathcomp-ssreflect mathcomp-fingroup ]
     ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
   useMelquiondRemake.logpath = "Interval";
   mlPlugin = true;

pkgs/development/coq-modules/itauto/default.nix

···
   ] null;
 
   mlPlugin = true;
-  extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
+  nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
   enableParallelBuilding = false;
 
   meta = {

pkgs/development/coq-modules/ltac2/default.nix

···
   release."0.1-8.7".rev     = "v0.1-8.7";
   release."0.1-8.7".sha256  = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0";
 
-  nativeBuildInputs = [ which ];
   mlPlugin = true;
 
   meta = {

pkgs/development/coq-modules/math-classes/default.nix

···
   release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby";
   release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw";
 
-  extraBuildInputs = [ bignums ];
+  propagatedBuildInputs = [ bignums ];
 
   meta = {
     homepage = "https://math-classes.github.io";

pkgs/development/coq-modules/mathcomp/default.nix

···
 # See the documentation at doc/languages-frameworks/coq.section.md.        #
 ############################################################################
 
-{ lib, ncurses, which, graphviz, lua, fetchzip,
+{ lib, ncurses, graphviz, lua, fetchzip,
   mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false,
-  coqPackages, coq, ocamlPackages, version ? null }@args:
+  coqPackages, coq, version ? null }@args:
 with builtins // lib;
 let
   repo  = "math-comp";
···
         inherit version pname defaultVersion release releaseRev repo owner;
 
         mlPlugin = versions.isLe "8.6" coq.coq-version;
-        extraNativeBuildInputs = [ which ] ++ optionals withDoc [ graphviz lua ];
-        extraBuildInputs = [ ncurses ] ++ mathcomp-deps;
+        nativeBuildInputs = optionals withDoc [ graphviz lua ];
+        buildInputs = [ ncurses ];
+        propagatedBuildInputs = mathcomp-deps;
 
         buildFlags = optional withDoc "doc";
 

pkgs/development/coq-modules/metacoq/default.nix

···
-{ lib, which, fetchzip,
+{ lib, fetchzip,
   mkCoqDerivation, recurseIntoAttrs,  single ? false,
   coqPackages, coq, equations, version ? null }@args:
 with builtins // lib;
···
       derivation = mkCoqDerivation ({
         inherit version pname defaultVersion release releaseRev repo owner;
 
-        extraNativeBuildInputs = [ which ];
         mlPlugin = true;
-        extraBuildInputs = [ coq.ocamlPackages.zarith ];
-        propagatedBuildInputs = [ equations ] ++ metacoq-deps;
+        propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
 
         patchPhase =  ''
           patchShebangs ./configure.sh

pkgs/development/coq-modules/metalib/default.nix

···
   release."8.10".sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs";
 
   sourceRoot = "source/Metalib";
-  installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}";
 
   meta = {
     license = licenses.mit;

pkgs/development/coq-modules/semantics/default.nix

···
   ] null;
 
   mlPlugin = true;
-  extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
-  extraBuildInputs = (with coq.ocamlPackages; [ num ]);
+  nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
+  propagatedBuildInputs = (with coq.ocamlPackages; [ num ]);
 
   postPatch = ''
     for p in Make Makefile.coq.local

pkgs/development/coq-modules/simple-io/default.nix

···
   ] null;
   release."1.7.0".sha256 = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci";
   release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax";
-  extraNativeBuildInputs = (with coq.ocamlPackages; [ cppo zarith ]);
-  propagatedBuildInputs = [ coq-ext-lib ]
-  ++ (with coq.ocamlPackages; [ ocaml ocamlbuild ]);
-
   mlPlugin = true;
+  nativeBuildInputs = [ coq.ocamlPackages.cppo ];
+  propagatedBuildInputs = [ coq-ext-lib coq.ocamlPackages.ocamlbuild ];
 
   doCheck = true;
   checkTarget = "test";

pkgs/development/coq-modules/smtcoq/default.nix

···
     { case = isEq "8.13"; out = "itp22"; }
   ] null;
 
-  propagatedBuildInputs = [ trakt cvc4 ] ++ lib.optionals (!stdenv.isDarwin) [ veriT ];
-  extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml ocamlbuild ];
-  extraBuildInputs = with coq.ocamlPackages; [ findlib num zarith ];
+  propagatedBuildInputs = [ trakt cvc4 ]
+    ++ lib.optionals (!stdenv.isDarwin) [ veriT ]
+    ++ (with coq.ocamlPackages; [ num zarith ]);
+  mlPlugin = true;
+  nativeBuildInputs = with coq.ocamlPackages; [ ocamlbuild ];
 
   meta = {
     description = "Communication between Coq and SAT/SMT solvers ";

pkgs/development/ocaml-modules/elpi/default.nix

···
-{ stdenv, lib, fetchzip, buildDunePackage, camlp5
+{ lib
+, buildDunePackage, camlp5
 , re, perl, ncurses
 , ppxlib, ppx_deriving
 , ppxlib_0_15, ppx_deriving_0_15
+, coqPackages
 , version ? "1.14.1"
 }:
 with lib;
-let fetched = import ../../../build-support/coq/meta-fetch/default.nix
-  {inherit lib stdenv fetchzip; } ({
+let fetched = coqPackages.metaFetch ({
     release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis=";
     release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r";
     release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka";
···
   buildInputs = [ perl ncurses ];
 
   propagatedBuildInputs = [ camlp5 re ]
-  ++ (if lib.versionAtLeast version "1.13"
+  ++ (if lib.versionAtLeast version "1.13" || version == "dev"
      then [ ppxlib ppx_deriving ]
      else [ ppxlib_0_15 ppx_deriving_0_15 ]
   );

pkgs/top-level/coq-packages.nix

···
-{ lib, stdenv, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
+{ lib, stdenv, fetchzip
+, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
 , ocamlPackages_4_10, ocamlPackages_4_12, fetchpatch, makeWrapper, coq2html
 }@args:
 let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in
···
       inherit coq lib;
       coqPackages = self;
 
+      metaFetch = import ../build-support/coq/meta-fetch/default.nix
+        {inherit lib stdenv fetchzip; };
       mkCoqDerivation = callPackage ../build-support/coq {};
 
       contribs = recurseIntoAttrs