Merge branch 'master' into staging-next

Manually resolved a conflict in
pkgs/development/libraries/libbladeRF/default.nix.

doc/languages-frameworks/coq.section.md

···
-# Coq {#sec-language-coq}
+# Coq and coq packages {#sec-language-coq}
 
-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.
+## Coq derivation: `coq`
 
-Some extensions (plugins) might require OCaml and sometimes other OCaml packages. The `coq.ocamlPackages` attribute can be used to depend on the same package set Coq was built against.
+The Coq derivation is overridable through the `coq.override overrides`, where overrides is an attribute set which contains the arguments to override. We recommend overriding either of the following
++ `version` (optional, defaults to the latest version of Coq selected for nixpkgs, see `pkgs/top-level/coq-packages` to witness this choice), which follows the conventions explained in the `coqPackages` section below,
++ `customOCamlPackage` (optional, defaults to `null`, which lets Coq choose a version automatically), which can be set to any of the ocaml packages attribute of `ocaml-ng` (such as `ocaml-ng.ocamlPackages_4_10` which is the default for Coq 8.11 for example).
++ `coq-version` (optional, defaults to the short version e.g. "8.10"), is a version number of the form "x.y" that indicates which Coq's version build behavior to mimic when using a source which is not a release. E.g. `coq.override { version = "d370a9d1328a4e1cdb9d02ee032f605a9d94ec7a"; coq-version = "8.10"; }`.
+
+## Coq packages attribute sets: `coqPackages`
+
+The recommended way of defining a derivation for a Coq library, is to use the `coqPackages.mkCoqDerivation` function, which is essentially a specialization of `mkDerivation` taking into account most of the specifics of Coq libraries. The following attributes are supported:
+- `pname` (required) is the name of the package,
+- `version` (optional, defaults to `null`), is the version to fetch and build,
+  this attribute is interpreted in several ways depending on its type and pattern:
+  + if it is a known released version string, i.e. from the `release` attribute below, the according release is picked, and the `version` attribute of the resulting derivation is set to this release string,
+  + if it is a majorMinor `"x.y"` prefix of a known released version (as defined above), then the latest `"x.y.z"` known released version is selected (for the ordering given by `versionAtLeast`),
+  + if it is a path or a string representing an absolute path (i.e. starting with `"/"`), the provided path is selected as a source, and the `version` attribute of the resulting derivation is set to `"dev"`,
+  + if it is a string of the form `owner:branch` then it tries to download the `branch` of owner `owner` for a project of the same name using the same vcs, and the `version` attribute of the resulting derivation is set to `"dev"`, additionally if the owner is not provided (i.e. if the `owner:` prefix is missing), it defaults to the original owner of the package (see below),
+  + if it is a string of the form `"#N"`, and the domain is github, then it tries to download the current head of the pull request `#N` from github,
+- `defaultVersion` (optional). Coq libraries may be compatible with some specific versions of Coq only. The `defaultVersion` attribute is used when no `version` is provided (or if `version = null`) to select the version of the library to use by default, depending on the context. This selection will mainly depend on a `coq` version number but also possibly on other packages versions (e.g. `mathcomp`). If its value ends up to be `null`, the package is marked for removal in end-user `coqPackages` attribute set.
+- `release` (optional, defaults to `{}`), lists all the known releases of the library and for each of them provides an attribute set with at least a `sha256` attribute (you may use the shell command `nix-prefetch-url --unpack <archive-url>` to find it, where `<archive-url>` is for example `https://github.com/owner/repo/archive/version.tar.gz`), each attribute set of the list of releases also takes optional overloading arguments for the fetcher as below (i.e.`domain`, `owner`, `repo`, `rev` assuming the default fetcher is used) and optional overrides for the result of the fetcher (i.e. `version` and `src`).
+- `fetcher` (optional, default to a generic fetching mechanism supporting github or gitlab based infrastructures), is a function that takes at least an `owner`, a `repo`, a `rev`, and a `sha256` and returns an attribute set with a `version` and `src`.
+- `repo` (optional, defaults to the value of `pname`),
+- `owner` (optional, defaults to `"coq-community"`).
+- `domain` (optional, defaults to `"github.com"`), domains including the strings `"github"` or `"gitlab"` in their names are automatically supported, otherwise, one must change the `fetcher` argument to support them (cf `pkgs/development/coq-modules/heq/default.nix` for an example),
+- `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), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
+- `extraBuildInputs` (optional), by default `buildInputs` just contains `coq`, 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.
+- `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.
+- `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`.
 
-Coq libraries may be compatible with some specific versions of Coq only. The `compatibleCoqVersions` attribute is used to precisely select those versions of Coq that are compatible with this derivation.
+It also takes other standard `mkDerivation` attributes, they are added as such, except for `meta` which extends an automatically computed `meta` (where the `platform` is the same as `coq` and the homepage is automatically computed).
 
-Here is a simple package example. It is a pure Coq library, thus it depends on Coq. It builds on the Mathematical Components library, thus it also takes `mathcomp` as `buildInputs`. Its `Makefile` has been generated using `coq_makefile` so we only have to set the `$COQLIB` variable at install time.
+Here is a simple package example. It is a pure Coq library, thus it depends on Coq. It builds on the Mathematical Components library, thus it also takes some `mathcomp` derivations as `extraBuildInputs`.
 
 ```nix
-{ stdenv, fetchFromGitHub, coq, mathcomp }:
-
-stdenv.mkDerivation rec {
-  name = "coq${coq.coq-version}-multinomials-${version}";
-  version = "1.0";
-  src = fetchFromGitHub {
-    owner = "math-comp";
-    repo = "multinomials";
-    rev = version;
-    sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
+{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough,
+  lib, version ? null }:
+with lib; mkCoqDerivation {
+  /* namePrefix leads to e.g. `name = coq8.11-mathcomp1.11-multinomials-1.5.2` */
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "multinomials";
+  owner = "math-comp";
+  inherit version;
+  defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
+      { cases = [ (range "8.7" "8.12")  "1.11.0" ];             out = "1.5.2"; }
+      { cases = [ (range "8.7" "8.11")  (range "1.8" "1.10") ]; out = "1.5.0"; }
+      { cases = [ (range "8.7" "8.10")  (range "1.8" "1.10") ]; out = "1.4"; }
+      { cases = [ "8.6"                 (range "1.6" "1.7") ];  out = "1.1"; }
+    ] null;
+  release = {
+    "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s";
+    "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3";
+    "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw";
+    "1.5.0".rev    = "1.5";
+    "1.4".sha256   = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p";
+    "1.3".sha256   = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4";
+    "1.2".sha256   = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
+    "1.1".sha256   = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
+    "1.0".sha256   = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
   };
 
-  buildInputs = [ coq ];
-  propagatedBuildInputs = [ mathcomp ];
-
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+  propagatedBuildInputs =
+    [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ];
 
   meta = {
     description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
-    inherit (src.meta) homepage;
-    license = stdenv.lib.licenses.cecill-b;
-    inherit (coq.meta) platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
+    license = licenses.cecill-c;
   };
 }
 ```

nixos/modules/virtualisation/podman.nix

···
 { config, lib, pkgs, utils, ... }:
 let
   cfg = config.virtualisation.podman;
+  toml = pkgs.formats.toml { };
+  nvidia-docker = pkgs.nvidia-docker.override { containerRuntimePath = "${pkgs.runc}/bin/runc"; };
 
   inherit (lib) mkOption types;
 
···
       '';
     };
 
+    enableNvidia = mkOption {
+      type = types.bool;
+      default = false;
+      description = ''
+        Enable use of NVidia GPUs from within podman containers.
+      '';
+    };
+
     extraPackages = mkOption {
       type = with types; listOf package;
       default = [ ];
···
 
   };
 
-  config = lib.mkIf cfg.enable {
+  config = lib.mkIf cfg.enable (lib.mkMerge [
+    {
+      environment.systemPackages = [ cfg.package ]
+        ++ lib.optional cfg.dockerCompat dockerCompat;
 
-    environment.systemPackages = [ cfg.package ]
-      ++ lib.optional cfg.dockerCompat dockerCompat;
-
-    environment.etc."cni/net.d/87-podman-bridge.conflist".source = utils.copyFile "${pkgs.podman-unwrapped.src}/cni/87-podman-bridge.conflist";
-
-    # Enable common /etc/containers configuration
-    virtualisation.containers.enable = true;
-
-    assertions = [{
-      assertion = cfg.dockerCompat -> !config.virtualisation.docker.enable;
-      message = "Option dockerCompat conflicts with docker";
-    }];
+      environment.etc."cni/net.d/87-podman-bridge.conflist".source = utils.copyFile "${pkgs.podman-unwrapped.src}/cni/87-podman-bridge.conflist";
 
-  };
+      virtualisation.containers = {
+        enable = true; # Enable common /etc/containers configuration
+        containersConf.extraConfig = lib.optionalString cfg.enableNvidia
+          (builtins.readFile (toml.generate "podman.nvidia.containers.conf" {
+            engine = {
+              conmon_env_vars = [ "PATH=${lib.makeBinPath [ nvidia-docker ]}" ];
+              runtimes.nvidia = [ "${nvidia-docker}/bin/nvidia-container-runtime" ];
+            };
+          }));
+      };
 
+      assertions = [
+        {
+          assertion = cfg.dockerCompat -> !config.virtualisation.docker.enable;
+          message = "Option dockerCompat conflicts with docker";
+        }
+        {
+          assertion = cfg.enableNvidia -> !config.virtualisation.docker.enableNvidia;
+          message = "Option enableNvidia conflicts with docker.enableNvidia";
+        }
+      ];
+    }
+    (lib.mkIf cfg.enableNvidia {
+      environment.etc."nvidia-container-runtime/config.toml".source = "${nvidia-docker}/etc/podman-config.toml";
+    })
+  ]);
 }

pkgs/applications/graphics/hello-wayland/default.nix

···
+{ stdenv, lib, fetchFromGitHub
+, imagemagick, pkg-config, wayland, wayland-protocols
+}:
+
+stdenv.mkDerivation {
+  pname = "hello-wayland-unstable";
+  version = "2020-07-27";
+
+  src = fetchFromGitHub {
+    owner = "emersion";
+    repo = "hello-wayland";
+    rev = "501d0851cfa7f21c780c0eb52f0a6b23f02918c5";
+    sha256 = "0dz6przqp57kw8ycja3gw6jp9x12217nwbwdpgmvw7jf0lzhk4xr";
+  };
+
+  nativeBuildInputs = [ imagemagick pkg-config ];
+  buildInputs = [ wayland wayland-protocols ];
+
+  installPhase = ''
+    runHook preBuild
+    mkdir -p $out/bin
+    install hello-wayland $out/bin
+    runHook postBuild
+  '';
+
+  meta = with lib; {
+    description = "Hello world Wayland client";
+    homepage = "https://github.com/emersion/hello-wayland";
+    maintainers = with maintainers; [ qyliss ];
+    license = licenses.mit;
+    platforms = platforms.linux;
+  };
+}

pkgs/applications/networking/cluster/octant/plugins/starboard-octant-plugin.nix

···
 
 buildGoModule rec {
   pname = "starboard-octant-plugin";
-  version = "0.7.1";
+  version = "0.8.0";
 
   src = fetchFromGitHub {
     owner = "aquasecurity";
     repo = pname;
     rev = "v${version}";
-    sha256 = "11c8znbijhvxl2mas205mb18sqw868l6c86ah5hlkqh3niq2gmv3";
+    sha256 = "sha256-wMt/I2zpdM7l+YNwHkAA6sVRWUtlGpN+94jqx2Jy4HA=";
   };
 
-  vendorSha256 = "0rmynfm5afjxc2lxy2rh9y6zhdd2q95wji2q8hcz78zank43rkcq";
+  vendorSha256 = "sha256-fhIIqirEEdqn/n8bBtLw07fEGfnpC/8SOLbkhnytyME=";
 
   meta = with lib; {
     description = "Octant plugin for viewing Starboard security information";

pkgs/applications/networking/cluster/terragrunt/default.nix

···
 
 buildGoModule rec {
   pname = "terragrunt";
-  version = "0.26.7";
+  version = "0.27.0";
 
   src = fetchFromGitHub {
     owner = "gruntwork-io";
     repo = pname;
     rev = "v${version}";
-    sha256 = "1431n6zs2mfkgh281xi0d7m9hxifrrsnd46fnpb54mr6lj9h0sdb";
+    sha256 = "sha256-MbhJ1f6Da+kkkCV85kH8Yv74cMzp7JvxeQb0By9aGp8=";
   };
 
-  vendorSha256 = "18ix11g709fvh8h02k3p2bmzrq5fjzaqa50h3g74s3hyl2gc9s9h";
+  vendorSha256 = "sha256-AMxBzUHRsq1HOMtvgYqIw22Cky7gQ7/2hI8wQnxaXb0=";
 
   doCheck = false;
 

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

···
 # - The exact version can be specified through the `version` argument to
 #   the derivation; it defaults to the latest stable version.
 
-{ stdenv, fetchFromGitHub, writeText, pkgconfig, gnumake42
-, ocamlPackages, ncurses
+{ stdenv, fetchzip, writeText, pkgconfig, gnumake42
+, customOCamlPackages ? null
+, ocamlPackages_4_05, ocamlPackages_4_09, ocamlPackages_4_10, ncurses
 , buildIde ? !(stdenv.isDarwin && stdenv.lib.versionAtLeast version "8.10")
 , glib, gnome3, wrapGAppsHook
 , csdp ? null
-, version
-}:
-
+, version, coq-version ? null,
+}@args:
+let lib = import ../../../../build-support/coq/extra-lib.nix {inherit (stdenv) lib;}; in
+with builtins; with lib;
 let
-  sha256 = {
-   "8.5pl1"    = "1976ki5xjg2r907xj9p7gs0kpdinywbwcqlgxqw75dgp0hkgi00n";
-   "8.5pl2"    = "109rrcrx7mz0fj7725kjjghfg5ydwb24hjsa5hspa27b4caah7rh";
-   "8.5pl3"    = "15c3rdk59nifzihsp97z4vjxis5xmsnrvpb86qiazj143z2fmdgw";
-   "8.6"       = "148mb48zpdax56c0blfi7v67lx014lnmrvxxasi28hsibyz2lvg4";
-   "8.6.1"     = "0llrxcxwy5j87vbbjnisw42rfw1n1pm5602ssx64xaxx3k176g6l";
-   "8.7.0"     = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m";
-   "8.7.1"     = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8";
-   "8.7.2"     = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w";
-   "8.8.0" = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8";
-   "8.8.1" = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk";
-   "8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd";
-   "8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh";
-   "8.9.1" = "1xrq6mkhpq994bncmnijf8jwmwn961kkpl4mwwlv7j3dgnysrcv2";
-   "8.10.0" = "138jw94wp4mg5dgjc2asn8ng09ayz1mxdznq342n0m469j803gzg";
-   "8.10.1" = "072v2zkjzf7gj48137wpr3c9j0hg9pdhlr5l8jrgrwynld8fp7i4";
-   "8.10.2" = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz";
-   "8.11.0" = "1rfdic6mp7acx2zfwz7ziqk12g95bl9nyj68z4n20a5bcjv2pxpn";
-   "8.11.1" = "0qriy9dy36dajsv5qmli8gd6v55mah02ya334nw49ky19v7518m0";
-   "8.11.2" = "0f77ccyxdgbf1nrj5fa8qvrk1cyfy06fv8gj9kzfvlcgn0cf48sa";
-   "8.12.0" = "18dc7k0piv6v064zgdadpw6mkkxk7j663hb3svgj5236fihjr0cz";
-   "8.12.1" = "1rkcyjjrzcqw9xk93hsq0vvji4f8r5iq0f739mghk60bghkpnb7q";
-   "8.12.2" = "18gscfm039pqhq4msq01nraig5dm9ab98bjca94zldf8jvdv0x2n";
-   "8.13+beta1" = "1v4a6dpj41flspa4ihcr7m5ahqz10kbn62fmrldmv7gzq6jsyfyq";
-  }.${version};
-  coq-version = stdenv.lib.versions.majorMinor version;
-  versionAtLeast = stdenv.lib.versionAtLeast coq-version;
-  ideFlags = stdenv.lib.optionalString (buildIde && !versionAtLeast "8.10")
+  release = {
+   "8.5pl1".sha256     = "1976ki5xjg2r907xj9p7gs0kpdinywbwcqlgxqw75dgp0hkgi00n";
+   "8.5pl2".sha256     = "109rrcrx7mz0fj7725kjjghfg5ydwb24hjsa5hspa27b4caah7rh";
+   "8.5pl3".sha256     = "15c3rdk59nifzihsp97z4vjxis5xmsnrvpb86qiazj143z2fmdgw";
+   "8.6.0".sha256      = "148mb48zpdax56c0blfi7v67lx014lnmrvxxasi28hsibyz2lvg4";
+   "8.6.0".rev         = "V8.6";
+   "8.6.1".sha256      = "0llrxcxwy5j87vbbjnisw42rfw1n1pm5602ssx64xaxx3k176g6l";
+   "8.7.0".sha256      = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m";
+   "8.7.1".sha256      = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8";
+   "8.7.2".sha256      = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w";
+   "8.8.0".sha256      = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8";
+   "8.8.1".sha256      = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk";
+   "8.8.2".sha256      = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd";
+   "8.9.0".sha256      = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh";
+   "8.9.1".sha256      = "1xrq6mkhpq994bncmnijf8jwmwn961kkpl4mwwlv7j3dgnysrcv2";
+   "8.10.0".sha256     = "138jw94wp4mg5dgjc2asn8ng09ayz1mxdznq342n0m469j803gzg";
+   "8.10.1".sha256     = "072v2zkjzf7gj48137wpr3c9j0hg9pdhlr5l8jrgrwynld8fp7i4";
+   "8.10.2".sha256     = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz";
+   "8.11.0".sha256     = "1rfdic6mp7acx2zfwz7ziqk12g95bl9nyj68z4n20a5bcjv2pxpn";
+   "8.11.1".sha256     = "0qriy9dy36dajsv5qmli8gd6v55mah02ya334nw49ky19v7518m0";
+   "8.11.2".sha256     = "0f77ccyxdgbf1nrj5fa8qvrk1cyfy06fv8gj9kzfvlcgn0cf48sa";
+   "8.12.0".sha256     = "18dc7k0piv6v064zgdadpw6mkkxk7j663hb3svgj5236fihjr0cz";
+   "8.12.1".sha256     = "1rkcyjjrzcqw9xk93hsq0vvji4f8r5iq0f739mghk60bghkpnb7q";
+   "8.12.2".sha256     = "18gscfm039pqhq4msq01nraig5dm9ab98bjca94zldf8jvdv0x2n";
+   "8.13+beta1".sha256 = "1v4a6dpj41flspa4ihcr7m5ahqz10kbn62fmrldmv7gzq6jsyfyq";
+  };
+  releaseRev = v: "V${v}";
+  fetched = import ../../../../build-support/coq/meta-fetch/default.nix
+    { inherit stdenv fetchzip; }
+    { inherit release releaseRev; location = { owner = "coq"; repo = "coq";}; }
+    args.version;
+  version = fetched.version;
+  coq-version = args.coq-version or (if version != "dev" then versions.majorMinor version else "dev");
+  versionAtLeast = v: (coq-version == "dev") || (stdenv.lib.versionAtLeast coq-version v);
+  ideFlags = optionalString (buildIde && !versionAtLeast "8.10")
     "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt";
   csdpPatch = if csdp != null then ''
     substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
     substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
   '' else "";
+  ocamlPackages = if !isNull customOCamlPackages then customOCamlPackages
+    else with versions; switch coq-version [
+      { case = range "8.11" "8.13"; out = ocamlPackages_4_10; }
+      { case = range "8.7" "8.10";  out = ocamlPackages_4_09; }
+      { case = range "8.5" "8.6";   out = ocamlPackages_4_05; }
+    ] ocamlPackages_4_10;
+  ocamlBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ]
+    ++ optional (!versionAtLeast "8.10") ocamlPackages.camlp5
+    ++ optional (!versionAtLeast "8.13") ocamlPackages.num
+    ++ optional (versionAtLeast "8.13") ocamlPackages.zarith;
 self = stdenv.mkDerivation {
   pname = "coq";
-  inherit version;
+  inherit (fetched) version src;
 
   passthru = {
     inherit coq-version;
-    inherit ocamlPackages;
+    inherit ocamlPackages ocamlBuildInputs;
     # For compatibility
-    inherit (ocamlPackages) ocaml camlp5 findlib num;
+    inherit (ocamlPackages) ocaml camlp5 findlib num ;
     emacsBufferSetup = pkgs: ''
       ; Propagate coq paths to children
       (inherit-local-permanent coq-prog-name "${self}/bin/coqtop")
···
         (coq-prog-args))
       (mapc (lambda (arg)
         (when (file-directory-p (concat arg "/lib/coq/${coq-version}/user-contrib"))
-          (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${stdenv.lib.concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)}))
+          (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)}))
       ; TODO Abstract this pattern from here and nixBufferBuilders.withPackages!
       (defvar nixpkgs--coq-buffer-count 0)
       (when (eq nixpkgs--coq-buffer-count 0)
···
     '';
   };
 
-  src = fetchFromGitHub {
-    owner = "coq";
-    repo = "coq";
-    rev = "V${version}";
-    inherit sha256;
-  };
-
-  nativeBuildInputs = [ pkgconfig ]
-  ++ stdenv.lib.optional (!versionAtLeast "8.6") gnumake42
-  ;
-  buildInputs = [ ncurses ocamlPackages.ocaml ocamlPackages.findlib ]
-  ++ stdenv.lib.optional (!versionAtLeast "8.10") ocamlPackages.camlp5
-  ++ stdenv.lib.optional (!versionAtLeast "8.12") ocamlPackages.num
-  ++ stdenv.lib.optionals buildIde
-    (if versionAtLeast "8.10"
-     then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ]
-     else [ ocamlPackages.lablgtk ]);
-
-  propagatedBuildInputs =
-     stdenv.lib.optional (versionAtLeast "8.13") ocamlPackages.zarith
-  ++ stdenv.lib.optional (coq-version == "8.12") ocamlPackages.num;
+  nativeBuildInputs = [ pkgconfig ] ++ optional (!versionAtLeast "8.6") gnumake42;
+  buildInputs = [ ncurses ] ++ ocamlBuildInputs
+    ++ optionals buildIde
+      (if versionAtLeast "8.10"
+       then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ]
+       else [ ocamlPackages.lablgtk ]);
 
   postPatch = ''
     UNAME=$(type -tp uname)

pkgs/applications/virtualization/nvidia-docker/default.nix

···
 , makeWrapper
 , buildGoModule
 , buildGoPackage
-, git
 , glibc
+, docker
+, linkFarm
+, containerRuntimePath ? "${docker}/libexec/docker/runc"
 }:
 
 with lib; let
   libnvidia-container = callPackage ./libnvc.nix { };
+  isolatedContainerRuntimePath = linkFarm "isolated_container_runtime_path" [
+    {
+      name = "runc";
+      path = containerRuntimePath;
+    }
+  ];
 
   nvidia-container-runtime = buildGoPackage rec {
-    pname = "nvidia-container-toolkit";
+    pname = "nvidia-container-runtime";
     version = "3.4.0";
     src = fetchFromGitHub {
       owner = "NVIDIA";
···
   installPhase = ''
     mkdir -p $out/{bin,etc}
     cp -r bin $out
+
     wrapProgram $out/bin/nvidia-container-cli \
       --prefix LD_LIBRARY_PATH : /run/opengl-driver/lib:/run/opengl-driver-32/lib
+
+    # nvidia-container-runtime invokes docker-runc or runc if that isn't available on PATH
+    wrapProgram $out/bin/nvidia-container-runtime --prefix PATH : ${isolatedContainerRuntimePath}
+
     cp ${./config.toml} $out/etc/config.toml
     substituteInPlace $out/etc/config.toml --subst-var-by glibcbin ${lib.getBin glibc}
+
+    cp ${./podman-config.toml} $out/etc/podman-config.toml
+    substituteInPlace $out/etc/podman-config.toml --subst-var-by glibcbin ${lib.getBin glibc}
   '';
 
   meta = {

pkgs/applications/virtualization/nvidia-docker/podman-config.toml

···
+disable-require = true
+#swarm-resource = "DOCKER_RESOURCE_GPU"
+
+[nvidia-container-cli]
+#root = "/run/nvidia/driver"
+#path = "/usr/bin/nvidia-container-cli"
+environment = []
+#debug = "/var/log/nvidia-container-runtime-hook.log"
+ldcache = "/tmp/ld.so.cache"
+load-kmods = true
+no-cgroups = true
+#user = "root:video"
+ldconfig = "@@glibcbin@/bin/ldconfig"

pkgs/build-support/coq/default.nix

···
+{ lib, stdenv, coqPackages, coq, fetchzip }@args:
+let lib = import ./extra-lib.nix {inherit (args) lib;}; in
+with builtins; with lib;
+let
+  isGitHubDomain = d: match "^github.*" d != null;
+  isGitLabDomain = d: match "^gitlab.*" d != null;
+in
+{ pname,
+  version ? null,
+  fetcher ? null,
+  owner ? "coq-community",
+  domain ? "github.com",
+  repo ? pname,
+  defaultVersion ? null,
+  releaseRev ? (v: v),
+  displayVersion ? {},
+  release ? {},
+  extraBuildInputs ? [],
+  namePrefix ? [],
+  enableParallelBuilding ? true,
+  extraInstallFlags ? [],
+  setCOQBIN ? true,
+  mlPlugin ? false,
+  useMelquiondRemake ? null,
+  dropAttrs ? [],
+  keepAttrs ? [],
+  dropDerivationAttrs ? [],
+  ...
+}@args:
+let
+  args-to-remove = foldl (flip remove) ([
+    "version" "fetcher" "repo" "owner" "domain" "releaseRev"
+    "displayVersion" "defaultVersion" "useMelquiondRemake"
+    "release" "extraBuildInputs" "extraPropagatedBuildInputs" "namePrefix" "meta"
+    "extraInstallFlags" "setCOQBIN" "mlPlugin"
+    "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
+  fetch = import ../coq/meta-fetch/default.nix
+    { inherit stdenv fetchzip; } ({
+      inherit release releaseRev;
+      location = { inherit domain owner repo; };
+    } // optionalAttrs (args?fetcher) {inherit fetcher;});
+  fetched = fetch (if !isNull version then version else defaultVersion);
+  namePrefix = args.namePrefix or [ "coq" ];
+  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;
+  var-coqlib-install = (optionalString (versions.isGe "8.7" coq.coq-version) "COQMF_") + "COQLIB";
+in
+
+stdenv.mkDerivation (removeAttrs ({
+
+  name = prefix-name + (display-pkg pname "-" fetched.version);
+
+  inherit (fetched) version src;
+
+  buildInputs = [ coq ] ++ optionals mlPlugin coq.ocamlBuildInputs ++ extraBuildInputs;
+  inherit enableParallelBuilding;
+
+  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 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}/" ++
+    extraInstallFlags;
+}) //
+(optionalAttrs (args?useMelquiondRemake) rec {
+  COQUSERCONTRIB = "$out/lib/coq/${coq.coq-version}/user-contrib";
+  preConfigurePhases = "autoconf";
+  configureFlags = [ "--libdir=${COQUSERCONTRIB}/${useMelquiondRemake.logpath or ""}" ];
+  buildPhase = "./remake -j$NIX_BUILD_CORES";
+  installPhase = "./remake install";
+}) //
+(removeAttrs args args-to-remove)) dropDerivationAttrs)

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

···
+{ lib }:
+with builtins; with lib; recursiveUpdate lib (rec {
+
+  versions =
+    let
+      truncate = n: v: concatStringsSep "." (take n (splitVersion v));
+      opTruncate = op: v0: v: let n = length (splitVersion v0); in
+         op (truncate n v) (truncate n v0);
+    in rec {
+
+    /* Get string of the first n parts of a version string.
+
+       Example:
+       - truncate 2 "1.2.3-stuff"
+         => "1.2"
+
+       - truncate 4 "1.2.3-stuff"
+         => "1.2.3.stuff"
+    */
+
+    inherit truncate;
+
+    /* Get string of the first three parts (major, minor and patch)
+       of a version string.
+
+       Example:
+         majorMinorPatch "1.2.3-stuff"
+         => "1.2.3"
+    */
+    majorMinorPatch = truncate 3;
+
+    /* Version comparison predicates,
+      - isGe v0 v <-> v is greater or equal than v0   [*]
+      - isLe v0 v <-> v is lesser  or equal than v0   [*]
+      - isGt v0 v <-> v is strictly greater than v0   [*]
+      - isLt v0 v <-> v is strictly lesser  than v0   [*]
+      - isEq v0 v <-> v is equal to v0                [*]
+      - range low high v <-> v is between low and high [**]
+
+    [*]  truncating v to the same number of digits as v0
+    [**] truncating v to low for the lower bound and high for the upper bound
+
+      Examples:
+      - isGe "8.10" "8.10.1"
+        => true
+      - isLe "8.10" "8.10.1"
+        => true
+      - isGt "8.10" "8.10.1"
+        => false
+      - isGt "8.10.0" "8.10.1"
+        => true
+      - isEq "8.10" "8.10.1"
+        => true
+      - range "8.10" "8.11" "8.11.1"
+        => true
+      - range "8.10" "8.11+" "8.11.0"
+        => false
+      - range "8.10" "8.11+" "8.11+beta1"
+        => false
+
+    */
+    isGe = opTruncate versionAtLeast;
+    isGt = opTruncate (flip versionOlder);
+    isLe = opTruncate (flip versionAtLeast);
+    isLt = opTruncate versionOlder;
+    isEq = opTruncate pred.equal;
+    range = low: high: pred.inter (versions.isGe low) (versions.isLe high);
+  };
+
+  /* Returns a list of list, splitting it using a predicate.
+     This is analoguous to builtins.split sep list,
+     with a predicate as a separator and a list instead of a string.
+
+    Type: splitList :: (a -> bool) -> [a] -> [[a]]
+
+    Example:
+      splitList (x: x == "x") [ "y" "x" "z" "t" ]
+      => [ [ "y" ] "x" [ "z" "t" ] ]
+  */
+  splitList = pred: l: # put in file lists
+    let loop = (vv: v: l: if l == [] then vv ++ [v]
+      else let hd = head l; tl = tail l; in
+      if pred hd then loop (vv ++ [ v hd ]) [] tl else loop vv (v ++ [hd]) tl);
+    in loop [] [] l;
+
+  pred = {
+    /* Predicate intersection, union, and complement */
+    inter = p: q: x: p x && q x;
+    union = p: q: x: p x || q x;
+    compl = p:    x: ! p x;
+    true  = p: true;
+    false = p: false;
+
+    /* predicate "being equal to y" */
+    equal = y:    x: x == y;
+  };
+
+  /* Emulate a "switch - case" construct,
+   instead of relying on `if then else if ...` */
+  /* Usage:
+  ```nix
+  switch-if [
+    if-clause-1
+    ..
+    if-clause-k
+  ] default-out
+  ```
+  where a if-clause has the form `{ cond = b; out = r; }`
+  the first branch such as `b` is true */
+
+  switch-if = c: d: (findFirst (getAttr "cond") {} c).out or d;
+
+  /* Usage:
+  ```nix
+  switch x [
+    simple-clause-1
+    ..
+    simple-clause-k
+  ] default-out
+  ```
+  where a simple-clause has the form `{ case = p; out = r; }`
+  the first branch such as `p x` is true
+  or
+  ```nix
+  switch [ x1 .. xn ] [
+    complex-clause-1
+    ..
+    complex-clause-k
+  ] default-out
+  ```
+  where a complex-clause is either a simple-clause
+  or has the form { cases = [ p1 .. pn ]; out = r; }
+  in which case the first branch such as all `pi x` are true
+
+  if the variables p are not functions,
+  they are converted to a equal p
+  if out is missing the default-out is taken */
+
+  switch = var: clauses: default: with pred; let
+      compare = f:  if isFunction f then f else equal f;
+      combine = cl: var:
+        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;
+})

pkgs/build-support/coq/meta-fetch/default.nix

···
+{ stdenv, fetchzip }@args:
+let lib = import ../extra-lib.nix {inherit (args.stdenv) lib;}; in
+with builtins; with lib;
+let
+  default-fetcher = {domain ? "github.com", owner ? "", repo, rev, name ? "source", sha256 ? null, ...}@args:
+    let ext = if args?sha256 then "zip" else "tar.gz";
+        fmt = if args?sha256 then "zip" else "tarball";
+        pr  = match "^#(.*)$" rev;
+        url = switch-if [
+          { cond = isNull pr && !isNull (match "^github.*" domain);
+            out = "https://${domain}/${owner}/${repo}/archive/${rev}.${ext}"; }
+          { cond = !isNull pr && !isNull (match "^github.*" domain);
+            out = "https://api.${domain}/repos/${owner}/${repo}/${fmt}/pull/${head pr}/head"; }
+          { cond = isNull pr && !isNull (match "^gitlab.*" domain);
+            out = "https://${domain}/${owner}/${repo}/-/archive/${rev}/${repo}-${rev}.${ext}"; }
+          { cond = !isNull (match "(www.)?mpi-sws.org" domain);
+            out = "https://www.mpi-sws.org/~${owner}/${repo}/download/${repo}-${rev}.${ext}";}
+        ] (throw "meta-fetch: no fetcher found for domain ${domain} on ${rev}");
+        fetch = x: if args?sha256 then fetchzip (x // { inherit sha256; }) else fetchTarball x;
+    in fetch { inherit url ; };
+in
+{
+  fetcher ? default-fetcher,
+  location,
+  release ? {},
+  releaseRev ? (v: v),
+}:
+let isVersion      = x: isString x && match "^/.*" x == null && release?${x};
+    shortVersion   = x: if (isString x && match "^/.*" x == null)
+      then findFirst (v: versions.majorMinor v == x) null
+        (sort versionAtLeast (attrNames release))
+      else null;
+    isShortVersion = x: shortVersion x != null;
+    isPathString   = x: isString x && match "^/.*" x != null && pathExists x; in
+arg:
+switch arg [
+  { case = isNull;       out = { version = "broken"; src = ""; broken = true; }; }
+  { case = isPathString; out = { version = "dev"; src = arg; }; }
+  { case = pred.union isVersion isShortVersion;
+    out = let v = if isVersion arg then arg else shortVersion arg; in
+      if !release.${v}?sha256 then throw "meta-fetch: a sha256 must be provided for each release"
+      else {
+        version = release.${v}.version or v;
+        src = release.${v}.src or fetcher (location // { rev = releaseRev v; } // release.${v});
+      };
+    }
+  { case = isString;
+    out = let
+        splitted  = filter isString (split ":" arg);
+        rev       = last splitted;
+        has-owner = length splitted > 1;
+        version   = "dev"; in {
+      inherit version;
+      src = fetcher (location // { inherit rev; } //
+        (optionalAttrs has-owner { owner = head splitted; }));
+    }; }
+  { case = isAttrs;
+    out = let
+    { version = arg.version or "dev";
+      src = (arg.fetcher or fetcher) (location // (arg.location or {}));
+    }; }
+  { case = isPath;
+    out = {
+      version = "dev" ;
+      src = builtins.path {path = arg; name = location.name or "source";}; }; }
+] (throw "not a valid source description")

pkgs/build-support/rust/default-crate-overrides.nix

···
-{ stdenv, pkgconfig, curl, darwin, libiconv, libgit2, libssh2,
+{ stdenv, pkg-config, curl, darwin, libiconv, libgit2, libssh2,
   openssl, sqlite, zlib, dbus, dbus-glib, gdk-pixbuf, cairo, python3,
-  libsodium, postgresql, gmp, foundationdb, ... }:
+  libsodium, postgresql, gmp, foundationdb, capnproto, nettle, clang,
+  llvmPackages, ... }:
 
 let
   inherit (darwin.apple_sdk.frameworks) CoreFoundation Security;
···
 {
   cairo-rs = attrs: {
     buildInputs = [ cairo ];
+  };
+
+  capnp-rpc = attrs: {
+    nativeBuildInputs = [ capnproto ];
   };
 
   cargo = attrs: {
···
   };
 
   libz-sys = attrs: {
-    nativeBuildInputs = [ pkgconfig ];
+    nativeBuildInputs = [ pkg-config ];
     buildInputs = [ zlib ];
     extraLinkFlags = ["-L${zlib.out}/lib"];
   };
 
   curl-sys = attrs: {
-    nativeBuildInputs = [ pkgconfig ];
+    nativeBuildInputs = [ pkg-config ];
     buildInputs = [ zlib curl ];
     propagatedBuildInputs = [ curl zlib ];
     extraLinkFlags = ["-L${zlib.out}/lib"];
   };
 
   dbus = attrs: {
-    nativeBuildInputs = [ pkgconfig ];
+    nativeBuildInputs = [ pkg-config ];
     buildInputs = [ dbus ];
   };
 
···
 
   libgit2-sys = attrs: {
     LIBGIT2_SYS_USE_PKG_CONFIG = true;
-    nativeBuildInputs = [ pkgconfig ];
+    nativeBuildInputs = [ pkg-config ];
     buildInputs = [ openssl zlib libgit2 ];
   };
 
   libsqlite3-sys = attrs: {
-    nativeBuildInputs = [ pkgconfig ];
+    nativeBuildInputs = [ pkg-config ];
     buildInputs = [ sqlite ];
   };
 
   libssh2-sys = attrs: {
-    nativeBuildInputs = [ pkgconfig ];
+    nativeBuildInputs = [ pkg-config ];
     buildInputs = [ openssl zlib libssh2 ];
   };
 
   libdbus-sys = attrs: {
-    nativeBuildInputs = [ pkgconfig ];
+    nativeBuildInputs = [ pkg-config ];
     buildInputs = [ dbus ];
   };
 
+  nettle-sys = attrs: {
+    nativeBuildInputs = [ pkg-config ];
+    buildInputs = [ nettle clang ];
+    LIBCLANG_PATH = "${llvmPackages.libclang}/lib";
+  };
+
   openssl = attrs: {
     buildInputs = [ openssl ];
   };
 
   openssl-sys = attrs: {
-    nativeBuildInputs = [ pkgconfig ];
+    nativeBuildInputs = [ pkg-config ];
     buildInputs = [ openssl ];
   };
 
   pq-sys = attr: {
-    nativeBuildInputs = [ pkgconfig ];
+    nativeBuildInputs = [ pkg-config ];
     buildInputs = [ postgresql ];
   };
 
···
     propagatedBuildInputs = [ Security ];
   };
 
+  sequoia-openpgp = attrs: {
+    buildInputs = [ gmp ];
+  };
+
+  sequoia-openpgp-ffi = attrs: {
+    buildInputs = [ gmp ];
+  };
+
+  sequoia-ipc = attrs: {
+    buildInputs = [ gmp ];
+  };
+
+  sequoia-guide = attrs: {
+    buildInputs = [ gmp ];
+  };
+
+  sequoia-store = attrs: {
+    nativeBuildInputs = [ capnproto ];
+    buildInputs = [ sqlite gmp ];
+  };
+
+  sequoia-sq = attrs: {
+    buildInputs = [ sqlite gmp ];
+  };
+
+  sequoia-tool = attrs: {
+    nativeBuildInputs = [ capnproto ];
+    buildInputs = [ sqlite gmp ];
+  };
+
   serde_derive = attrs: {
     buildInputs = stdenv.lib.optional stdenv.isDarwin Security;
   };
 
   thrussh-libsodium = attrs: {
-    nativeBuildInputs = [ pkgconfig ];
+    nativeBuildInputs = [ pkg-config ];
     buildInputs = [ libsodium ];
   };
 

pkgs/development/compilers/rust/1_45.nix

···
   # building
   bootstrapVersion = "1.44.1";
 
-  # fetch hashes by running `print-hashes.sh 1.45.0`
+  # fetch hashes by running `print-hashes.sh ${bootstrapVersion}`
   bootstrapHashes = {
     i686-unknown-linux-gnu = "e69689b0a1b66599cf83e7dd54f839419007e44376195e93e301a3175da3d854";
     x86_64-unknown-linux-gnu = "a41df89a461a580536aeb42755e43037556fba2e527dd13a1e1bb0749de28202";

pkgs/development/compilers/rust/1_48.nix

···
   # building
   bootstrapVersion = "1.47.0";
 
-  # fetch hashes by running `print-hashes.sh 1.45.2`
+  # fetch hashes by running `print-hashes.sh ${bootstrapVersion}`
   bootstrapHashes = {
     i686-unknown-linux-gnu = "84bf092130ea5216fc701871e633563fc1c01b6528f60cb0767e96cd8eec30bf";
     x86_64-unknown-linux-gnu = "d0e11e1756a072e8e246b05d54593402813d047d12e44df281fbabda91035d96";

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

···
-{ stdenv, fetchFromGitHub, coq, StructTact }:
+{ lib, mkCoqDerivation, coq, StructTact, version ? null }:
 
-let param =
-  {
-      version = "20200201";
-      rev = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d";
-      sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1";
-  };
-in
-
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-Cheerios-${param.version}";
-
-  src = fetchFromGitHub {
-    owner = "uwplse";
-    repo = "cheerios";
-    inherit (param) rev sha256;
-  };
-
-  buildInputs = [ coq ];
+with lib; mkCoqDerivation {
+  pname   = "cheerios";
+  owner   = "uwplse";
+  inherit version;
+  defaultVersion = if versions.isGe "8.6" coq.coq-version then "20200201" else null;
+  release."20200201".rev    = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d";
+  release."20200201".sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1";
 
   propagatedBuildInputs = [ StructTact ];
-  enableParallelBuilding = true;
-
   preConfigure = "patchShebangs ./configure";
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
- };
 }

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

···
-{ stdenv, fetchFromGitHub, coq, bignums }:
+{ lib, mkCoqDerivation, coq, bignums, version ? null }:
 
-let
-  coqVersions = {
-    "8.6" = "1.4.0";
-    "8.7" = "1.4.0";
-    "8.8" = "1.6.0";
-    "8.9" = "1.6.0";
-    "8.10" = "1.7.0";
-    "8.11" = "1.7.0";
-  };
-  params = {
-    "1.4.0" = {
-      version = "1.4.0";
-      rev = "168c6b86c7d3f87ee51791f795a8828b1521589a";
-      sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm";
-    };
-    "1.6.0" = {
-      version = "1.6.0";
-      rev = "328aa06270584b578edc0d2925e773cced4f14c8";
-      sha256 = "07sy9kw1qlynsqy251adgi8b3hghrc9xxl2rid6c82mxfsp329sd";
-    };
-    "1.7.0" = {
-      version = "1.7.0";
-      rev = "08b5481ed6ea1a5d2c4c068b62156f5be6d82b40";
-      sha256 = "1w7fmcpf0691gcwq00lm788k4ijlwz3667zj40j5jjc8j8hj7cq3";
-    };
-  };
-  param = params.${coqVersions.${coq.coq-version}};
-in
-
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-CoLoR-${param.version}";
+with lib; mkCoqDerivation {
+  pname = "color";
+  owner = "fblanqui";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    {case = range "8.10" "8.11"; out = "1.7.0"; }
+    {case = range "8.8"  "8.9";  out = "1.6.0"; }
+    {case = range "8.6"  "8.7";  out = "1.4.0"; }
+  ] null;
 
-  src = fetchFromGitHub {
-    owner = "fblanqui";
-    repo = "color";
-    inherit (param) rev sha256;
-  };
+  release."1.7.0".rev    = "08b5481ed6ea1a5d2c4c068b62156f5be6d82b40";
+  release."1.7.0".sha256 = "1w7fmcpf0691gcwq00lm788k4ijlwz3667zj40j5jjc8j8hj7cq3";
+  release."1.6.0".rev    = "328aa06270584b578edc0d2925e773cced4f14c8";
+  release."1.6.0".sha256 = "07sy9kw1qlynsqy251adgi8b3hghrc9xxl2rid6c82mxfsp329sd";
+  release."1.4.0".rev    = "168c6b86c7d3f87ee51791f795a8828b1521589a";
+  release."1.4.0".sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm";
 
-  buildInputs = [ coq bignums ];
+  extraBuildInputs = [ bignums ];
   enableParallelBuilding = false;
 
-  installPhase = ''
-    make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
-  '';
-
-  meta = with stdenv.lib; {
+  meta = {
     homepage = "http://color.inria.fr/";
     description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant.";
     maintainers = with maintainers; [ jpas jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v coqVersions;
   };
 }

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

···
-{ stdenv, fetchFromGitHub, autoconf, automake, coq }:
-
-stdenv.mkDerivation rec {
-  name = "coq${coq.coq-version}-HoTT-${version}";
-  version = "20170921";
+{ lib, mkCoqDerivation, autoconf, automake, coq, version ? null }:
 
-  src = fetchFromGitHub {
-    owner = "HoTT";
-    repo = "HoTT";
-    rev = "e3557740a699167e6adb1a65855509d55a392fa1";
-    sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v";
-  };
+with lib; mkCoqDerivation {
+  pname = "HoTT";
+  owner = "HoTT";
+  inherit version;
+  defaultVersion = if coq.coq-version == "8.6" then "20170921" else null;
+  release."20170921".rev    = "e3557740a699167e6adb1a65855509d55a392fa1";
+  release."20170921".sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v";
 
-  buildInputs = [ autoconf automake coq ];
-  enableParallelBuilding = true;
+  extraBuildInputs = [ autoconf automake ];
 
   preConfigure = ''
     patchShebangs ./autogen.sh
···
     rmdir $out/share
   '';
 
-  installFlags = [
-    "COQBIN=${coq}/bin"
-  ];
-
-  meta = with stdenv.lib; {
+  meta = {
     homepage = "http://homotopytypetheory.org/";
     description = "Homotopy type theory";
     maintainers = with maintainers; [ siddharthist ];
-    platforms = coq.meta.platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: v == "8.6";
   };
 }

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

···
-{ stdenv, fetchFromGitHub, coq }:
-
-let param =
-  {
-      version = "20200131";
-      rev = "203d4c20211d6b17741f1fdca46dbc091f5e961a";
-      sha256 = "0xylkdmb2dqnnqinf3pigz4mf4zmczcbpjnn59g5g76m7f2cqxl0";
-  };
-in
-
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-InfSeqExt-${param.version}";
-
-  src = fetchFromGitHub {
-    owner = "DistributedComponents";
-    repo = "InfSeqExt";
-    inherit (param) rev sha256;
-  };
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-  buildInputs = [ coq ];
-
-  enableParallelBuilding = true;
-
+mkCoqDerivation {
+  pname = "InfSeqExt";
+  owner = "DistributedComponents";
+  inherit version;
+  defaultVersion = if lib.versions.isGe "8.5" coq.coq-version then "20200131" else null;
+  release."20200131".rev    = "203d4c20211d6b17741f1fdca46dbc091f5e961a";
+  release."20200131".sha256 = "0xylkdmb2dqnnqinf3pigz4mf4zmczcbpjnn59g5g76m7f2cqxl0";
   preConfigure = "patchShebangs ./configure";
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
- };
 }

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

···
-{ stdenv, fetchFromGitHub, coq, ssreflect, coq-ext-lib, simple-io }:
-
-let params =
-  {
-    "8.5" = {
-      version = "20170512";
-      rev = "31eb050ae5ce57ab402db9726fb7cd945a0b4d03";
-      sha256 = "033ch10i5wmqyw8j6wnr0dlbnibgfpr1vr0c07q3yj6h23xkmqpg";
-    };
-
-    "8.6" = {
-      version = "20171102";
-      rev = "0fdb769e1dc87a278383b44a9f5102cc7ccbafcf";
-      sha256 = "0fri4nih40vfb0fbr82dsi631ydkw48xszinq43lyinpknf54y17";
-    };
-
-    "8.8" = {
-      version = "20190311";
-      rev = "22af9e9a223d0038f05638654422e637e863b355";
-      sha256 = "00rnr19lg6lg0haq1sy4ld38p7imzand6fc52fvfq27gblxkp2aq";
-    };
-
-    "8.9" = rec {
-      version = "1.1.0";
-      rev = "v${version}";
-      sha256 = "1c34v1k37rk7v0xk2czv5n79mbjxjrm6nh3llg2mpfmdsqi68wf3";
-    };
-
-    "8.10" = rec {
-      version = "1.2.1";
-      rev = "v${version}";
-      sha256 = "17vz88xjzxh3q7hs6hnndw61r3hdfawxp5awqpgfaxx4w6ni8z46";
-    };
-
-    "8.11" = rec {
-      version = "1.3.2";
-      rev = "v${version}";
-      sha256 = "0lciwaqv288dh2f13xk2x0lrn6zyrkqy6g4yy927wwzag2gklfrs";
-    };
-
-    "8.12" = rec {
-      version = "1.4.0";
-      rev = "v${version}";
-      sha256 = "068p48pm5yxjc3yv8qwzp25bp9kddvxj81l31mjkyx3sdrsw3kyc";
-    };
-  };
-  param = params.${coq.coq-version};
-in
-
-let inherit (stdenv.lib) maintainers optional optionals versionAtLeast; in
-
-let recent = versionAtLeast coq.coq-version "8.8"; in
-
-stdenv.mkDerivation {
-
-  name = "coq${coq.coq-version}-QuickChick-${param.version}";
-
-  src = fetchFromGitHub {
-    owner = "QuickChick";
-    repo = "QuickChick";
-    inherit (param) rev sha256;
-  };
+{ lib, mkCoqDerivation, coq, ssreflect, coq-ext-lib, simple-io }:
+with lib;
+let recent = versions.isGe "8.7" coq.coq-version; in
+mkCoqDerivation {
+  pname = "QuickChick";
+  owner = "QuickChick";
+  defaultVersion = with versions; switch [ coq.coq-version ssreflect.version ] [
+      { cases = [ "8.12" pred.true  ]; out = "1.4.0"; }
+      { cases = [ "8.11" pred.true  ]; out = "1.3.2"; }
+      { cases = [ "8.10" pred.true  ]; out = "1.2.1"; }
+      { cases = [ "8.9"  pred.true  ];  out = "1.1.0"; }
+      { cases = [ "8.8"  pred.true  ];  out = "20190311"; }
+      { cases = [ "8.7"  isLe "1.8" ];  out = "1.0.0"; }
+      { cases = [ "8.6"  pred.true  ];  out = "20171102"; }
+      { cases = [ "8.5"  pred.true  ];  out = "20170512"; }
+    ] null;
+  release."1.4.0".sha256    = "068p48pm5yxjc3yv8qwzp25bp9kddvxj81l31mjkyx3sdrsw3kyc";
+  release."1.3.2".sha256    = "0lciwaqv288dh2f13xk2x0lrn6zyrkqy6g4yy927wwzag2gklfrs";
+  release."1.2.1".sha256    = "17vz88xjzxh3q7hs6hnndw61r3hdfawxp5awqpgfaxx4w6ni8z46";
+  release."1.1.0".sha256    = "1c34v1k37rk7v0xk2czv5n79mbjxjrm6nh3llg2mpfmdsqi68wf3";
+  release."1.0.0".sha256    = "1gqy9a4yavd0sa7kgysf9gf2lq4p8dmn4h89y8081f2j8zli0w5y";
+  release."20190311".rev    = "22af9e9a223d0038f05638654422e637e863b355";
+  release."20190311".sha256 = "00rnr19lg6lg0haq1sy4ld38p7imzand6fc52fvfq27gblxkp2aq";
+  release."20171102".rev    = "0fdb769e1dc87a278383b44a9f5102cc7ccbafcf";
+  release."20171102".sha256 = "0fri4nih40vfb0fbr82dsi631ydkw48xszinq43lyinpknf54y17";
+  release."20170512".rev    = "31eb050ae5ce57ab402db9726fb7cd945a0b4d03";
+  release."20170512".sha256 = "033ch10i5wmqyw8j6wnr0dlbnibgfpr1vr0c07q3yj6h23xkmqpg";
+  releaseRev = v: "v${v}";
 
-  preConfigure = stdenv.lib.optionalString recent
+  preConfigure = optionalString recent
     "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native";
 
-  buildInputs = [ coq ]
-  ++ (with coq.ocamlPackages; [ ocaml findlib ])
-  ++ optionals (recent && !versionAtLeast coq.coq-version "8.10")
-       (with coq.ocamlPackages; [ camlp5 ocamlbuild ])
-  ++ optional recent coq.ocamlPackages.num
-  ;
+  mlPlugin = true;
+  extraBuildInputs = optional recent coq.ocamlPackages.num;
   propagatedBuildInputs = [ ssreflect ]
-  ++ optionals recent [ coq-ext-lib simple-io ]
-  ++ optional (versionAtLeast coq.coq-version "8.10")
-       coq.ocamlPackages.ocamlbuild
-  ;
+    ++ optionals recent [ coq-ext-lib simple-io ]
+    ++ optional  recent coq.ocamlPackages.ocamlbuild;
+  extraInstallFlags = [ "-f Makefile.coq" ];
 
   enableParallelBuilding = false;
-
-  installPhase = ''
-    make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
-  '';
 
   meta = {
-    homepage = "https://github.com/QuickChick/QuickChick";
     description = "Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck";
     maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v params;
-  };
-
 }

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

···
-{ stdenv, fetchFromGitHub, coq }:
-
-let param =
-  {
-      version = "20181102";
-      rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510";
-      sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v";
-  };
-in
-
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-StructTact-${param.version}";
-
-  src = fetchFromGitHub {
-    owner = "uwplse";
-    repo = "StructTact";
-    inherit (param) rev sha256;
-  };
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-  buildInputs = [ coq ];
-
-  enableParallelBuilding = true;
-
+with lib; mkCoqDerivation {
+  pname = "StructTact";
+  owner = "uwplse";
+  inherit version;
+  defaultVersion = if versions.isGe "8.5" coq.coq-version then "20181102" else null;
+  release."20181102".rev =    "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510";
+  release."20181102".sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v";
   preConfigure = "patchShebangs ./configure";
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  passthru = {
-    compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.5";
- };
 }

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

···
-{ stdenv, fetchFromGitHub, coq, compcert }:
+{ lib, mkCoqDerivation, coq, compcert, version ? null }:
 
-stdenv.mkDerivation rec {
+with lib; mkCoqDerivation {
   pname = "coq${coq.coq-version}-VST";
-  version = "2.6";
-
-  src = fetchFromGitHub {
-    owner = "PrincetonUniversity";
-    repo = "VST";
-    rev = "v${version}";
-    sha256 = "00bf9hl4pvmsqa08lzjs1mrxyfgfxq4k6778pnldmc8ichm90jgk";
-  };
-
-  buildInputs = [ coq ];
+  namePrefix = [];
+  displayVersion = { coq = false; };
+  owner = "PrincetonUniversity";
+  repo = "VST";
+  inherit version;
+  defaultVersion = if coq.coq-version == "8.11" then "2.6" else null;
+  release."2.6".sha256 = "00bf9hl4pvmsqa08lzjs1mrxyfgfxq4k6778pnldmc8ichm90jgk";
+  releaseRev = v: "v${v}";
   propagatedBuildInputs = [ compcert ];
 
   preConfigure = "patchShebangs util";
···
     done
   '';
 
-  enableParallelBuilding = true;
-
-  passthru.compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.11" ];
-
   meta = {
     description = "Verified Software Toolchain";
     homepage = "https://vst.cs.princeton.edu/";
     inherit (compcert.meta) platforms;
   };
-
 }

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

···
-{ stdenv, fetchFromGitHub, coq }:
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-let params =
-  {
-    "8.6" = {
-      version = "20180221";
-      rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b";
-      sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2";
-    };
+with lib; mkCoqDerivation {
+  pname = "Velisarios";
+  owner = "vrahli";
+  inherit version;
+  defaultVersion = if versions.range "8.6" "8.8" coq.coq-version then "20180221" else null;
 
-    "8.7" = {
-      version = "20180221";
-      rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b";
-      sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2";
-    };
-
-    "8.8" = {
-      version = "20180221";
-      rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b";
-      sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2";
-    };
-  };
-  param = params.${coq.coq-version};
-in
-
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-Velisarios-${param.version}";
-
-  src = fetchFromGitHub {
-    owner = "vrahli";
-    repo = "Velisarios";
-    inherit (param) rev sha256;
-  };
-
-  buildInputs = [
-    coq coq.ocaml coq.camlp5 coq.findlib
-  ];
-  enableParallelBuilding = true;
+  release."20180221".rev    = "e1eee1f10d5d46331a560bd8565ac101229d0d6b";
+  release."20180221".sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2";
+  mlPlugin = true;
 
   buildPhase = "make -j$NIX_BUILD_CORES";
   preBuild = "./create-makefile.sh";
···
     mkdir -p $out/lib/coq/${coq.coq-version}/Velisarios
     cp -pR model/*.vo $out/lib/coq/${coq.coq-version}/Velisarios
   '';
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" ];
- };
 }

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

···
-{ stdenv, fetchFromGitHub, coq, Cheerios, InfSeqExt, ssreflect }:
-
-let param =
-  if stdenv.lib.versionAtLeast coq.coq-version "8.7" then
-  {
-      version = "20200131";
-      rev = "fdb4ede19d2150c254f0ebcfbed4fb9547a734b0";
-      sha256 = "1a2k19f9q5k5djbxplqmmpwck49kw3lrm3aax920h4yb40czkd8m";
-  } else {
-      version = "20181102";
-      rev = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564";
-      sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z";
-  };
-in
+{ lib, mkCoqDerivation, coq, Cheerios, InfSeqExt, ssreflect, version ? null }:
 
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-verdi-${param.version}";
 
-  src = fetchFromGitHub {
-    owner = "uwplse";
-    repo = "verdi";
-    inherit (param) rev sha256;
-  };
+with lib; mkCoqDerivation {
+  pname = "verdi";
+  owner = "uwplse";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.7"; out = "20200131"; }
+    { case = isEq "8.6"; out = "20181102"; }
+  ] null;
+  release."20200131".rev    = "fdb4ede19d2150c254f0ebcfbed4fb9547a734b0";
+  release."20200131".sha256 = "1a2k19f9q5k5djbxplqmmpwck49kw3lrm3aax920h4yb40czkd8m";
+  release."20181102".rev    = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564";
+  release."20181102".sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z";
 
-  buildInputs = [ coq ];
   propagatedBuildInputs = [ Cheerios InfSeqExt ssreflect ];
-
-  enableParallelBuilding = true;
-
   preConfigure = "patchShebangs ./configure";
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
- };
 }

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

···
-{ stdenv, fetchgit, coq, mathcomp }:
+{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
 
-stdenv.mkDerivation rec {
+with lib; mkCoqDerivation {
+  pname   = "autosubst";
+  owner   = "uds-psl";
+  inherit version;
+  defaultVersion = with versions;
+    if range "8.5" "8.7" coq.coq-version then "5b40a32e" else null;
 
-  name = "coq-autosubst-${coq.coq-version}-${version}";
-  version = "5b40a32e";
+  release."5b40a32e".rev    = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034";
+  release."5b40a32e".sha256 = "1wqfzc9az85fvx71xxfii502jgc3mp0r3xwfb8vnb03vkk625ln0";
 
-  src = fetchgit {
-    url = "git://github.com/uds-psl/autosubst.git";
-    rev = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034";
-    sha256 = "06pcjbngzwqyncvfwzz88j33wvdj9kizxyg5adp7y6186h8an341";
-  };
-
-  buildInputs = [ coq ];
-  propagatedBuildInputs = [ mathcomp ];
+  propagatedBuildInputs = [ mathcomp.ssreflect ];
 
   patches = [./0001-changes-to-work-with-Coq-8.6.patch];
 
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  meta = with stdenv.lib; {
+  meta = {
     homepage = "https://www.ps.uni-saarland.de/autosubst/";
     description = "Automation for de Bruijn syntax and substitution in Coq";
     maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
-  };
-
-
 }

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

···
-{ stdenv, fetchFromGitHub, coq }:
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-let params = {
-      "8.6" = {
-        rev = "v8.6.0";
-        sha256 = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj";
-      };
-      "8.7" = {
-        rev = "V8.7.0";
-        sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
-      };
-      "8.8" = {
-        rev = "V8.8.0";
-        sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
-      };
-      "8.9" = {
-        rev = "V8.9.0";
-        sha256 = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01";
-      };
-      "8.10" = {
-        rev = "V8.10.0";
-        sha256 = "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5";
-      };
-      "8.11" = {
-        rev = "V8.11.0";
-        sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp";
-      };
-      "8.12" = {
-        rev = "V8.12.0";
-        sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8";
-      };
-      "8.13" = {
-        rev = "V8.13.0";
-        sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y";
-      };
-    };
-    param = params.${coq.coq-version};
-in
+with lib; mkCoqDerivation {
+  pname = "bignums";
+  owner = "coq";
+  displayVersion = { bignums = ""; };
+  inherit version;
+  defaultVersion = if versions.isGe "8.5" coq.coq-version
+    then "${coq.coq-version}.0" else null;
 
-stdenv.mkDerivation {
+  release."8.13.0".sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y";
+  release."8.12.0".sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8";
+  release."8.11.0".sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp";
+  release."8.10.0".sha256 = "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5";
+  release."8.9.0".sha256  = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01";
+  release."8.8.0".sha256  = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
+  release."8.7.0".sha256  = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
+  release."8.6.0".rev     = "v8.6.0";
+  release."8.6.0".sha256  = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj";
+  releaseRev = v: "V${v}";
 
-  name = "coq${coq.coq-version}-bignums";
+  mlPlugin = true;
 
-  src = fetchFromGitHub {
-    owner = "coq";
-    repo = "bignums";
-    inherit (param) rev sha256;
-  };
-
-  buildInputs = with coq.ocamlPackages; [ ocaml findlib coq ]
-  ++ stdenv.lib.optional (!stdenv.lib.versionAtLeast coq.coq-version "8.10") camlp5
-  ;
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  meta = with stdenv.lib; {
-    license = licenses.lgpl2;
-    platforms = coq.meta.platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v params;
-  };
+  meta = { license = licenses.lgpl2; };
 }

pkgs/development/coq-modules/category-theory/default.nix

···
-{ stdenv, fetchgit, coq, ssreflect, equations }:
+{ lib, mkCoqDerivation, coq, ssreflect, equations, version ? null }:
 
-let
-  params =
-    let
-    v20180709 = {
-      version = "20180709";
-      rev = "3b9ba7b26a64d49a55e8b6ccea570a7f32c11ead";
-      sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs";
-    };
-    v20190414 = {
-      version = "20190414";
-      rev = "706fdb4065cc2302d92ac2bce62cb59713253119";
-      sha256 = "16lg4xs2wzbdbsn148xiacgl4wq4xwfqjnjkdhfr3w0qh1s81hay";
-    };
-  in {
-    "8.6" = v20180709;
-    "8.7" = v20180709;
-    "8.8" = v20190414;
-    "8.9" = v20190414;
-  };
-  param = params.${coq.coq-version};
-in
+with lib; mkCoqDerivation {
 
-stdenv.mkDerivation {
+  pname = "category-theory";
+  owner = "jwiegley";
 
-  name = "coq${coq.coq-version}-category-theory-${param.version}";
+  release."20190414".rev    = "706fdb4065cc2302d92ac2bce62cb59713253119";
+  release."20190414".sha256 = "16lg4xs2wzbdbsn148xiacgl4wq4xwfqjnjkdhfr3w0qh1s81hay";
+  release."20180709".rev    = "3b9ba7b26a64d49a55e8b6ccea570a7f32c11ead";
+  release."20180709".sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs";
 
-  src = fetchgit {
-    url = "git://github.com/jwiegley/category-theory.git";
-    inherit (param) rev sha256;
-  };
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.8" "8.9"; out = "20190414"; }
+    { case = range "8.6" "8.7"; out = "20180709"; }
+  ] null;
 
-  buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml camlp5 findlib ]);
+  mlPlugin = true;
   propagatedBuildInputs = [ ssreflect equations ];
 
-  buildFlags = [ "JOBS=$(NIX_BUILD_CORES)" ];
-
-  installPhase = ''
-    make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
-  '';
-
-  meta = with stdenv.lib; {
-    homepage = "https://github.com/jwiegley/category-theory";
+  meta = {
     description = "A formalization of category theory in Coq for personal study and practical work";
     maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v params;
-  };
-
 }

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

···
-{ stdenv, fetchFromGitHub, coq }:
+{ lib, mkCoqDerivation, coq, callPackage }:
 
-let mkContrib = repo: revs: param:
-  stdenv.mkDerivation rec {
-    name = "coq${coq.coq-version}-${repo}-${version}";
-    version = param.version;
-
-    src = fetchFromGitHub {
+with lib; let mkContrib = pname: coqs: param:
+  let contribVersion = {version ? null}: mkCoqDerivation ({
+      inherit pname version;
       owner = "coq-contribs";
-      repo = repo;
-      rev = param.rev;
-      sha256 = param.sha256;
-    };
-
-    buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ];
-
-    installFlags =
-       stdenv.lib.optional (stdenv.lib.versionAtLeast coq.coq-version "8.9") "-f Makefile.coq"
-    ++ [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-    passthru = {
-      compatibleCoqVersions = v: builtins.elem v revs;
-    };
-  }; in
+      mlPlugin = true;
+    } // optionalAttrs (builtins.elem coq.coq-version coqs) ({
+      defaultVersion = param.version;
+      release = { "${param.version}" = { inherit (param) rev sha256; }; };
+    } // (removeAttrs param [ "version" "rev" "sha256" ]))
+  ); in
+  makeOverridable contribVersion {} ; in
 {
   aac-tactics = mkContrib "aac-tactics" [ "8.7" "8.8" ] {
     "8.7" = {
···
     sha256 = "02jcp74i5icv92xkq3mcx91786d56622ghgnjiz3b51wfqs6ldic";
   };
 
-  firing-squad = mkContrib "firing-squad" [ "8.6" "8.7" ] {
-    version = "v8.5.0-9-gbe728cd";
-    rev = "be728cddbee58088809b51c25425d2a4bdf9b823";
-    sha256 = "0i0v5x6lncjasxk22pras3644ff026q8jai45dbimf2fz73312c9";
+  firing-squad = mkContrib "firing-squad" [ "8.6" ] {
+      version = "v8.5.0-9-gbe728cd";
+      rev = "be728cddbee58088809b51c25425d2a4bdf9b823";
+      sha256 = "0i0v5x6lncjasxk22pras3644ff026q8jai45dbimf2fz73312c9";
   };
 
   float = mkContrib "float" [ "8.7" ] {
···
     version = "v8.6.0";
     rev = "6279ed83244dc4aec2e23ffb4c87e3f10a50326d";
     sha256 = "1yvlnqwa7ka4a0yg0j7zrzvayhsm1shvsjjawjv552sxc9519aag";
+    installFlags = [ "COQBIN=$(out)/lib/coq/${coq.coq-version}/bin/" ]; # hack
   };
 
   ipc = mkContrib "ipc" [ "8.6" "8.7" ] {
···
     version = "v8.5.0-7-ge54c9a8";
     rev = "e54c9a86df5cb90ef6ea04d3753273186bb2d906";
     sha256 = "19csz50846gvfwmhhc37nmlvf70g53cpb1kpmcnjlj82y8r63ajz";
-  };
-
-  math-classes = mkContrib "math-classes" [ "8.6" ] {
-    version = "v8.6.0-19-ge2c6453";
-    rev = "e2c6453e2f6cc1b7f0e1371675f4a76b19fab2c7";
-    sha256 = "0das56i8wi7v0s30lbadjlfqas1jlq0mm13yxq6s7zqqbdl5r0bk";
   };
 
   maths = mkContrib "maths" [ "8.5" "8.6" "8.7" ] {

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

···
-{ stdenv, fetchFromGitHub, coq, mathcomp-algebra }:
+{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
 
-let
-  version = "20190812";
-in
-
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-coq-bits-${version}";
-
-  src = fetchFromGitHub {
-    owner = "coq-community";
-    repo = "bits";
-    rev = "1.0.0";
-    sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";
-  };
+with lib; mkCoqDerivation {
+  pname = "coq-bits";
+  repo = "bits";
+  inherit version;
+  defaultVersion = if versions.isGe "8.7" coq.version then "20190812" else null;
 
-  buildInputs = [ coq ];
-  propagatedBuildInputs = [ mathcomp-algebra ];
+  release."20190812".rev    = "1.0.0";
+  release."20190812".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";
 
-  enableParallelBuilding = true;
+  propagatedBuildInputs = [ mathcomp.algebra ];
 
   installPhase = ''
     make -f Makefile CoqMakefile
     make -f CoqMakefile COQLIB=$out/lib/coq/${coq.coq-version}/ install
   '';
 
-  meta = with stdenv.lib; {
-    homepage = "https://github.com/coq-community/bits";
+  meta = {
     description = "A formalization of bitset operations in Coq";
     license = licenses.asl20;
     maintainers = with maintainers; [ ptival ];
-    platforms = coq.meta.platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
   };
 }

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

···
-{ stdenv, fetchFromGitHub, which, coq }:
-
-let params = {
-  "8.11" = rec {
-    version = "1.6.0_8.11";
-    rev = "v${version}";
-    sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
-  };
-  "8.12" = rec {
-    version = "1.6.0";
-    rev = "v${version}";
-    sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
-  };
-};
-  param = params.${coq.coq-version};
-in
+{ lib, mkCoqDerivation, which, coq, version ? null }:
 
-stdenv.mkDerivation rec {
-  name = "coq${coq.coq-version}-elpi-${param.version}";
-
-  src = fetchFromGitHub {
-    owner = "LPCIC";
-    repo = "coq-elpi";
-    inherit (param) rev sha256;
-  };
+with builtins; with lib; let
+  elpi = coq.ocamlPackages.elpi.override (
+    optionalAttrs (coq.coq-version == "8.11") { version = "1.11.4"; }
+  );
+in mkCoqDerivation {
+  pname = "elpi";
+  repo  = "coq-elpi";
+  owner = "LPCIC";
+  inherit version;
+  defaultVersion = lib.switch coq.coq-version [
+    { case = "8.13"; out = "1.8.1"; }
+    { case = "8.12"; out = "1.8.0"; }
+    { case = "8.11"; out = "1.6.0_8.11"; }
+  ] null;
+  release."1.8.1".sha256      = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r";
+  release."1.8.0".sha256      = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1";
+  release."1.7.0".sha256      = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8";
+  release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
+  release."1.6.0".sha256      = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
+  releaseRev = v: "v${v}";
 
   nativeBuildInputs = [ which ];
-  buildInputs = [ coq coq.ocaml ] ++ (with coq.ocamlPackages; [ findlib elpi ]);
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+  mlPlugin = true;
+  extraBuildInputs = [ elpi ];
 
   meta = {
     description = "Coq plugin embedding ELPI.";
-    maintainers = [ stdenv.lib.maintainers.cohencyril ];
-    license = stdenv.lib.licenses.lgpl21;
-    inherit (coq.meta) platforms;
-    inherit (src.meta) homepage;
-  };
-
-  passthru = {
-    compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params;
+    maintainers = [ maintainers.cohencyril ];
+    license = licenses.lgpl21;
   };
 }

pkgs/development/coq-modules/coq-ext-lib/default.nix

···
-{ stdenv, fetchFromGitHub, coq, ...}@args:
-
-let
-  hashes = {
-    "0.9.4" = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0";
-    "0.9.5" = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg";
-    "0.9.7" = "00v4bm4glv1hy08c8xsm467az6d1ashrznn8p2bmbmmp52lfg7ag";
-    "0.10.0" = "1kxi5bmjwi5zqlqgkyzhhxwgcih7wf60cyw9398k2qjkmi186r4a";
-    "0.10.1" = "0r1vspad8fb8bry3zliiz4hfj4w1iib1l2gm115a94m6zbiksd95";
-    "0.10.2" = "1b150rc5bmz9l518r4m3vwcrcnnkkn9q5lrwygkh0a7mckgg2k9f";
-    "0.10.3" = "0795gs2dlr663z826mp63c8h2zfadn541dr8q0fvnvi2z7kfyslb";
-    "0.11.1" = "0dmf1p9j8lm0hwaq0af18jxdwg869xi2jm8447zng7krrq3kvkg5";
-    "0.11.2" = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6";
-    "0.11.3" = "1w99nzpk72lffxis97k235axss5lmzhy5z3lga2i0si95mbpil42";
-  };
-
-  default-versions = {
-    "8.5" = "0.9.4";
-    "8.6" = "0.9.5";
-    "8.7" = "0.9.7";
-    "8.8" = "0.11.3";
-    "8.9" = "0.11.3";
-    "8.10" = "0.11.3";
-    "8.11" = "0.11.3";
-    "8.12" = "0.11.3";
-  };
-
-  param = rec {
-    version = args.version or default-versions.${coq.coq-version};
-    sha256 = hashes.${version};
-  };
-
-in
-
-stdenv.mkDerivation rec {
-
-  name = "coq${coq.coq-version}-coq-ext-lib-${version}";
-  inherit (param) version;
-
-  src = fetchFromGitHub {
-    owner = "coq-community";
-    repo = "coq-ext-lib";
-    rev = "v${version}";
-    inherit (param) sha256;
-  };
-
-  buildInputs = [ coq ];
-
-  enableParallelBuilding = true;
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+with lib; mkCoqDerivation rec {
+  pname = "coq-ext-lib";
+  owner = "coq-ext-lib";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.8" "8.12"; out = "0.11.3"; }
+    { case = "8.7";              out = "0.9.7"; }
+    { case = "8.6";              out = "0.9.5"; }
+    { case = "8.5";              out = "0.9.4"; }
+  ] null;
+  release."0.11.3".sha256 = "1w99nzpk72lffxis97k235axss5lmzhy5z3lga2i0si95mbpil42";
+  release."0.11.2".sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6";
+  release."0.10.3".sha256 = "0795gs2dlr663z826mp63c8h2zfadn541dr8q0fvnvi2z7kfyslb";
+  release."0.11.1".sha256 = "0dmf1p9j8lm0hwaq0af18jxdwg869xi2jm8447zng7krrq3kvkg5";
+  release."0.10.2".sha256 = "1b150rc5bmz9l518r4m3vwcrcnnkkn9q5lrwygkh0a7mckgg2k9f";
+  release."0.10.1".sha256 = "0r1vspad8fb8bry3zliiz4hfj4w1iib1l2gm115a94m6zbiksd95";
+  release."0.10.0".sha256 = "1kxi5bmjwi5zqlqgkyzhhxwgcih7wf60cyw9398k2qjkmi186r4a";
+  release."0.9.7".sha256  = "00v4bm4glv1hy08c8xsm467az6d1ashrznn8p2bmbmmp52lfg7ag";
+  release."0.9.5".sha256  = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg";
+  release."0.9.4".sha256  = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0";
+  releaseRev = v: "v${v}";
 
-  meta = with stdenv.lib; {
-    homepage = "https://github.com/coq-ext-lib/coq-ext-lib";
+  meta = {
     description = "A collection of theories and plugins that may be useful in other Coq developments";
     maintainers = with maintainers; [ jwiegley ptival ];
-    platforms = coq.meta.platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v default-versions;
   };
 }

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

···
-{ stdenv, fetchgit, coq, ssreflect }:
+{ lib, mkCoqDerivation, coq, ssreflect, version ? null }:
 
-let params =
-  {
-    "8.5" = {
-      version = "20171215";
-      rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
-      sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
-    };
+with lib; mkCoqDerivation {
 
-    "8.6" = {
-      version = "20171215";
-      rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
-      sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
-    };
+  pname = "coq-haskell";
+  owner = "jwiegley";
+  inherit version;
+  defaultVersion = if versions.range "8.5" "8.8" coq.coq-version then "20171215" else null;
+  release."20171215".rev    = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
+  release."20171215".sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
 
-    "8.7" = {
-      version = "20171215";
-      rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
-      sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
-    };
-
-    "8.8" = {
-      version = "20171215";
-      rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
-      sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
-    };
-  };
-  param = params.${coq.coq-version};
-in
-
-stdenv.mkDerivation {
-
-  name = "coq${coq.coq-version}-coq-haskell-${param.version}";
-
-  src = fetchgit {
-    url = "git://github.com/jwiegley/coq-haskell.git";
-    inherit (param) rev sha256;
-  };
-
-  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib ];
+  mlPlugin = true;
+  extraInstallFlags = [ "-f Makefile.coq" ];
   propagatedBuildInputs = [ coq ssreflect ];
-
   enableParallelBuilding = false;
 
-  installPhase = ''
-    make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
-  '';
-
-  meta = with stdenv.lib; {
-    homepage = "https://github.com/jwiegley/coq-haskell";
+  meta = {
     description = "A library for formalizing Haskell types and functions in Coq";
     maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v params;
   };
 }

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

···
+{ coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials,
+  lib, which, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  pname = "CoqEAL";
+  owner = "CoqEAL";
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+      { cases = [ (isGe "8.7") "1.11.0" ]; out = "1.0.4"; }
+      { cases = [ (isGe "8.7") "1.10.0" ]; out = "1.0.3"; }
+    ] null;
+
+  release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk";
+  release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
+
+  extraBuildInputs = [ which ];
+  propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ];
+
+  meta = {
+    description = "CoqEAL - The Coq Effective Algebra Library";
+    license = licenses.mit;
+  };
+}

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

···
-{ stdenv, fetchFromGitHub, coq }:
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-let
-  params = {
-    "8.8" = {
-      version = "1.1";
-      sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h";
-      buildInputs = [ coq.ocamlPackages.camlp5 ];
-    };
-    "8.9" = {
-      version = "1.1.1";
-      sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9";
-      buildInputs = [ coq.ocamlPackages.camlp5 ];
-    };
-    "8.10" = {
-      version = "1.3";
-      sha256 = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd";
-    };
-    "8.11" = {
-      version = "1.3";
-      sha256 = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b";
-    };
-    "8.12" = {
-      version = "1.3";
-      sha256 = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8";
-    };
-  };
-  param = params.${coq.coq-version};
-in
+with lib; mkCoqDerivation {
+  inherit version;
+  pname = "coqhammer";
+  owner = "lukaszcz";
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = "8.12"; out = "1.3-coq8.12"; }
+    { case = "8.11"; out = "1.3-coq8.11"; }
+    { case = "8.10"; out = "1.3-coq8.10"; }
+    { case = "8.9";  out = "1.1.1-coq8.9"; }
+    { case = "8.8";  out = "1.1-coq8.8"; }
+  ] null;
+  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";
 
-stdenv.mkDerivation rec {
-  inherit (param) version;
-  name = "coq${coq.coq-version}-coqhammer-${version}";
-
-  src = fetchFromGitHub {
-    owner = "lukaszcz";
-    repo = "coqhammer";
-    rev = "v${version}-coq${coq.coq-version}";
-    inherit (param) sha256;
-  };
+  release."1.3-coq8.12".version  = "1.3";
+  release."1.3-coq8.11".version  = "1.3";
+  release."1.3-coq8.10".version  = "1.3";
+  release."1.1.1-coq8.9".version = "1.1.1";
+  release."1.1-coq8.9".version   = "1.1";
+  releaseRev = v: "v${v}";
 
   postPatch = ''
     substituteInPlace Makefile.coq.local --replace \
···
     substituteInPlace Makefile.coq.local --replace 'g++' 'c++' --replace 'gcc' 'cc'
   '';
 
-  buildInputs = [ coq ] ++ (with coq.ocamlPackages; [
-    ocaml findlib
-  ]) ++ (param.buildInputs or []);
-
   preInstall = ''
     mkdir -p $out/bin
   '';
 
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+  mlPlugin = true;
 
   meta = {
     homepage = "http://cl-informatik.uibk.ac.at/cek/coqhammer/";
     description = "Automation for Dependent Type Theory";
-    license = stdenv.lib.licenses.lgpl21;
-    inherit (coq.meta) platforms;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
+    license = licenses.lgpl21;
+    maintainers = [ maintainers.vbgl ];
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v params;
-  };
-
 }

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

···
-{ stdenv, which, fetchFromGitHub, coq, bignums }:
+{ which, lib, mkCoqDerivation, coq, bignums, version ? null }:
 
-let
-  params =
-    let v_8_8 = {
-          version = "8.8";
-          sha256 = "075yjczk79pf1hd3lgdjiz84ilkzfxjh18lgzrhhqp7d3kz5lxp5";
-        };
-        v_8_10 = {
-          version = "8.10";
-          sha256 = "0r9gnh5a5ykiiz5h1i8xnzgiydpwc4z9qhndxyya85xq0f910qaz";
-        };
-    in
-      {
-        "8.7" = {
-          version = "8.7.2";
-          sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k";
-        };
-        "8.8" = v_8_8;
-        "8.9" = v_8_8;
-        "8.10" = v_8_10;
-        "8.11" = v_8_10;
-	"8.12" = {
-	  version = "8.12";
-          sha256 = "1slka4w0pya15js4drx9frj7lxyp3k2lzib8v23givzpnxs8ijdj";
-	};
-      };
-  param = params.${coq.coq-version};
-in
+with lib; mkCoqDerivation {
 
-stdenv.mkDerivation rec {
+  pname = "coqprime";
+  owner = "thery";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = "8.12";              out = "8.12"; }
+    { case = range "8.10" "8.11"; out = "8.10"; }
+    { case = range "8.8"  "8.9";  out = "8.8"; }
+    { case = "8.7";               out = "8.7.2"; }
+  ] null;
 
-  inherit (param) version;
-  name = "coq${coq.coq-version}-coqprime-${version}";
-
-  src = fetchFromGitHub {
-    owner = "thery";
-    repo = "coqprime";
-    rev = "v${version}";
-    inherit (param) sha256;
-  };
-
-  buildInputs = [ which coq ];
+  release."8.12".sha256  = "1slka4w0pya15js4drx9frj7lxyp3k2lzib8v23givzpnxs8ijdj";
+  release."8.10".sha256  = "0r9gnh5a5ykiiz5h1i8xnzgiydpwc4z9qhndxyya85xq0f910qaz";
+  release."8.8".sha256   = "075yjczk79pf1hd3lgdjiz84ilkzfxjh18lgzrhhqp7d3kz5lxp5";
+  release."8.7.2".sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k";
+  releaseRev = v: "v${v}";
 
+  extraBuildInputs = [ which ];
   propagatedBuildInputs = [ bignums ];
 
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Library to certify primality using Pocklington certificate and Elliptic Curve Certificate";
     license = licenses.lgpl21;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
-    inherit (coq.meta) platforms;
-    inherit (src.meta) homepage;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v params;
+    maintainers = [ maintainers.vbgl ];
   };
 }

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

···
-{ stdenv, fetchurl, which, coq, ssreflect }:
+{ lib, mkCoqDerivation, which, autoconf,
+  coq, ssreflect, version ? null }:
 
-let param =
-  if stdenv.lib.versionAtLeast coq.coq-version "8.8"
-  then {
-    version = "3.1.0";
-    uid = "38287";
-    sha256 = "07436wkvnq9jyf7wyhp77bpl157s3qhba1ay5xrkxdi26qdf3h14";
-  } else {
-    version = "3.0.2";
-    uid = "37523";
-    sha256 = "1biia7nfqf7vaqq5gmykl4rwjyvrcwss6r2jdf0in5pvp2rnrj2w";
-  }
-; in
-
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-coquelicot-${param.version}";
-  src = fetchurl {
-    url = "https://gforge.inria.fr/frs/download.php/file/${param.uid}/coquelicot-${param.version}.tar.gz";
-    inherit (param) sha256;
-  };
+with lib; mkCoqDerivation {
+  pname = "coquelicot";
+  owner = "coquelicot";
+  domain = "gitlab.inria.fr";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.8" ;        out = "3.2.0"; }
+    { case = range "8.8" "8.13"; out = "3.1.0"; }
+    { case = range "8.5" "8.9";  out = "3.0.2"; }
+  ] null;
+  release."3.2.0".sha256 = "07w7dbl8x7xxnbr2q39wrdh054gvi3daqjpdn1jm53crsl1fjxm4";
+  release."3.1.0".sha256 = "02i0djar13yk01hzaqprcldhhscn9843x9nf6x3jkv4wv1jwnx9f";
+  release."3.0.2".sha256 = "1rqfbbskgz7b1bcpva8wh3v3456sq2364y804f94sc8y5sij23nl";
+  releaseRev = v: "coquelicot-${v}";
 
-  nativeBuildInputs = [ which ];
-  buildInputs = [ coq ];
+  nativeBuildInputs = [ which autoconf ];
   propagatedBuildInputs = [ ssreflect ];
-
-  configureFlags = [ "--libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Coquelicot" ];
-  buildPhase = "./remake";
-  installPhase = "./remake install";
+  useMelquiondRemake.logpath = "Coquelicot";
 
   meta = {
     homepage = "http://coquelicot.saclay.inria.fr/";
     description = "A Coq library for Reals";
-    license = stdenv.lib.licenses.lgpl3;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
-    inherit (coq.meta) platforms;
+    license = licenses.lgpl3;
+    maintainers = [ maintainers.vbgl ];
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
-  };
-
 }

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

···
-{ stdenv, fetchFromGitHub, coq, bignums, math-classes }:
+{ lib, mkCoqDerivation, coq, bignums, math-classes, version ? null }:
 
-stdenv.mkDerivation rec {
+with lib; mkCoqDerivation rec {
   pname = "corn";
-  version = "8.8.1";
-  name = "coq${coq.coq-version}-${pname}-${version}";
-  src = fetchFromGitHub {
-    owner = "coq-community";
-    repo = pname;
-    rev = version;
-    sha256 = "0gh32j0f18vv5lmf6nb87nr5450w6ai06rhrnvlx2wwi79gv10wp";
-  };
-
-  buildInputs = [ coq ];
+  inherit version;
+  defaultVersion = if versions.range "8.6" "8.9" coq.coq-version then "8.8.1" else null;
+  release."8.8.1".sha256 = "0gh32j0f18vv5lmf6nb87nr5450w6ai06rhrnvlx2wwi79gv10wp";
 
   preConfigure = "patchShebangs ./configure.sh";
   configureScript = "./configure.sh";
···
 
   propagatedBuildInputs = [ bignums math-classes ];
 
-  enableParallelBuilding = true;
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
   meta = {
     homepage = "http://c-corn.github.io/";
-    license = stdenv.lib.licenses.gpl2;
+    license = licenses.gpl2;
     description = "A Coq library for constructive analysis";
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
-    inherit (coq.meta) platforms;
+    maintainers = [ maintainers.vbgl ];
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ];
-  };
-
 }

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

···
-{ stdenv, fetchFromGitHub, autoreconfHook, coq }:
+{ lib, mkCoqDerivation, autoreconfHook, coq, version ? null }:
 
-let params = {
-  "8.12" = {
-    version = "0.6.8";
-    sha256 = "1mj6sknsd53xfb387sp3kdwvl4wn80ck24bfzf3s6mgw1a12vyps";
-  };
-  "8.11" = {
-    version = "0.6.7";
-    sha256 = "01vpi7scvkl4ls1z2k2x9zd65wflzb667idj759859hlz3ps9z09";
-  };
-  "8.10" = {
-    version = "0.6.6";
-    sha256 = "1gjrm5zjzw4cisiwdr5b3iqa7s4cssa220xr0k96rwgk61rcjd8w";
-  };
-  "8.9" = {
-    version = "0.6.5";
-    sha256 = "1f34z24yg05b1096gqv36jr3vffkcjkf9qncii3pzhhvagxd0w2f";
-  };
-  "8.8" = {
-    version = "0.6.3";
-    rev = "0acbd0a594c7e927574d5f212cc73a486b5305d2";
-    sha256 = "0c95b0bz2kjm6swr5na4gs06lxxywradszxbr5ldh2zx02r3f3rx";
-  };
-  "8.7" = {
-    version = "0.6.2";
-    rev = "d76ddde37d918569945774733b7997e8b24daf51";
-    sha256 = "04lnf4b25yarysj848cfl8pd3i3pr3818acyp9hgwdgd1rqmhjwm";
-  };
-  "8.6" = {
-    version = "0.6.1";
-    rev = "c3b87af6bfa338e18b83f014ebd0e56e1f611663";
-    sha256 = "1jaafkwsb5450378nprjsds1illgdaq60gryi8kspw0i25ykz2c9";
-  };
-  "8.5" = {
-    version = "0.6";
-    sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n";
-  };
-};
-param = params.${coq.coq-version};
-in
+with lib;
+let hasWarning = versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in
 
-let hasWarning = stdenv.lib.versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in
+mkCoqDerivation {
+  pname = "dpdgraph";
+  owner = "Karmaki";
+  repo = "coq-dpdgraph";
+  inherit version;
+  defaultVersion = switch coq.coq-version [
+    { case = "8.12"; out = "0.6.8"; }
+    { case = "8.11"; out = "0.6.7"; }
+    { case = "8.10"; out = "0.6.6"; }
+    { case = "8.9";  out = "0.6.5"; }
+    { case = "8.8";  out = "0.6.3"; }
+    { case = "8.7";  out = "0.6.2"; }
+    { case = "8.6";  out = "0.6.1"; }
+    { case = "8.5";  out = "0.6"; }
+  ] null;
 
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-dpdgraph-${param.version}";
-  src = fetchFromGitHub {
-    owner = "Karmaki";
-    repo = "coq-dpdgraph";
-    rev = param.rev or "v${param.version}";
-    inherit (param) sha256;
-  };
+  release."0.6.8".sha256 = "1mj6sknsd53xfb387sp3kdwvl4wn80ck24bfzf3s6mgw1a12vyps";
+  release."0.6.7".sha256 = "01vpi7scvkl4ls1z2k2x9zd65wflzb667idj759859hlz3ps9z09";
+  release."0.6.6".sha256 = "1gjrm5zjzw4cisiwdr5b3iqa7s4cssa220xr0k96rwgk61rcjd8w";
+  release."0.6.5".sha256 = "1f34z24yg05b1096gqv36jr3vffkcjkf9qncii3pzhhvagxd0w2f";
+  release."0.6.3".rev    = "0acbd0a594c7e927574d5f212cc73a486b5305d2";
+  release."0.6.3".sha256 = "0c95b0bz2kjm6swr5na4gs06lxxywradszxbr5ldh2zx02r3f3rx";
+  release."0.6.2".rev    = "d76ddde37d918569945774733b7997e8b24daf51";
+  release."0.6.2".sha256 = "04lnf4b25yarysj848cfl8pd3i3pr3818acyp9hgwdgd1rqmhjwm";
+  release."0.6.1".rev    = "c3b87af6bfa338e18b83f014ebd0e56e1f611663";
+  release."0.6.1".sha256 = "1jaafkwsb5450378nprjsds1illgdaq60gryi8kspw0i25ykz2c9";
+  release."0.6".sha256   = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n";
+  releaseRev = v: "v${v}";
 
   nativeBuildInputs = [ autoreconfHook ];
-  buildInputs = [ coq ]
-  ++ (with coq.ocamlPackages; [ ocaml findlib ocamlgraph ]
-    ++ stdenv.lib.optional (!stdenv.lib.versionAtLeast coq.coq-version "8.10") camlp5);
+  mlPlugin = true;
+  extraBuildInputs = [ coq.ocamlPackages.ocamlgraph ];
 
   # dpd_compute.ml uses deprecated Pervasives.compare
   # Versions prior to 0.6.5 do not have the WARN_ERR build flag
-  preConfigure = stdenv.lib.optionalString hasWarning ''
+  preConfigure = optionalString hasWarning ''
     substituteInPlace Makefile.in --replace "-warn-error +a " ""
   '';
 
-  buildFlags = stdenv.lib.optional hasWarning "WARN_ERR=";
+  buildFlags = optional hasWarning "WARN_ERR=";
 
   preInstall = ''
     mkdir -p $out/bin
   '';
 
-  installFlags = [
-    "COQLIB=$(out)/lib/coq/${coq.coq-version}/"
-    "BINDIR=$(out)/bin"
-  ];
+  extraInstallFlags = [ "BINDIR=$(out)/bin" ];
 
   meta = {
     description = "Build dependency graphs between Coq objects";
-    license = stdenv.lib.licenses.lgpl21;
-    homepage = "https://github.com/Karmaki/coq-dpdgraph/";
-    maintainers = with stdenv.lib.maintainers; [ vbgl ];
-    platforms = coq.meta.platforms;
+    license = licenses.lgpl21;
+    maintainers = with maintainers; [ vbgl ];
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v params;
-  };
-
 }

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

···
-{ stdenv, fetchFromGitHub, coq }:
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-let
-  params = {
-    "8.6" = {
-      version = "1.0";
-      rev = "v1.0";
-      sha256 = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj";
-    };
+with lib; mkCoqDerivation {
+  pname = "equations";
+  owner = "mattam82";
+  repo = "Coq-Equations";
+  inherit version;
+  defaultVersion = switch coq.coq-version [
+    { case = "8.12"; out = "1.2.3+coq8.12"; }
+    { case = "8.11"; out = "1.2.3+coq8.11"; }
+    { case = "8.10"; out = "1.2.1+coq8.10-2"; }
+    { case = "8.9";  out = "1.2.1+coq8.9"; }
+    { case = "8.8";  out = "1.2+coq8.8"; }
+    { case = "8.7";  out = "1.0+coq8.7"; }
+    { case = "8.6";  out = "1.0+coq8.6"; }
+  ] null;
 
-    "8.7" = {
-      version = "1.0";
-      rev = "v1.0-8.7";
-      sha256 = "1bavg4zl1xn0jqrdq8iw7xqzdvdf39ligj9saz5m9c507zri952h";
-    };
+    release."1.0+coq8.6".version      = "1.0";
+    release."1.0+coq8.6".rev          = "v1.0";
+    release."1.0+coq8.6".sha256       = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj";
+    release."1.0+coq8.7".version      = "1.0";
+    release."1.0+coq8.7".rev          = "v1.0-8.7";
+    release."1.0+coq8.7".sha256       = "1bavg4zl1xn0jqrdq8iw7xqzdvdf39ligj9saz5m9c507zri952h";
+    release."1.2+coq8.8".version      = "1.2";
+    release."1.2+coq8.8".rev          = "v1.2-8.8";
+    release."1.2+coq8.8".sha256       = "06452fyzalz7zcjjp73qb7d6xvmqb6skljkivf8pfm55fsc8s7kx";
+    release."1.2.1+coq8.9".version    = "1.2.1";
+    release."1.2.1+coq8.9".rev        = "v1.2.1-8.9";
+    release."1.2.1+coq8.9".sha256     = "0d8ddj6nc6p0k25cd8fs17cq427zhzbc3v9pk2wd2fnvk70nlfij";
+    release."1.2.1+coq8.10-2".version = "1.2.1";
+    release."1.2.1+coq8.10-2".rev     = "v1.2.1-8.10-2";
+    release."1.2.1+coq8.10-2".sha256  = "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68";
+    release."1.2.3+coq8.11".version   = "1.2.3";
+    release."1.2.3+coq8.11".rev       = "v1.2.3-8.11";
+    release."1.2.3+coq8.11".sha256    = "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf";
+    release."1.2.3+coq8.12".version   = "1.2.3";
+    release."1.2.3+coq8.12".rev       = "v1.2.3-8.12";
+    release."1.2.3+coq8.12".sha256    = "1y0jkvzyz5ssv5vby41p1i8zs7nsdc8g3pzyq73ih9jz8h252643";
 
-    "8.8" = {
-      version = "1.2";
-      rev = "v1.2-8.8";
-      sha256 = "06452fyzalz7zcjjp73qb7d6xvmqb6skljkivf8pfm55fsc8s7kx";
-    };
-
-    "8.9" = {
-      version = "1.2.1";
-      rev = "v1.2.1-8.9";
-      sha256 = "0d8ddj6nc6p0k25cd8fs17cq427zhzbc3v9pk2wd2fnvk70nlfij";
-    };
-
-    "8.10" = {
-      version = "1.2.1";
-      rev = "v1.2.1-8.10-2";
-      sha256 = "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68";
-    };
-
-    "8.11" = {
-      version = "1.2.3";
-      rev = "v1.2.3-8.11";
-      sha256 = "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf";
-    };
-
-    "8.12" = {
-      version = "1.2.3";
-      rev = "v1.2.3-8.12";
-      sha256 = "1y0jkvzyz5ssv5vby41p1i8zs7nsdc8g3pzyq73ih9jz8h252643";
-    };
-  };
-  param = params.${coq.coq-version};
-in
-
-stdenv.mkDerivation rec {
-
-  name = "coq${coq.coq-version}-equations-${version}";
-  version = param.version;
-
-  src = fetchFromGitHub {
-    owner = "mattam82";
-    repo = "Coq-Equations";
-    rev = param.rev;
-    sha256 = param.sha256;
-  };
-
-  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ];
-
+  mlPlugin = true;
   preBuild = "coq_makefile -f _CoqProject -o Makefile";
 
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  meta = with stdenv.lib; {
+  meta = {
     homepage = "https://mattam82.github.io/Coq-Equations/";
     description = "A plugin for Coq to add dependent pattern-matching";
     maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v params;
-  };
-
 }

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

···
-{stdenv, fetchgit, coq, python27}:
+{lib, mkCoqDerivation, coq, python27, version ? null }:
 
-stdenv.mkDerivation rec {
+with lib; mkCoqDerivation rec {
+  pname = "fiat";
+  owner = "mit-plv";
+  repo = "fiat";
+  displayVersion = { fiat = v: "unstable-${v}"; };
+  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";
 
-  name = "coq-fiat-${coq.coq-version}-unstable-${version}";
-  version = "2016-10-24";
-
-  src = fetchgit {
-    url = "https://github.com/mit-plv/fiat.git";
-    rev = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a";
-    sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64";
-  };
-
-  buildInputs = [ coq python27 ] ++ (with coq.ocamlPackages; [ ocaml camlp5 ]);
+  mlPlugin = true;
+  extraBuildInputs = [ python27 ];
 
   prePatch = "patchShebangs etc/coq-scripts";
 
···
     cp -pR src/* $COQLIB/user-contrib/Fiat
   '';
 
-  meta = with stdenv.lib; {
+  meta = {
     homepage = "http://plv.csail.mit.edu/fiat/";
     description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications";
     maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: v == "8.5";
   };
 }

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

···
-{ stdenv, bash, which, autoconf, automake, fetchzip, coq }:
+{ lib, bash, which, autoconf, automake,
+  mkCoqDerivation, coq, version ? null }:
 
-let params =
-  if stdenv.lib.versionAtLeast coq.coq-version "8.7" then {
-    version = "3.3.1";
-    sha256 = "0k1nfgiszmai5dihhpfa5mgq9rwigl0n38dw10jn79x89xbdpyh5";
-  } else {
-    version = "2.6.1";
-    sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj";
-  }
-; in
+with lib; mkCoqDerivation {
+  pname = "flocq";
+  owner = "flocq";
+  domain = "gitlab.inria.fr";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.7";        out = "3.3.1"; }
+    { case = range "8.5" "8.8"; out = "2.6.1"; }
+  ] null;
+  release."3.3.1".sha256 = "1mk8adhi5hrllsr0hamzk91vf2405sjr4lh5brg9201mcw11abkz";
+  release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj";
+  releaseRev = v: "flocq-${v}";
 
-stdenv.mkDerivation rec {
+  nativeBuildInputs = [ bash which autoconf ];
+  mlPlugin = true;
+  useMelquiondRemake.logpath = "Flocq";
 
-  name = "coq${coq.coq-version}-flocq-${version}";
-  inherit (params) version;
-
-  src = fetchzip {
-    url = "https://gitlab.inria.fr/flocq/flocq/-/archive/flocq-${version}.tar.gz";
-    inherit (params) sha256;
-  };
-
-  nativeBuildInputs = [ bash which autoconf automake ];
-  buildInputs = [ coq ] ++ (with coq.ocamlPackages; [
-    ocaml camlp5
-  ]);
-
-  buildPhase = ''
-    ${bash}/bin/bash autogen.sh || autoconf
-    ${bash}/bin/bash configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Flocq
-    ./remake
-  '';
-
-  installPhase = ''
-    ./remake install
-  '';
-
-  meta = with stdenv.lib; {
-    homepage = "http://flocq.gforge.inria.fr/";
+  meta = {
     description = "A floating-point formalization for the Coq system";
     license = licenses.lgpl3;
     maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
   };
 }

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

···
-{ stdenv, fetchurl, which, coq, flocq }:
+{ which, lib, mkCoqDerivation, autoconf, coq, flocq, version ? null }:
 
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-gappalib-1.4.4";
-  src = fetchurl {
-    url = "https://gforge.inria.fr/frs/download.php/file/38338/gappalib-coq-1.4.4.tar.gz";
-    sha256 = "1ds9qp3ml07w5ali0rsczlwgdx4xcgasgbcnpi2lssgj1xpxgfpn";
-  };
+with lib; mkCoqDerivation {
+  pname = "gappalib";
+  repo = "coq";
+  owner = "gappa";
+  domain = "gitlab.inria.fr";
+  inherit version;
+  defaultVersion = if versions.isGe "8.8" coq.coq-version then "1.4.5" else null;
+  release."1.4.5".sha256 = "081hib1d9wfm29kis390qsqch8v6fs3q71g2rgbbzx5y5cf48n9k";
+  release."1.4.4".sha256 = "114q2hgw64j6kqa9mg3qcp1nlf0ia46z2xadq81fnkxqm856ml7l";
+  releaseRev = v: "gappalib-coq-${v}";
 
-  nativeBuildInputs = [ which ];
-  buildInputs = [ coq coq.ocamlPackages.ocaml ];
+  nativeBuildInputs = [ which autoconf ];
+  mlPlugin = true;
   propagatedBuildInputs = [ flocq ];
-
-  configurePhase = "./configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Gappa";
-  buildPhase = "./remake";
-  installPhase = "./remake install";
+  useMelquiondRemake.logpath = "Gappa";
 
   meta = {
     description = "Coq support library for Gappa";
-    license = stdenv.lib.licenses.lgpl21;
-    homepage = "http://gappa.gforge.inria.fr/";
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
-    inherit (coq.meta) platforms;
+    license = licenses.lgpl21;
+    maintainers = [ maintainers.vbgl ];
   };
-
-  passthru = {
-    compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.8" "8.9" "8.10" "8.11" "8.12" ];
-  };
-
 }

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

···
-{stdenv, fetchurl, coq, unzip}:
-
-stdenv.mkDerivation rec {
+{lib, fetchzip, mkCoqDerivation, coq, version ? null }:
 
-  name = "coq-heq-${coq.coq-version}-${version}";
-  version = "0.92";
+with lib; mkCoqDerivation {
+  pname = "heq";
+  repo = "Heq";
+  owner = "gil";
+  domain = "mpi-sws.org";
+  inherit version fetcher;
+  defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null;
+  release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74";
 
-  src = fetchurl {
-    url = "https://www.mpi-sws.org/~gil/Heq/download/Heq-${version}.zip";
-    sha256 = "03y71c4qs6cmy3s2hjs05g7pcgk9sqma6flj15394yyxbvr9is1p";
-  };
-
-  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 unzip ];
+  mlPlugin = true;
   propagatedBuildInputs = [ coq ];
 
+  extraInstallFlags = [ "COQLIB=$out/lib/coq/${coq.coq-version}" ];
   preBuild = "cd src";
 
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}" ];
-
-  meta = with stdenv.lib; {
+  meta = {
     homepage = "https://www.mpi-sws.org/~gil/Heq/";
     description = "Heq : a Coq library for Heterogeneous Equality";
     maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: !stdenv.lib.versionAtLeast v "8.8";
   };
 }

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

···
-{ stdenv, fetchFromGitHub, which, coq, coq-elpi }:
+{ lib, mkCoqDerivation, which, coq, coq-elpi, version ? null }:
 
-let
-  versions = {
-      "0.10.0" =  {
-        rev = "v0.10.0";
-        sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
-      };
-  };
-  version = x: versions.${x} // {version = x;};
-  params = {
-   "8.11" = version "0.10.0";
-   "8.12" = version "0.10.0";
-  };
-  param = params.${coq.coq-version};
-in
-
-stdenv.mkDerivation rec {
-  name = "coq${coq.coq-version}-hierarchy-builder-${param.version}";
-
-  src = fetchFromGitHub {
-    owner = "math-comp";
-    repo = "hierarchy-builder";
-    inherit (param) rev sha256;
-  };
+with lib; mkCoqDerivation {
+  pname = "hierarchy-builder";
+  owner = "math-comp";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.12";         out = "1.0.0"; }
+    { case = range "8.11" "8.12"; out = "0.10.0"; }
+  ] null;
+  release."1.0.0".sha256  = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
+  release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
+  releaseRev = v: "v${v}";
 
   propagatedBuildInputs = [ coq-elpi ];
-  buildInputs = [ coq coq.ocaml coq.ocamlPackages.elpi ];
 
-  installPhase = ''make -f Makefile.coq VFILES=structures.v COQLIB=$out/lib/coq/${coq.coq-version}/ install'';
+  extraInstallFlags = [ "VFILES=structures.v" ];
 
   meta = {
     description = "Coq plugin embedding ELPI.";
-    maintainers = [ stdenv.lib.maintainers.cohencyril ];
-    license = stdenv.lib.licenses.lgpl21;
-    inherit (coq.meta) platforms;
-    inherit (src.meta) homepage;
-  };
-
-  passthru = {
-    compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params;
+    maintainers = [ maintainers.cohencyril ];
+    license = licenses.lgpl21;
   };
 }

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

···
-{ stdenv, fetchurl, which, coq, coquelicot, flocq, mathcomp
-, bignums ? null }:
+{ lib, mkCoqDerivation, which, autoconf
+, coq, coquelicot, flocq, mathcomp
+, bignums ? null, version ? null }:
 
-let params =
-  let
-  v3_3 = {
-    version = "3.3.0";
-    uid = "37077";
-    sha256 = "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903";
-  };
-  v3_4 = {
-    version = "3.4.2";
-    uid = "38288";
-    sha256 = "00bgzbji0gkazwxhs4q8gz4ccqsa1y1r0m0ravr18ps2h8a8qva5";
-  };
-  v4_0 = {
-    version = "4.0.0";
-    uid = "38339";
-    sha256 = "19sbrv7jnzyxji7irfslhr9ralc0q3gx20nymig5vqbn3vssmgpz";
-  };
-  in {
-    "8.5" = v3_3;
-    "8.6" = v3_3;
-    "8.7" = v3_4;
-    "8.8" = v4_0;
-    "8.9" = v4_0;
-    "8.10" = v4_0;
-    "8.11" = v4_0;
-    "8.12" = v4_0;
-  };
-  param = params."${coq.coq-version}";
-in
+with lib; mkCoqDerivation {
+  pname = "interval";
+  owner = "coqinterval";
+  domain = "gitlab.inria.fr";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.8" ;        out = "4.1.0"; }
+    { case = range "8.8" "8.12"; out = "4.0.0"; }
+    { case = range "8.7" "8.11"; out = "3.4.2"; }
+    { case = range "8.5" "8.6";  out = "3.3.0"; }
+  ] null;
+  release."4.1.0".sha256 = "1jv27n5c4f3a9d8sizraa920iqi35x8cik8lm7pjp1dkiifz47nb";
+  release."4.0.0".sha256 = "1hhih6zmid610l6c8z3x4yzdzw9jniyjiknd1vpkyb2rxvqm3gzp";
+  release."3.4.2".sha256 = "07ngix32qarl3pjnm9d0vqc9fdrgm08gy7zp306hwxjyq7h1v7z0";
+  release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz";
+  releaseRev = v: "interval-${v}";
 
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-interval-${param.version}";
-
-  src = fetchurl {
-    url = "https://gforge.inria.fr/frs/download.php/file/${param.uid}/interval-${param.version}.tar.gz";
-    inherit (param) sha256;
-  };
-
-  nativeBuildInputs = [ which ];
-  buildInputs = [ coq ];
+  nativeBuildInputs = [ which autoconf ];
   propagatedBuildInputs = [ bignums coquelicot flocq ];
-
-  configurePhase = "./configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Interval";
-  buildPhase = "./remake";
-  installPhase = "./remake install";
+  useMelquiondRemake.logpath = "Interval";
 
-  meta = with stdenv.lib; {
-    homepage = "http://coq-interval.gforge.inria.fr/";
+  meta = with lib; {
     description = "Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant";
     license = licenses.cecill-c;
     maintainers = with maintainers; [ vbgl ];
-    platforms = coq.meta.platforms;
   };
-
-  passthru = {
-    compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params;
-  };
-
 }

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

···
-{ stdenv, fetchFromGitLab, coq, stdpp }:
+{ lib, mkCoqDerivation, coq, stdpp, version ? null }:
 
-stdenv.mkDerivation rec {
-  version = "3.3.0";
-  name = "coq${coq.coq-version}-iris-${version}";
-  src = fetchFromGitLab {
-    domain = "gitlab.mpi-sws.org";
-    owner = "iris";
-    repo = "iris";
-    rev = "iris-${version}";
-    sha256 = "0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp";
-  };
+with lib; mkCoqDerivation rec {
+  pname = "iris";
+  domain = "gitlab.mpi-sws.org";
+  owner = "iris";
+  inherit version;
+  defaultVersion = if versions.range "8.9" "8.12" coq.coq-version then "3.3.0" else null;
+  release."3.3.0".sha256 = "0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp";
+  releaseRev = v: "iris-${v}";
 
-  buildInputs = [ coq ];
   propagatedBuildInputs = [ stdpp ];
 
-  enableParallelBuilding = true;
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
   meta = {
-    homepage = "https://gitlab.mpi-sws.org/FP/iris-coq";
     description = "The Coq development of the Iris Project";
-    inherit (coq.meta) platforms;
-    license = stdenv.lib.licenses.bsd3;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
+    license = licenses.bsd3;
+    maintainers = [ maintainers.vbgl ];
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.9" "8.10" "8.11" "8.12" ];
-  };
-
 }

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

···
-{ stdenv, fetchFromGitHub, which, coq }:
+{ lib, mkCoqDerivation, which, coq, version ? null }:
 
-let params = {
-  "8.7" = {
-    version = "0.1";
-    rev = "v0.1-8.7";
-    sha256 = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0";
-  };
-  "8.8" = {
-    version = "0.1";
-    rev = "0.1";
-    sha256 = "1zz26cyv99whj7rrpgnhhm9dfqnpmrx5pqizn8ihf8jkq8d4drz7";
-  };
-  "8.9" = rec {
-    version = "0.2";
-    rev = version;
-    sha256 = "0xby1kb26r9gcvk5511wqj05fqm9paynwfxlfqkmwkgnfmzk0x73";
-  };
-  "8.10" = rec {
-    version = "0.3";
-    rev = version;
-    sha256 = "0pzs5nsakh4l8ffwgn4ryxbnxdv2x0r1i7bc598ij621haxdirrr";
-  };
-};
-  param = params.${coq.coq-version};
-in
-
-stdenv.mkDerivation rec {
-  inherit (param) version;
-  name = "coq${coq.coq-version}-ltac2-${version}";
-
-  src = fetchFromGitHub {
-    owner = "coq";
-    repo = "ltac2";
-    inherit (param) rev sha256;
-  };
+with lib; mkCoqDerivation {
+  pname = "ltac2";
+  owner = "coq";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = "8.10"; out = "0.3"; }
+    { case = "8.9";  out = "0.2"; }
+    { case = "8.8";  out = "0.1"; }
+    { case = "8.7";  out = "0.1-8.7"; }
+  ] null;
+  release."0.3".sha256 = "0pzs5nsakh4l8ffwgn4ryxbnxdv2x0r1i7bc598ij621haxdirrr";
+  release."0.2".sha256 = "0xby1kb26r9gcvk5511wqj05fqm9paynwfxlfqkmwkgnfmzk0x73";
+  release."0.1".sha256 = "1zz26cyv99whj7rrpgnhhm9dfqnpmrx5pqizn8ihf8jkq8d4drz7";
+  release."0.1-8.7".version = "0.1";
+  release."0.1-8.7".rev     = "v0.1-8.7";
+  release."0.1-8.7".sha256  = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0";
 
   nativeBuildInputs = [ which ];
-  buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib ])
-  ++ stdenv.lib.optional (!stdenv.lib.versionAtLeast coq.coq-version "8.10")
-     coq.ocamlPackages.camlp5
-  ;
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+  mlPlugin = true;
 
   meta = {
     description = "A robust and expressive tactic language for Coq";
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
-    license = stdenv.lib.licenses.lgpl21;
-    inherit (coq.meta) platforms;
-    inherit (src.meta) homepage;
-  };
-
-  passthru = {
-    compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params;
+    maintainers = [ maintainers.vbgl ];
+    license = licenses.lgpl21;
   };
 }

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

···
-{ stdenv, fetchFromGitHub, coq, bignums }:
+{ lib, mkCoqDerivation, coq, bignums, version ? null }:
 
-stdenv.mkDerivation rec {
+with lib; mkCoqDerivation {
 
-  name = "coq${coq.coq-version}-math-classes-${version}";
-  version = "8.11.0";
+  pname = "math-classes";
+  inherit version;
+  defaultVersion = if versions.range "8.6" "8.11" coq.coq-version then "8.11.0" else null;
+  release."8.11.0".sha256 = "1hjgncvm1m46lw6264w4dqsy8dbh74vhmzq52x0fba2yqlvy94sf";
 
-  src = fetchFromGitHub {
-    owner = "coq-community";
-    repo = "math-classes";
-    rev = version;
-    sha256 = "1hjgncvm1m46lw6264w4dqsy8dbh74vhmzq52x0fba2yqlvy94sf";
-  };
+  extraBuildInputs = [ bignums ];
 
-  buildInputs = [ coq bignums ];
-  enableParallelBuilding = true;
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  meta = with stdenv.lib; {
+  meta = {
     homepage = "https://math-classes.github.io";
     description = "A library of abstract interfaces for mathematical structures in Coq.";
     maintainers = with maintainers; [ siddharthist jwiegley ];
-    platforms = coq.meta.platforms;
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" ];
-  };
-
 }

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

···
+{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, mathcomp-real-closed,
+  lib, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "analysis";
+  owner = "math-comp";
+
+  release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
+  release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
+
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+      { cases = [ (range "8.10" "8.11") "1.11.0" ];             out = "0.3.1"; }
+      { cases = [ (range "8.8"  "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; }
+    ] null;
+
+  propagatedBuildInputs =
+    [ mathcomp.ssreflect mathcomp.field
+      mathcomp-finmap mathcomp-bigenough mathcomp-real-closed ];
+
+  meta = {
+    description = "Analysis library compatible with Mathematical Components";
+    license = licenses.cecill-c;
+  };
+}

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

···
+{ coq, mkCoqDerivation, mathcomp, lib, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "bigenough";
+  owner = "math-comp";
+
+  release = { "1.0.0".sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg"; };
+  inherit version;
+  defaultVersion = "1.0.0";
+
+  propagatedBuildInputs = [ mathcomp.ssreflect ];
+
+  meta = {
+    description = "A small library to do epsilon - N reasonning";
+    license = licenses.cecill-b;
+  };
+}

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

···
+{ coq, mkCoqDerivation, mathcomp, lib, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "finmap";
+  owner = "math-comp";
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+      { cases = [ (isGe "8.10")          (range "1.11" "1.12") ]; out = "1.5.1"; }
+      { cases = [ (range "8.7" "8.11")   "1.11.0" ];              out = "1.5.0"; }
+      { cases = [ (isEq "8.11")          (range "1.8" "1.10") ];  out = "1.4.0+coq-8.11"; }
+      { cases = [ (range "8.7" "8.11.0") (range "1.8" "1.10") ];  out = "1.4.0"; }
+      { cases = [ (range "8.7" "8.11.0") (range "1.8" "1.10") ];  out = "1.3.4"; }
+      { cases = [ (range "8.7" "8.9")    "1.7.0" ];               out = "1.1.0"; }
+      { cases = [ (range "8.6" "8.7")    (range "1.6.1" "1.7") ]; out = "1.0.0"; }
+    ] null;
+  release = {
+    "1.5.1".sha256          = "0ryfml4pf1dfya16d8ma80favasmrygvspvb923n06kfw9v986j7";
+    "1.5.0".sha256          = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
+    "1.4.1".sha256          = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
+    "1.4.0+coq-8.11".sha256 = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
+    "1.4.0".sha256          = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
+    "1.3.4".sha256          = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
+    "1.2.1".sha256          = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
+    "1.1.0".sha256          = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
+    "1.0.0".sha256          = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
+  };
+
+  propagatedBuildInputs = [ mathcomp.ssreflect ];
+
+  meta = {
+    description = "A finset and finmap library";
+    license = licenses.cecill-b;
+  };
+}

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

···
+{ coq, mkCoqDerivation, mathcomp, mathcomp-bigenough,
+  lib, version ? null }:
+
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "real-closed";
+  owner = "math-comp";
+  inherit version;
+  release = {
+    "1.1.2".sha256 = "0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn";
+    "1.1.1".sha256 = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b";
+    "1.0.5".sha256 = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2";
+    "1.0.4".sha256 = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b";
+    "1.0.3".sha256 = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
+    "1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
+  };
+
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+      { cases = [ (isGe "8.10")  "1.12.0" ]; out = "1.1.2"; }
+      { cases = [ (isGe "8.7")   "1.11.0" ]; out = "1.1.1"; }
+      { cases = [ (isGe "8.7")   (range "1.9.0" "1.10.0") ]; out = "1.0.4"; }
+      { cases = [ (isGe "8.7")   "1.8.0"  ]; out = "1.0.3"; }
+      { cases = [ (isGe "8.7")   "1.7.0"  ]; out = "1.0.1"; }
+    ] null;
+
+  propagatedBuildInputs = [ mathcomp.ssreflect mathcomp.field mathcomp-bigenough ];
+
+  meta = {
+    description = "Mathematical Components Library on real closed fields";
+    license = licenses.cecill-c;
+  };
+}

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

···
-#############################
-# Main derivation: mathcomp #
-########################################################################
-# This file mainly provides the `mathcomp` derivation, which is        #
-# essentially a meta-package containing all core mathcomp libraries    #
-# (ssreflect fingroup algebra solvable field character). They can be   #
-# accessed individually through the paththrough attributes of mathcomp #
-# bearing the same names (mathcomp.ssreflect, etc).                    #
-#                                                                      #
-# Do not use overrideAttrs, but overrideMathcomp instead, which        #
-# regenerate a full mathcomp derivation with sub-derivations, and      #
-# behave the same as `mathcomp_`, described below.                     #
-########################################################################
+############################################################################
+# This file mainly provides the `mathcomp` derivation, which is            #
+# essentially a meta-package containing all core mathcomp libraries        #
+# (ssreflect fingroup algebra solvable field character). They can be       #
+# accessed individually through the passthrough attributes of mathcomp     #
+# bearing the same names (mathcomp.ssreflect, etc).                        #
+############################################################################
+# Compiling a custom version of mathcomp using `mathcomp.override`.        #
+# This is the replacement for the former `mathcomp_ config` function.      #
+# See the documentation at doc/languages-frameworks/coq.section.md.        #
+############################################################################
 
-############################################################
-# Compiling a custom version of mathcomp using `mathcomp_` #
-##############################################################################
-# The prefered way to compile a custom version of mathcomp (other than a     #
-# released version which should be added to `mathcomp-config-initial`        #
-# and pushed to nixpkgs), is to apply the function `coqPackages.mathcomp_`   #
-# to either:                                                                 #
-# - a string without slash, which is interpreted as a github revision,       #
-#   i.e. either a tag, a branch or a commit hash                             #
-# - a string with slashes "owner/p_1/.../p_n", which is interpreted as       #
-#   github owner "owner" and revision "p_1/.../p_n".                         #
-# - a path which is interpreted as a local source for the repository,        #
-#   the name of the version is taken to be the basename of the path          #
-#   i.e. if the path is /home/you/git/package/branch/,                       #
-#        then "branch" is the name of the version                            #
-# - an attribute set which overrides some attributes (e.g. the src)          #
-#   if the version is updated, the name is automatically regenerated using   #
-#   the conventional schema "coq${coq.coq-version}-${pkgname}-${version}"    #
-# - a "standard" override function (old: new_attrs) to override the default  #
-#   attribute set, so that you can use old.${field} to patch the derivation. #
-##############################################################################
-
-#########################################################################
-# Example of use: https://github.com/math-comp/math-comp/wiki/Using-nix #
-#########################################################################
-
-#################################
-# Adding a new mathcomp version #
-#############################################################################
-# When adding a new version of mathcomp, add an attribute to `sha256` (use  #
-# ```sh                                                                     #
-# nix-prefetch-url --unpack                                                 #
-# https://github.com/math-comp/math-comp/archive/version.tar.gz             #
-# ```                                                                       #
-# to get the corresponding `sha256`) and to `coq-version` (read the release #
-# notes to check which versions of coq it is compatible with). Then add     #
-# it in `preference version`, if not all mathcomp-extra packages are        #
-# ready, you might want to give new release secondary priority.             #
-#############################################################################
-
-
-{ stdenv, fetchFromGitHub, ncurses, which, graphviz,
-  recurseIntoAttrs, withDoc ? false,
-  coqPackages,
-  mathcomp_, mathcomp, mathcomp-config,
-}:
-with builtins // stdenv.lib;
+{ lib, ncurses, which, graphviz, lua,
+  mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false,
+  coqPackages, coq, ocamlPackages, version ? null }@args:
+with builtins // lib;
 let
-  mathcomp-config-initial = rec {
-  #######################################################################
-  # CONFIGURATION (please edit this), it is exported as mathcomp-config #
-  #######################################################################
-    # sha256 of released mathcomp versions
-    sha256 = {
-      "1.12.0"       = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
-      "1.11.0"       = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
-      "1.11+beta1"   = "12i3zznwajlihzpqsiqniv20rklj8d8401lhd241xy4s21fxkkjm";
-      "1.10.0"       = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
-      "1.9.0"        = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
-      "1.8.0"        = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
-      "1.7.0"        = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
-      "1.6.1"        = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
-    };
-    # versions of coq compatible with released mathcomp versions
-    coq-versions     = {
-      "1.12.0"       = flip elem [ "8.13" ];
-      "1.11.0"       = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
-      "1.11+beta1"   = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
-      "1.10.0"       = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ];
-      "1.9.0"        = flip elem [ "8.7" "8.8" "8.9" "8.10" ];
-      "1.8.0"        = flip elem [ "8.7" "8.8" "8.9" ];
-      "1.7.0"        = flip elem [ "8.6" "8.7" "8.8" "8.9" ];
-      "1.6.1"        = flip elem [ "8.5"];
-    };
-
-    # sets the default version of mathcomp given a version of Coq
-    # this is currently computed using version-perference below
-    # but it can be set to a fixed version number
-    preferred-version = let v = head (
-      filter (mc: mathcomp-config.coq-versions.${mc} coq.coq-version)
-        mathcomp-config.version-preferences ++ ["0.0.0"]);
-     in if v == "0.0.0" then head mathcomp-config.version-preferences else v;
-
-    # mathcomp preferred versions by decreasing order
-    # (the first version in the list will be tried first)
-    version-preferences =
-      [ "1.12.0" "1.10.0" "1.11.0" "1.9.0" "1.8.0" "1.7.0" "1.6.1" ];
-
-    # list of core mathcomp packages sorted by dependency order
-    packages = _version: # unused in current versions of mathcomp
-      # because the following list of packages is fixed for
-      # all versions of mathcomp up to 1.11.0
-      [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
-
-    # compute the dependencies of the core package pkg
-    # (assuming the total ordering above, change if necessary)
-    deps = version: pkg: if pkg == "single" then [] else
-      (pred-split-list (x: x == pkg) (mathcomp-config.packages version)).left;
-  };
-
-  ##############################################################
-  # COMPUTED using the configuration above (edit with caution) #
-  ##############################################################
-
-  # generic split function (TODO: move to lib?)
-  pred-split-list = pred: l:
-    let loop = v: l: if l == [] then {left = v; right = [];}
-      else let hd = builtins.head l; tl = builtins.tail l; in
-      if pred hd then {left = v; right = tl;} else loop (v ++ [hd]) tl;
-    in loop [] l;
-
-  pkgUp = l: r: l // r // {
-    meta     = (l.meta or {}) // (r.meta or {});
-    passthru = (l.passthru or {}) // (r.passthru or {});
+  repo  = "math-comp";
+  owner = "math-comp";
+  withDoc = single && (args.withDoc or false);
+  defaultVersion = with versions; switch coq.coq-version [
+      { case = isGe  "8.13";        out = "1.12.0"; } # lower version of coq to 8.10 when all mathcomp packages are ported
+      { case = range "8.7"  "8.12"; out = "1.11.0"; }
+      { case = range "8.7" "8.11";  out = "1.10.0"; }
+      { case = range "8.7" "8.11";  out = "1.9.0";  }
+      { case = range "8.7" "8.9";   out = "1.8.0";  }
+      { case = range "8.6" "8.9";   out = "1.7.0";  }
+      { case = range "8.5" "8.7";   out = "1.6.4";  }
+    ] null;
+  release = {
+    "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
+    "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
+    "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
+    "1.9.0".sha256  = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
+    "1.8.0".sha256  = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
+    "1.7.0".sha256  = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
+    "1.6.4".sha256  = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz";
+    "1.6.1".sha256  = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
   };
+  releaseRev = v: "mathcomp-${v}";
 
-  coq = coqPackages.coq;
-  mathcomp-deps = mathcomp-config.deps mathcomp.config.preferred-version;
+  # list of core mathcomp packages sorted by dependency order
+  packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
 
-  # default set of attributes given a 'package' name.
-  # this attribute set will be extended using toOverrideFun
-  default-attrs = package:
-    let
+  mathcomp_ = package: let
+      mathcomp-deps = if package == "single" then []
+        else map mathcomp_ (head (splitList (pred.equal package) packages));
       pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
-      pkgname = if package == "single" then "mathcomp" else "mathcomp-${package}";
+      pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
       pkgallMake = ''
         echo "all.v"  > Make
         echo "-I ." >>   Make
         echo "-R . mathcomp.all" >> Make
       '';
-    in
-      rec {
-        version = "master";
-        name = "coq${coq.coq-version}-${pkgname}-${version}";
+      derivation = mkCoqDerivation ({
+        inherit version pname defaultVersion release releaseRev repo owner;
 
-        nativeBuildInputs = optionals withDoc [ graphviz ];
-        buildInputs = [ ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
-        propagatedBuildInputs = [ coq ];
-        enableParallelBuilding = true;
+        nativeBuildInputs = optional withDoc graphviz;
+        mlPlugin = versions.isLe "8.6" coq.coq-version;
+        extraBuildInputs = [ ncurses which ] ++ optional withDoc lua;
+        propagatedBuildInputs = mathcomp-deps;
 
         buildFlags = optional withDoc "doc";
 
-        COQBIN = "${coq}/bin/";
-
         preBuild = ''
           patchShebangs etc/utils/ssrcoqdep || true
+        '' + ''
           cd ${pkgpath}
         '' + optionalString (package == "all") pkgallMake;
 
-        installPhase = ''
-          make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
-        '' + optionalString withDoc ''
-          make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/
-        '';
+        installTargets = "install" + optionalString withDoc " doc";
 
-        meta = with stdenv.lib; {
+        meta = {
           homepage    = "https://math-comp.github.io/";
           license     = licenses.cecill-b;
-          maintainers = [ maintainers.vbgl maintainers.jwiegley maintainers.cohencyril ];
-          platforms   = coq.meta.platforms;
-        };
-
-        passthru = {
-          mathcompDeps = mathcomp-deps package;
-          inherit package mathcomp-config;
-          compatibleCoqVersions = _: true;
-        };
-      };
-
-  # converts a string, path or attribute set into an override function
-  toOverrideFun = overrides:
-    if isFunction overrides then overrides else old:
-      let
-          pkgname = if old.passthru.package == "single" then "mathcomp"
-                    else "mathcomp-${old.passthru.package}";
-
-          string-attrs = if hasAttr overrides mathcomp-config.sha256 then
-                let version = overrides;
-                in {
-                  inherit version;
-                  src = fetchFromGitHub {
-                    owner  = "math-comp";
-                    repo   = "math-comp";
-                    rev    = "mathcomp-${version}";
-                    sha256 = mathcomp-config.sha256.${version};
-                  };
-                  passthru = old.passthru // {
-                    compatibleCoqVersions = mathcomp-config.coq-versions.${version};
-                    mathcompDeps = mathcomp-config.deps version old.passthru.package;
-                  };
-                }
-              else
-                let splitted = filter isString (split "/" overrides);
-                    owner    = head splitted;
-                    ref      = concatStringsSep "/" (tail splitted);
-                    version  = head (reverseList splitted);
-                in if length splitted == 1 then {
-                  inherit version;
-                  src = fetchTarball "https://github.com/math-comp/math-comp/archive/${version}.tar.gz";
-                } else {
-                  inherit version;
-                  src = fetchTarball "https://github.com/${owner}/math-comp/archive/${ref}.tar.gz";
-                };
-
-          attrs =
-            if overrides == null || overrides == "" then _: {}
-            else  if isString overrides then string-attrs
-            else  if isPath overrides then { version = baseNameOf overrides; src = overrides; }
-            else  if isAttrs overrides then pkgUp old overrides
-            else  let overridesStr = toString overrides; in
-                  abort "${overridesStr} not a legitimate overrides";
-      in
-        attrs // (if attrs?version && ! (attrs?name)
-                  then { name = "coq${coq.coq-version}-${pkgname}-${attrs.version}"; } else {});
-
-  # generates {ssreflect = «derivation ...» ; ... ; character = «derivation ...», ...}
-  mkMathcompGenSet = pkgs: o:
-    fold (pkg: pkgs: pkgs // {${pkg} = mkMathcompGen pkg o;}) {} pkgs;
-  # generates the derivation of one mathcomp package.
-  mkMathcompGen = package: overrides:
-    let
-      up = x: o: x // (toOverrideFun o x);
-      fixdeps = attrs:
-        let version = attrs.version or "master";
-            mcdeps  = if package == "single" then {}
-                      else mkMathcompGenSet (filter isString attrs.passthru.mathcompDeps) overrides;
-            allmc   = mkMathcompGenSet (mathcomp-config.packages version ++ [ "single" ]) overrides;
-        in {
-          propagatedBuildInputs = [ coq ]
-                                  ++ filter isDerivation attrs.passthru.mathcompDeps
-                                  ++ attrValues mcdeps
-          ;
-          passthru = allmc //
-                     { overrideMathcomp = o: mathcomp_ (old: up (up old overrides) o); };
+          maintainers = with maintainers; [ vbgl jwiegley cohencyril ];
         };
-    in
-      stdenv.mkDerivation (up (up (default-attrs package) overrides) fixdeps);
+      } // optionalAttrs (package != "single") { passthru = genAttrs packages mathcomp_; });
+    patched-derivation1 = derivation.overrideAttrs (o:
+      optionalAttrs (o.pname != null && o.pname == "mathcomp-all" &&
+         o.version != null && o.version != "dev" && versions.isLt "1.7" o.version)
+      { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; }
+    );
+    patched-derivation = patched-derivation1.overrideAttrs (o:
+      optionalAttrs (versions.isLe "8.7" coq.coq-version ||
+            (o.version != "dev" && versions.isLe "1.7" o.version))
+      {
+        installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
+      }
+    );
+    in patched-derivation;
 in
-{
-  mathcomp-config    = mathcomp-config-initial;
-  mathcomp_          = mkMathcompGen "all";
-  mathcomp           = mathcomp_ mathcomp-config.preferred-version;
-  # mathcomp-single    = mathcomp.single;
-  ssreflect          = mathcomp.ssreflect;
-  mathcomp-ssreflect = mathcomp.ssreflect;
-  mathcomp-fingroup  = mathcomp.fingroup;
-  mathcomp-algebra   = mathcomp.algebra;
-  mathcomp-solvable  = mathcomp.solvable;
-  mathcomp-field     = mathcomp.field;
-  mathcomp-character = mathcomp.character;
-}
+mathcomp_ (if single then "single" else "all")

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

···
-##########################################################
-# Main derivation:                                       #
-#   mathcomp-finmap mathcomp-analysis mathcomp-bigenough #
-#   mathcomp-multinomials mathcomp-real-closed coqeal    #
-# Additionally:                                          #
-#   mathcomp-extra-all  contains all the extra packages  #
-#   mathcomp-extra-fast contains the one not marked slow #
-########################################################################
-# This file mainly provides the above derivations, which are packages  #
-# extra mathcomp libraries based on mathcomp.                          #
-########################################################################
-
-#####################################################
-# Compiling customs versions using `mathcomp-extra` #
-##############################################################################
-# The prefered way to compile a custom version of mathcomp extra packages    #
-# (other than released versions which should be added to                     #
-# `rec-mathcomp-extra-config` and pushed to nixpkgs, see below),             #
-# is to use `coqPackages.mathcomp-extra name version` where                  #
-# 1. `name` is a string representing the name of a declared package          #
-#    OR undeclared package.                                                  #
-# 2. `version` is either:                                                    #
-# - a string without slash, which is interpreted as a github revision,       #
-#   i.e. either a tag, a branch or a commit hash                             #
-# - a string with slashes "owner/p_1/.../p_n", which is interpreted as       #
-#   github owner "owner" and revision "p_1/.../p_n".                         #
-# - a path which is interpreted as a local source for the repository,        #
-#   the name of the version is taken to be the basename of the path          #
-#   i.e. if the path is /home/you/git/package/branch/,                       #
-#        then "branch" is the name of the version                            #
-# - an attribute set which overrides some attributes (e.g. the src)          #
-#   if the version is updated, the name is automatically regenerated using   #
-#   the conventional schema "coq${coq.coq-version}-${pkgname}-${version}"    #
-# - a "standard" override function (old: new_attrs) to override the default  #
-#   attribute set, so that you can use old.${field} to patch the derivation. #
-#                                                                            #
-# Should you choose to use `pkg.overrideAttrs` instead, we provide the       #
-# function mathcomp-extra-override which takes a name and a version exactly  #
-# as above and returns an override function.                                 #
-##############################################################################
-
-#########################################################################
-# Example of use: https://github.com/math-comp/math-comp/wiki/Using-nix #
-#########################################################################
-
-###########################################
-# Adding a new package or package version #
-################################################################################
-# 1. Update or add a `package` entry to `initial`, it must be a function       #
-#    taking the version as argument and returning an attribute set. Everything #
-#    is optional and the default for the sources of the repository and the     #
-#    homepage will be https://github.com/math-comp/${package}.                 #
-#                                                                              #
-# 2. Update or add a `package` entry to `sha256` for each release.             #
-#    You may use                                                               #
-#    ```sh                                                                     #
-#    nix-prefetch-url --unpack                                                 #
-#    https://github.com/math-comp/math-comp/archive/version.tar.gz             #
-#    ```                                                                       #
-#                                                                              #
-# 3. Update or create a new consistent set of extra packages.                  #
-#    /!\ They must all be co-compatible. /!\                                   #
-#    Do not use versions that may disappear: it must either be                 #
-#    - a tag from the main repository (e.g. version or tag), or                #
-#    - a revision hash that has been *merged in master*                        #
-################################################################################
-
-{ stdenv, fetchFromGitHub, recurseIntoAttrs,
-  which, mathcomp, coqPackages,
-  mathcomp-extra-config, mathcomp-extra-override,
-  mathcomp-extra, current-mathcomp-extra,
-}:
-with builtins // stdenv.lib;
-let
-  ##############################
-  # CONFIGURATION, please edit #
-  ##############################
-  ############################
-  # Packages base delaration #
-  ############################
-  rec-mathcomp-extra-config = {
-    initial = {
-      mathcomp-finmap = {version, coqPackages}: {
-        meta = {
-          description = "A finset and finmap library";
-          repo = "finmap";
-          homepage = "https://github.com/math-comp/finmap";
-        };
-        passthru.compatibleCoqVersions = flip elem [ "8.8" "8.9" "8.10" "8.11" ];
-      };
-
-      mathcomp-bigenough = {version, coqPackages}: {
-        meta = {
-          description = "A small library to do epsilon - N reasonning";
-          repo = "bigenough";
-          homepage = "https://github.com/math-comp/bigenough";
-        };
-        passthru.compatibleCoqVersions = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ];
-      };
-
-      multinomials = {version, coqPackages}: {
-        buildInputs = [ which ];
-        propagatedBuildInputs = with coqPackages;
-          [ mathcomp.algebra mathcomp-finmap mathcomp-bigenough ];
-        meta = {
-          description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
-          repo = "multinomials";
-          homepage = "https://github.com/math-comp/multinomials";
-        };
-        passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ];
-      };
-
-      mathcomp-analysis = {version, coqPackages}: {
-        propagatedBuildInputs = with coqPackages;
-          [ mathcomp.field mathcomp-finmap mathcomp-bigenough mathcomp-real-closed ];
-        meta = {
-          description = "Analysis library compatible with Mathematical Components";
-          homepage = "https://github.com/math-comp/analysis";
-          repo = "analysis";
-          license = stdenv.lib.licenses.cecill-c;
-        };
-        passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ];
-      };
-
-      mathcomp-real-closed = {version, coqPackages}: {
-        propagatedBuildInputs = with coqPackages;
-          [ mathcomp.field mathcomp-bigenough ];
-        meta = {
-          description = "Mathematical Components Library on real closed fields";
-          repo = "real-closed";
-          homepage = "https://github.com/math-comp/real-closed";
-        };
-        passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ];
-      };
-
-      coqeal = {version, coqPackages}: {
-        buildInputs = [ which ];
-        propagatedBuildInputs = with coqPackages;
-          [ mathcomp-algebra bignums paramcoq multinomials ];
-        meta = {
-          description = "CoqEAL - The Coq Effective Algebra Library";
-          homepage = "https://github.com/coqeal/coqeal";
-          license = stdenv.lib.licenses.mit;
-          owner = "CoqEAL";
-        };
-        passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ];
-      };
-    };
-
-    ###############################
-    # sha256 of released versions #
-    ###############################
-    sha256 = {
-      mathcomp-finmap = {
-        "1.5.0"          = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
-        "1.4.1"          = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
-        "1.4.0+coq-8.11" = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
-        "1.4.0"          = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
-        "1.3.4"          = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
-        "1.3.3"          = "1n844zjhv354kp4g4pfbajix0plqh7yxv6471sgyb46885298am5";
-        "1.3.1"          = "14rvm0rm5hd3pd0srgak3jqmddzfv6n7gdpjwhady5xcgrc7gsx7";
-        "1.2.1"          = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
-        "1.2.0"          = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4";
-        "1.1.0"          = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
-        "1.0.0"          = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
-      };
-      mathcomp-bigenough = {
-        "1.0.0" = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
-      };
-      mathcomp-analysis = {
-        "0.3.1" = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
-        "0.3.0" = "03klwi4fja0cqb4myp3kgycfbmdv00bznmxf8yg3zzzzw997hjqc";
-        "0.2.3" = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
-        "0.2.2" = "1d5dwg9di2ppdzfg21zr0a691zigb5kz0lcw263jpyli1nrq7cvk";
-        "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd";
-        "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al";
-      };
-      multinomials = {
-        "1.5.2" = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s";
-        "1.5.1" = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3";
-        "1.5"   = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw";
-        "1.4"   = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p";
-        "1.3"   = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4";
-        "1.2"   = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
-        "1.1"   = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
-        "1.0"   = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
-      };
-      mathcomp-real-closed = {
-        "1.1.1" = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b";
-        "1.1.0" = "0zgfmrlximw77bw5w6w0xg2nampp02pmrwnrzx8m1n5pqljnv8fh";
-        "1.0.5" = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2";
-        "1.0.4" = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b";
-        "1.0.3" = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
-        "1.0.2" = "0097pafwlmzd0gyfs31bxpi1ih04i72nxhn99r93aj20mn7mcsgl";
-        "1.0.1" = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
-      };
-      coqeal = {
-        "1.0.4" = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk";
-        "1.0.3" = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
-        "1.0.2" = "1brmf3gj03iky1bcl3g9vx8vknny7xfvs0y2rfr85am0296sxsfj";
-        "1.0.1" = "19jhdrv2yp9ww0h8q73ihb2w1z3glz4waf2d2n45klafxckxi7bm";
-        "1.0.0" = "1had6f1n85lmh9x31avbmgl3m0rsiw9f8ma95qzk5b57fjg5k1ii";
-      };
-    };
-
-    ################################
-    # CONSISTENT sets of packages. #
-    ################################
-    for-coq-and-mc = let
-      v6 = {
-        mathcomp-finmap       = "1.5.0";
-        mathcomp-bigenough    = "1.0.0";
-        mathcomp-analysis     = "0.3.1";
-        multinomials          = "1.5.2";
-        mathcomp-real-closed  = "1.1.1";
-        coqeal                = "1.0.4";
-      };
-      v5 = {
-        mathcomp-finmap       = "1.5.0";
-        mathcomp-bigenough    = "1.0.0";
-        mathcomp-analysis     = "0.3.0";
-        multinomials          = "1.5.1";
-        mathcomp-real-closed  = "1.0.5";
-        coqeal                = "1.0.4";
-      };
-      v4 = v3 // { coqeal = "1.0.3"; };
-      v3 = {
-        mathcomp-finmap       = "1.4.0";
-        mathcomp-bigenough    = "1.0.0";
-        mathcomp-analysis     = "0.2.3";
-        multinomials          = "1.5";
-        mathcomp-real-closed  = "1.0.4";
-        coqeal                = "1.0.0";
-      };
-      v2 = {
-        mathcomp-finmap       = "1.3.4";
-        mathcomp-bigenough    = "1.0.0";
-        mathcomp-analysis     = "0.2.3";
-        multinomials          = "1.4";
-        mathcomp-real-closed  = "1.0.3";
-        coqeal                = "1.0.0";
-      };
-      v1 = {
-        mathcomp-finmap       = "1.1.0";
-        mathcomp-bigenough    = "1.0.0";
-        multinomials          = "1.1";
-        mathcomp-real-closed  = "1.0.1";
-        coqeal                = "1.0.0";
-      };
-    in
-      {
-        "8.11" = {
-          "1.11.0"     = v6;
-          "1.11+beta1" = v5;
-          "1.10.0"       = v4 // {mathcomp-finmap = "1.4.0+coq-8.11";};
-        };
-        "8.10" = {
-          "1.11.0"       = removeAttrs v6 ["coqeal"];
-          "1.11+beta1"   = removeAttrs v5 ["coqeal"];
-          "1.10.0"       = v4;
-          "1.9.0"        = removeAttrs v3 ["coqeal"];
-        };
-        "8.9" = {
-          "1.11.0"       = removeAttrs v6 ["mathcomp-analysis"];
-          "1.11+beta1"   = removeAttrs v5 ["mathcomp-analysis"];
-          "1.10.0"       = v4;
-          "1.9.0"        = removeAttrs v3 ["coqeal"];
-          "1.8.0"        = removeAttrs v2 ["coqeal"];
-        };
-        "8.8" = {
-          "1.11.0"       = removeAttrs v6 ["mathcomp-analysis"];
-          "1.11+beta1"   = removeAttrs v5 ["mathcomp-analysis"];
-          "1.10.0"       = removeAttrs v4 ["mathcomp-analysis"];
-          "1.9.0"        = removeAttrs v3 ["coqeal"];
-          "1.8.0"        = removeAttrs v2 ["coqeal"];
-          "1.7.0"        = removeAttrs v1 ["coqeal" "multinomials"];
-        };
-        "8.7" = {
-          "1.11.0"       = removeAttrs v6 ["mathcomp-analysis"];
-          "1.11+beta1"   = removeAttrs v5 ["mathcomp-analysis"];
-          "1.10.0"       = removeAttrs v4 ["mathcomp-analysis"];
-          "1.9.0"        = removeAttrs v3 ["coqeal" "mathcomp-analysis"];
-          "1.8.0"        = removeAttrs v2 ["coqeal" "mathcomp-analysis"];
-          "1.7.0"        = removeAttrs v1 ["coqeal" "multinomials"];
-        };
-      };
-  };
-
-  ##############################
-  # GENERATION, EDIT WITH CARE #
-  ##############################
-  coq = coqPackages.coq;
-
-  default-attrs = {
-    version = "master";
-    buildInputs = [];
-    propagatedBuildInputs = (with coqPackages; [ ssreflect ]);
-    installFlags = [ "-f" "Makefile.coq" "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-    meta = {
-      inherit (mathcomp.meta) platforms license;
-      owner = "math-comp";
-      maintainers = [ maintainers.vbgl maintainers.cohencyril ];
-    };
-    passthru.compatibleCoqVersions = (_: true);
-  };
-
-  pkgUp = recursiveUpdateUntil (path: l: r: !(isAttrs l && isAttrs r) || path == ["src"]);
-
-  # Fixes a partial attribute set using the configuration
-  # in the style of the above mathcomp-extra-config.initial,
-  # and generates a name according to the conventional naming scheme below
-  fix-attrs = pkgcfg:
-    let attrs = pkgUp default-attrs pkgcfg; in
-    pkgUp attrs (rec {
-      name = "coq${coq.coq-version}mathcomp${mathcomp.version}-${attrs.meta.repo or attrs.meta.package or "anonymous"}-${attrs.version}";
-      src = attrs.src or (fetchTarball "${meta.homepage}/archive/${attrs.version}.tar.gz");
-      meta = rec {
-        homepage = attrs.meta.homepage or attrs.src.meta.homepage or "https://github.com/${owner}/${repo}";
-        owner    = attrs.meta.owner or "math-comp";
-        repo     = attrs.meta.repo or attrs.meta.package or "math-comp-nix";
-      };
-    });
-
-  # Gets a version out of a string, path or attribute set.
-  getVersion = arg:
-    if isFunction arg then (arg {}).version
-    else  if arg == "" then "master"
-    else  if isDerivation arg then arg.drvAttrs.version or "master"
-    else  if isAttrs arg then arg.version or "master"
-    else  if isString arg then head (reverseList (split "/" arg))
-    else  if isPath arg   then (baseNameOf arg)
-    else "master";
-
-  # Converts a string, path or attribute set into an override function
-  # It tries to fill the `old` argument of the override function using
-  # `mathcomp-extra-config.initial` first and finishes with `fix-attrs`
-  rec-mathcomp-extra-override = generic: old: let
-    version = getVersion generic;
-    package = old.meta.package or "math-comp-nix";
-    cfg = pkgUp ((mathcomp-extra-config.initial.${package} or (_: {}))
-      { inherit version coqPackages; }) old
-          // { inherit version; };
-    fix = attrs: fix-attrs (pkgUp cfg attrs);
-  in
-    if isFunction generic then fix (generic cfg)
-    else  if generic == null || generic == "" then fix {}
-    else  if isDerivation generic then generic.drvAttrs
-    else  if isAttrs generic then fix generic
-    else  if generic == "broken" then fix { meta.broken = true; passthru.compatibleCoqVersions = _: false; }
-    else  let fixedcfg = fix cfg; in fixedcfg // (
-      if isString generic then
-        if (mathcomp-extra-config.sha256.${package} or {})?${generic} then {
-          src = fetchFromGitHub {
-            inherit (fixedcfg.meta) owner repo;
-            rev = version;
-            sha256 = mathcomp-extra-config.sha256.${package}.${version};
-          };
-        }
-        else  let splitted = filter isString (split "/" generic); in {
-        src = fetchTarball
-          ("https://github.com/" +
-           (if length splitted == 1 then "${fixedcfg.meta.owner}/${fixedcfg.meta.repo}/archive/${version}.tar.gz"
-            else "${head splitted}/${fixedcfg.meta.repo}/archive/${concatStringsSep "/" (tail splitted)}.tar.gz"));
-        }
-      else  if isPath generic then { src = generic; }
-      else abort "${toString generic} not a legitimate generic version/override");
-
-  # applies mathcomp-extra-config.for-coq-and-mc to the current mathcomp version
-  for-this = mathcomp-extra-config.for-coq-and-mc.${coq.coq-version}.${mathcomp.version} or {};
-
-  # specializes mathcomp-extra to the current mathcomp version.
-  rec-current-mathcomp-extra = package: mathcomp-extra package (for-this.${package} or {});
-in
-  {
-    mathcomp-extra-override = rec-mathcomp-extra-override;
-    mathcomp-extra-config   = rec-mathcomp-extra-config;
-    current-mathcomp-extra  = rec-current-mathcomp-extra;
-    mathcomp-extra          = package: version:
-      stdenv.mkDerivation (mathcomp-extra-override version {meta = {inherit package;};});
-
-    mathcomp-finmap       = current-mathcomp-extra "mathcomp-finmap";
-    mathcomp-analysis     = current-mathcomp-extra "mathcomp-analysis";
-    mathcomp-bigenough    = current-mathcomp-extra "mathcomp-bigenough";
-    multinomials          = current-mathcomp-extra "multinomials";
-    mathcomp-real-closed  = current-mathcomp-extra "mathcomp-real-closed";
-    coqeal                = current-mathcomp-extra "coqeal";
-
-    mathcomp-extra-fast    = map current-mathcomp-extra
-      (attrNames (filterAttrs (pkg: config: !(config?slow && config.slow)) for-this));
-    mathcomp-extra-all    = map current-mathcomp-extra (attrNames for-this);
-  }

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

···
-{ stdenv, fetchFromGitHub, coq }:
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-stdenv.mkDerivation rec {
-  name = "coq${coq.coq-version}-metalib-${version}";
-  version = "20200527";
-
-  src = fetchFromGitHub {
-    owner = "plclub";
-    repo = "metalib";
-    rev = "597fd7d0c93eb159274e84a39d554f10f1efccf8";
-    sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs";
-  };
+with lib; mkCoqDerivation {
+  pname = "metalib";
+  owner = "plclub";
+  inherit version;
+  defaultVersion = if versions.range "8.10" "8.12" coq.coq-version then "20200527" else null;
+  release."20200527".rev    = "597fd7d0c93eb159274e84a39d554f10f1efccf8";
+  release."20200527".sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs";
 
   sourceRoot = "source/Metalib";
-
-  buildInputs = [ coq ];
-
-  enableParallelBuilding = true;
-
   installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}";
 
-  meta = with stdenv.lib; {
-    homepage = "https://github.com/plclub/metalib";
+  meta = {
     license = licenses.mit;
     maintainers = [ maintainers.jwiegley ];
-    platforms = coq.meta.platforms;
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.10" "8.11" "8.12" ];
-  };
-
 }

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

···
+{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough,
+  lib, version ? null }:
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "multinomials";
+  owner = "math-comp";
+  inherit version;
+  defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
+      { cases = [ (range "8.7" "8.12")  "1.11.0" ];             out = "1.5.2"; }
+      { cases = [ (range "8.7" "8.11")  (range "1.8" "1.10") ]; out = "1.5.0"; }
+      { cases = [ (range "8.7" "8.10")  (range "1.8" "1.10") ]; out = "1.4"; }
+      { cases = [ "8.6"                 (range "1.6" "1.7") ];  out = "1.1"; }
+    ] null;
+  release = {
+    "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s";
+    "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3";
+    "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw";
+    "1.5.0".rev    = "1.5";
+    "1.4".sha256   = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p";
+    "1.3".sha256   = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4";
+    "1.2".sha256   = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
+    "1.1".sha256   = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
+    "1.0".sha256   = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
+  };
+
+  propagatedBuildInputs =
+    [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ];
+
+  meta = {
+    description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
+    license = licenses.cecill-c;
+  };
+}

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

···
-{stdenv, fetchFromGitHub, coq, unzip}:
-
-let
-  versions = {
-    pre_8_6 = rec {
-      rev = "v${version}";
-      version = "1.2.8";
-      sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb";
-    };
-    post_8_6 = rec {
-      rev = "v${version}";
-      version = "4.0.2";
-      sha256 = "1q96bsxclqx84xn5vkid501jkwlc1p6fhb8szrlrp82zglj58b0b";
-    };
-  };
-  params = {
-    "8.5" = versions.pre_8_6;
-    "8.6" = versions.post_8_6;
-    "8.7" = versions.post_8_6;
-    "8.8" = versions.post_8_6;
-    "8.9" = versions.post_8_6;
-    "8.10" = versions.post_8_6;
-    "8.11" = versions.post_8_6;
-    "8.12" = versions.post_8_6;
-  };
-  param = params.${coq.coq-version};
-in
-
-stdenv.mkDerivation rec {
-  inherit (param) version;
-  name = "coq${coq.coq-version}-paco-${version}";
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-  src = fetchFromGitHub {
-    inherit (param) rev sha256;
-    owner = "snu-sf";
-    repo = "paco";
-  };
-
-  buildInputs = [ coq ];
+with lib; mkCoqDerivation {
+  pname = "paco";
+  owner = "snu-sf";
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.6";         out = "4.0.2"; }
+    { case = range "8.5" "8.8";  out = "1.2.8"; }
+  ] null;
+  release."4.0.2".sha256 = "1q96bsxclqx84xn5vkid501jkwlc1p6fhb8szrlrp82zglj58b0b";
+  release."1.2.8".sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb";
+  releaseRev = v: "v${v}";
 
   preBuild = "cd src";
 
···
     cp -pR *.vo $COQLIB/user-contrib/Paco
   '';
 
-  meta = with stdenv.lib; {
+  meta = {
     homepage = "http://plv.mpi-sws.org/paco/";
     description = "A Coq library implementing parameterized coinduction";
     maintainers = with maintainers; [ jwiegley ptival ];
-    platforms = coq.meta.platforms;
   };
-
-  passthru = {
-    compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params;
-  };
-
 }

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

···
-{ stdenv, fetchFromGitHub, coq }:
-
-let params =
-  {
-    "8.7" = {
-      sha256 = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj";
-      buildInputs = [ coq.ocamlPackages.camlp5 ];
-    };
-    "8.8" = {
-      sha256 = "0rc4lshqvnfdsph98gnscvpmlirs9wx91qcvffggg73xw0p1g9s0";
-      buildInputs = [ coq.ocamlPackages.camlp5 ];
-    };
-    "8.9" = {
-      sha256 = "1jjzgpff09xjn9kgp7w69r096jkj0x2ksng3pawrmhmn7clwivbk";
-      buildInputs = [ coq.ocamlPackages.camlp5 ];
-    };
-    "8.10" = {
-      sha256 = "1lq1mw15w4yky79qg3rm0mpzqi2ir51b6ak04ismrdr7ixky49y8";
-    };
-    "8.11" = {
-      sha256 = "09c6813988nvq4fpa45s33k70plnhxsblhm7cxxkg0i37mhvigsa";
-    };
-    "8.12" = {
-      sha256 = "0qd72r45if4h7c256qdfiimv75zyrs0w0xqij3m866jxaq591v4i";
-    };
-  };
-  param = params.${coq.coq-version};
-in
-
-stdenv.mkDerivation rec {
-  version = "1.1.2";
-  name = "coq${coq.coq-version}-paramcoq-${version}";
-  src = fetchFromGitHub {
-    owner = "coq-community";
-    repo = "paramcoq";
-    rev = "v${version}+coq${coq.coq-version}";
-    inherit (param) sha256;
-  };
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-  buildInputs = [ coq ]
-  ++ (with coq.ocamlPackages; [ ocaml findlib ])
-  ++ (param.buildInputs or [])
-  ;
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v params;
-  };
-
+with lib; mkCoqDerivation {
+  pname = "paramcoq";
+  inherit version;
+  defaultVersion = if versions.range "8.7" "8.12" coq.coq-version
+    then "1.1.2+coq${coq.coq-version}" else null;
+  displayVersion = { paramcoq = "1.1.2"; };
+  release."1.1.2+coq8.12".sha256 = "0qd72r45if4h7c256qdfiimv75zyrs0w0xqij3m866jxaq591v4i";
+  release."1.1.2+coq8.11".sha256 = "09c6813988nvq4fpa45s33k70plnhxsblhm7cxxkg0i37mhvigsa";
+  release."1.1.2+coq8.10".sha256 = "1lq1mw15w4yky79qg3rm0mpzqi2ir51b6ak04ismrdr7ixky49y8";
+  release."1.1.2+coq8.9".sha256  = "1jjzgpff09xjn9kgp7w69r096jkj0x2ksng3pawrmhmn7clwivbk";
+  release."1.1.2+coq8.8".sha256  = "0rc4lshqvnfdsph98gnscvpmlirs9wx91qcvffggg73xw0p1g9s0";
+  release."1.1.2+coq8.7".sha256  = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj";
+  releaseRev = v: "v${v}";
+  mlPlugin = true;
   meta = {
     description = "Coq plugin for parametricity";
-    inherit (src.meta) homepage;
-    license = stdenv.lib.licenses.mit;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
-    inherit (coq.meta) platforms;
+    license = licenses.mit;
+    maintainers = [ maintainers.vbgl ];
   };
 }

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

···
-{ stdenv, fetchFromGitHub, coq, coq-ext-lib }:
+{ lib, mkCoqDerivation, coq, coq-ext-lib, version ? null }:
 
-stdenv.mkDerivation rec {
-  version = "1.3.0";
-  name = "coq${coq.coq-version}-simple-io-${version}";
-  src = fetchFromGitHub {
-    owner = "Lysxia";
-    repo = "coq-simple-io";
-    rev = version;
-    sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax";
-  };
-
-  buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml ocamlbuild ]);
-
+with lib; mkCoqDerivation {
+  pname = "simple-io";
+  owner = "Lysxia";
+  repo = "coq-simple-io";
+  inherit version;
+  defaultVersion = if versions.range "8.7" "8.12" coq.coq-version then "1.3.0" else null;
+  release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax";
+  extraBuildInputs = (with coq.ocamlPackages; [ ocaml ocamlbuild ]);
   propagatedBuildInputs = [ coq-ext-lib ];
 
   doCheck = true;
   checkTarget = "test";
 
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
   meta = {
     description = "Purely functional IO for Coq";
-    inherit (src.meta) homepage;
-    inherit (coq.meta) platforms;
-    license = stdenv.lib.licenses.mit;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
+    license = licenses.mit;
+    maintainers = [ maintainers.vbgl ];
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
-  };
-
 }

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

···
-{ stdenv, fetchFromGitLab, coq }:
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-stdenv.mkDerivation rec {
-  name = "coq${coq.coq-version}-stdpp-${version}";
-  version = "1.4.0";
-  src = fetchFromGitLab {
-    domain = "gitlab.mpi-sws.org";
-    owner = "iris";
-    repo = "stdpp";
-    rev = "coq-stdpp-${version}";
-    sha256 = "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r";
-  };
-
-  buildInputs = [ coq ];
-
-  enableParallelBuilding = true;
-
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+with lib; mkCoqDerivation rec {
+  pname = "stdpp";
+  inherit version;
+  domain = "gitlab.mpi-sws.org";
+  owner = "iris";
+  defaultVersion = if versions.range "8.8" "8.12" coq.coq-version then "1.4.0" else null;
+  release."1.4.0".sha256 = "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r";
+  releaseRev = v: "coq-stdpp-${v}";
 
   meta = {
-    inherit (src.meta) homepage;
     description = "An extended “Standard Library” for Coq";
-    inherit (coq.meta) platforms;
-    license = stdenv.lib.licenses.bsd3;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
+    license = licenses.bsd3;
+    maintainers = [ maintainers.vbgl ];
   };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.8" "8.9" "8.10" "8.11" "8.12" ];
-  };
-
 }

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

···
-{ stdenv, fetchurl, fetchFromGitHub, coq }:
-
-let params =
-  if stdenv.lib.versionAtLeast coq.coq-version "8.10"
-  then rec {
-    version = "20200328";
-    src = fetchFromGitHub {
-      owner = "charguer";
-      repo = "tlc";
-      rev = version;
-      sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx";
-    };
-  } else rec {
-    version = "20181116";
-    src = fetchurl {
-      url = "http://tlc.gforge.inria.fr/releases/tlc-${version}.tar.gz";
-      sha256 = "0iv6f6zmrv2lhq3xq57ipmw856ahsql754776ymv5wjm88ld63nm";
-    };
-  }
-; in
-
-stdenv.mkDerivation {
-  inherit (params) version src;
-  pname = "coq${coq.coq-version}-tlc";
+{ lib, mkCoqDerivation, coq, version ? null }:
 
-  buildInputs = [ coq ];
+with lib; mkCoqDerivation {
+  pname = "tlc";
+  owner = "charguer";
+  inherit version;
+  displayVersion = { tlc = false; };
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.10" "8.12"; out = "20200328"; }
+    { case = range "8.6"  "8.12"; out = "20181116"; }
+  ] null;
+  release."20200328".sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx";
+  release."20181116".sha256 = "032lrbkxqm9d3fhf6nv1kq2z0mqd3czv3ijlbsjwnfh12xck4vpl";
 
   installFlags = [ "CONTRIB=$(out)/lib/coq/${coq.coq-version}/user-contrib" ];
 
   meta = {
     homepage = "http://www.chargueraud.org/softs/tlc/";
     description = "A non-constructive library for Coq";
-    license = stdenv.lib.licenses.free;
-    maintainers = [ stdenv.lib.maintainers.vbgl ];
-    inherit (coq.meta) platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ];
+    license = licenses.free;
+    maintainers = [ maintainers.vbgl ];
   };
 }

pkgs/development/haskell-modules/configuration-common.nix

···
     sha256 = "0g2m0y46zr3xs9fswkm4h9adhsg6gzl5zwgidshsjh3k3rq4h7b1";
   });
 
+  # https://github.com/ekmett/half/issues/35
+  half = if pkgs.stdenv.isAarch64
+    then dontCheck super.half
+    else super.half;
+
   # 2020-11-19: Jailbreaking until: https://github.com/snapframework/heist/pull/124
   heist = doJailbreak super.heist;
 

pkgs/development/libraries/libbladeRF/default.nix

···
-{ stdenv, lib, fetchFromGitHub, pkg-config, cmake, git, doxygen, help2man, ncurses, tecla
+{ stdenv, lib, fetchFromGitHub, fetchpatch, pkg-config, cmake, git, doxygen, help2man, ncurses, tecla
 , libusb1, udev }:
 
 let
···
     rev = "libbladeRF_v${version}";
     sha256 = "0g89al4kwfbx1l3zjddgb9ay4mhr7zk0ndchca3sm1vq2j47nf4l";
   };
+
+  # This patch is required for version 2.2.1. As the patch is already part of
+  # upstream master, it will be incorporated into the next release. The patch
+  # fixes a (well-justified) compiler warning which breaks the build because
+  # we compile with -Werror.
+  patches = [ (fetchpatch {
+    url = "https://github.com/Nuand/bladeRF/commit/163425d48a3b7d8c100d7295220d3648c050d0dd.patch";
+    sha256 = "1swsymlyxm3yk2k8l71z1fv0a5k2rmab02f0c7xkrvk683mq6yxw";
+  }) ];
 
   nativeBuildInputs = [ cmake pkg-config git doxygen help2man ];
   # ncurses used due to https://github.com/Nuand/bladeRF/blob/ab4fc672c8bab4f8be34e8917d3f241b1d52d0b8/host/utilities/bladeRF-cli/CMakeLists.txt#L208

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

···
-{ lib, fetchzip, buildDunePackage, camlp5
+{ stdenv, lib, fetchzip, buildDunePackage, camlp5
 , ppxlib, ppx_deriving, re, perl, ncurses
+, version ? "1.12.0"
 }:
-
+with lib;
+let fetched = import ../../../build-support/coq/meta-fetch/default.nix
+  {inherit stdenv fetchzip; } ({
+    release."1.12.0".sha256 = "1agisdnaq9wrw3r73xz14yrq3wx742i6j8i5icjagqk0ypmly2is";
+    release."1.11.4".sha256 = "1m0jk9swcs3jcrw5yyw5343v8mgax238cjb03s8gc4wipw1fn9f5";
+    releaseRev = v: "v${v}";
+    location = { domain = "github.com"; owner = "LPCIC"; repo = "elpi"; };
+  }) version;
+in
 buildDunePackage rec {
   pname = "elpi";
-  version = "1.11.4";
-
-   src = fetchzip {
-     url = "https://github.com/LPCIC/elpi/releases/download/v${version}/elpi-v${version}.tbz";
-     sha256 = "1hmjp2z52j17vwhhdkj45n9jx11jxkdg2dwa0n04yyw0qqy4m7c1";
-   };
+  inherit (fetched) version src;
 
   minimumOCamlVersion = "4.04";
 
···
 
   meta = {
     description = "Embeddable λProlog Interpreter";
-    license = lib.licenses.lgpl21Plus;
-    maintainers = [ lib.maintainers.vbgl ];
+    license = licenses.lgpl21Plus;
+    maintainers = [ maintainers.vbgl ];
     homepage = "https://github.com/LPCIC/elpi";
   };
 

pkgs/development/python-modules/apprise/default.nix

···
-{ lib, buildPythonPackage, fetchPypi
+{ lib, buildPythonPackage, fetchPypi, installShellFiles
 , Babel, requests, requests_oauthlib, six, click, markdown, pyyaml
-, pytestrunner, coverage, flake8, mock, pytest, pytestcov, tox, gntp, sleekxmpp
+, pytestrunner, coverage, flake8, mock, pytestCheckHook, pytestcov, tox, gntp, sleekxmpp
 }:
 
 buildPythonPackage rec {
   pname = "apprise";
-  version = "0.8.9";
+  version = "0.9.0";
 
   src = fetchPypi {
     inherit pname version;
-    sha256 = "024db00c6a80dbc8c9038b2de211c9fd32963046612882f3f54ad78930f3e0f7";
+    sha256 = "bab3563bc1e0c64938c4c7700112797bd99f20eb5d4a3e6038338bc8f060e153";
   };
 
-  nativeBuildInputs = [ Babel ];
+  nativeBuildInputs = [ Babel installShellFiles ];
 
   propagatedBuildInputs = [
     requests requests_oauthlib six click markdown pyyaml
   ];
 
   checkInputs = [
-    pytestrunner coverage flake8 mock pytest pytestcov tox gntp sleekxmpp
+    pytestrunner coverage flake8 mock pytestCheckHook pytestcov tox gntp sleekxmpp
   ];
+
+  disabledTests = [ "test_apprise_cli_nux_env"  ];
+
+  postInstall = ''
+    installManPage packaging/man/apprise.1
+  '';
 
   meta = with lib; {
     homepage = "https://github.com/caronc/apprise";

pkgs/development/python-modules/archinfo/default.nix

···
+{ lib
+, buildPythonPackage
+, fetchFromGitHub
+, pytestCheckHook
+, nose
+}:
+
+buildPythonPackage rec {
+  pname = "archinfo";
+  version = "9.0.5327";
+
+  src = fetchFromGitHub {
+    owner = "angr";
+    repo = pname;
+    rev = "v${version}";
+    sha256 = "0r7nj2hf51c954ihfxyhpbz1sd9lrc6i9zfkz11s22wpggvp06mz";
+  };
+
+  checkInputs = [
+    nose
+    pytestCheckHook
+  ];
+
+  pythonImportsCheck = [ "archinfo" ];
+
+  meta = with lib; {
+    description = "Classes with architecture-specific information";
+    homepage = "https://github.com/angr/archinfo";
+    license = with licenses; [ bsd2 ];
+    maintainers = [ maintainers.fab ];
+  };
+}

pkgs/development/python-modules/minidump/default.nix

···
+{ lib
+, buildPythonPackage
+, fetchPypi
+}:
+
+buildPythonPackage rec {
+  pname = "minidump";
+  version = "0.0.13";
+
+  src = fetchPypi {
+    inherit pname version;
+    sha256 = "1w93yh2dz7llxjgv0jn7gf9praz7d5952is7idgh0lsyj67ri2ms";
+  };
+
+  # Upstream doesn't have tests
+  doCheck = false;
+  pythonImportsCheck = [ "minidump" ];
+
+  meta = with lib; {
+    description = "Python library to parse and read Microsoft minidump file format";
+    homepage = "https://github.com/skelsec/minidump";
+    license = with licenses; [ mit ];
+    maintainers = [ maintainers.fab ];
+  };
+}

pkgs/misc/vim-plugins/generated.nix

···
 
   ale = buildVimPluginFrom2Nix {
     pname = "ale";
-    version = "2021-01-05";
+    version = "2021-01-06";
     src = fetchFromGitHub {
       owner = "dense-analysis";
       repo = "ale";
-      rev = "7e4c125d38181a0e0d0c7883091e2fe683243ce4";
-      sha256 = "0ngmcdbsqxjc00c1jab0h3dic5q1l781bhih30m5xx8qylqhf4g2";
+      rev = "4c454c96a9d142475b155a94cc24fad34eca26b2";
+      sha256 = "0xjacj8pw25qrzasgiwpisrc2fbh4k7ljpn1pq07z2h756cn54lf";
     };
     meta.homepage = "https://github.com/dense-analysis/ale/";
   };
···
 
   barbar-nvim = buildVimPluginFrom2Nix {
     pname = "barbar-nvim";
-    version = "2020-12-28";
+    version = "2021-01-05";
     src = fetchFromGitHub {
       owner = "romgrk";
       repo = "barbar.nvim";
-      rev = "383ffc0712c71481a068e49430321366c53585f2";
-      sha256 = "14s42n4nl94nygszihgji01dwviw1ykqylpm2akdgfhwv1nz1ljn";
+      rev = "e0b4935d5956025ab595195d935a5bac00f1a973";
+      sha256 = "0h723j5zhj8mzwghykd84rxdr0l4ngvyy692d6sl2zz940mvwlkw";
     };
     meta.homepage = "https://github.com/romgrk/barbar.nvim/";
   };
···
 
   brainfuck-vim = buildVimPluginFrom2Nix {
     pname = "brainfuck-vim";
-    version = "2021-01-04";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "fruit-in";
       repo = "brainfuck-vim";
-      rev = "4b85810e1e826dcbb9a38122d4c52e85e470e81a";
-      sha256 = "1q25w1v7kimq0cnjk8afy8ackfshhs25ra8w11l7qra3lrxkwj9b";
+      rev = "ada4fce239ab5386aee51a9453cb0fafc7c2626d";
+      sha256 = "1mm82m7p3khykd1fkag4ppvf2xgnqj8jbhdq7gq06ys1wxzw9rhj";
     };
     meta.homepage = "https://github.com/fruit-in/brainfuck-vim/";
   };
···
 
   coc-nvim = buildVimPluginFrom2Nix {
     pname = "coc-nvim";
-    version = "2021-01-04";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "neoclide";
       repo = "coc.nvim";
-      rev = "5b4b18d2ed2b18870034c7ee853164e1274ab158";
-      sha256 = "0bgprss79nbwc3wd8yi0j90prxmh8saxswfpvpp3x8hilvwiyrrq";
+      rev = "5b8af3eaee714f2c390f2f8e83ea47b78d24eab8";
+      sha256 = "1x088m180wk6b0gk1xdw8crmrhp7s05yshj8nigqyhafm589a7vf";
     };
     meta.homepage = "https://github.com/neoclide/coc.nvim/";
   };
···
     meta.homepage = "https://github.com/Shougo/context_filetype.vim/";
   };
 
+  coq-vim = buildVimPluginFrom2Nix {
+    pname = "coq-vim";
+    version = "2013-01-16";
+    src = fetchFromGitHub {
+      owner = "jvoorhis";
+      repo = "coq.vim";
+      rev = "9b229f5872854dadfb8ba4b67a6a273f37eca4b8";
+      sha256 = "0hpfwcm8lvv831b7i27lw72nqxfy7jymq6a6g3xmf0ycb0l3pnky";
+    };
+    meta.homepage = "https://github.com/jvoorhis/coq.vim/";
+  };
+
   Coqtail = buildVimPluginFrom2Nix {
     pname = "Coqtail";
     version = "2021-01-03";
···
 
   defx-nvim = buildVimPluginFrom2Nix {
     pname = "defx-nvim";
-    version = "2021-01-05";
+    version = "2021-01-06";
     src = fetchFromGitHub {
       owner = "Shougo";
       repo = "defx.nvim";
-      rev = "f44e9486509482ae20c785d39be05581c3dbad15";
-      sha256 = "1s1qmn5v3ghy79da03pf805zdg8j5w0ybri3z36fr2y5s9k7mj4d";
+      rev = "6bf297376aa9ad76500778081ed2ff92fef72301";
+      sha256 = "0k0iyvyg1cbalml1sv8vvs47k4af8vvz0gk6vba6yzjf72v6vj2d";
     };
     meta.homepage = "https://github.com/Shougo/defx.nvim/";
   };
···
 
   deoplete-nvim = buildVimPluginFrom2Nix {
     pname = "deoplete-nvim";
-    version = "2020-12-24";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "Shougo";
       repo = "deoplete.nvim";
-      rev = "b098a5286e95c456d91eed3589a2850aae421219";
-      sha256 = "0y2ijzyn8jqpx5dkbglpa4ivsz6yml49xby7bbz6675rlcawlsq9";
+      rev = "028ebd60d5ad963bf8f77e13c2a85e9edb190f48";
+      sha256 = "0qy6knv5c4v568lvz3fh3ca2lcaym19hi0ywwvj6xyrllil2kk4b";
     };
     meta.homepage = "https://github.com/Shougo/deoplete.nvim/";
   };
···
 
   fern-vim = buildVimPluginFrom2Nix {
     pname = "fern-vim";
-    version = "2021-01-04";
+    version = "2021-01-06";
     src = fetchFromGitHub {
       owner = "lambdalisue";
       repo = "fern.vim";
-      rev = "9783dff6ac69c4e99b78807b08912c4c34100e22";
-      sha256 = "141bifgf06bi43blw6wz7bdsb9l52iqxm9v7b609y49cz71z7n2c";
+      rev = "591e2001fe0546ba28cc7dd614c40f5d92050f92";
+      sha256 = "0cwzsqfyj4bk8f3y9aw9rmfx99gg760apkj7ppww14drc6lzfq09";
     };
     meta.homepage = "https://github.com/lambdalisue/fern.vim/";
   };
···
 
   fzf-vim = buildVimPluginFrom2Nix {
     pname = "fzf-vim";
-    version = "2020-12-30";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "junegunn";
       repo = "fzf.vim";
-      rev = "811b8607c653afe365bb97e6568501b0ad498017";
-      sha256 = "16g0p2gadbw22qlsqrla3nv4a1bipzj00j4qsr2nb2ci13c1831z";
+      rev = "d43df0ea2f099836c2e3499756101e87bcbd3e25";
+      sha256 = "1hclx6c476i523qa5r27r2jbdfdrlbgan1j7aczzwgj3lahbdlvx";
     };
     meta.homepage = "https://github.com/junegunn/fzf.vim/";
   };
···
 
   julia-vim = buildVimPluginFrom2Nix {
     pname = "julia-vim";
-    version = "2020-12-07";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "JuliaEditorSupport";
       repo = "julia-vim";
-      rev = "e14fd34409de39025af93873adc6d26a831d70f9";
-      sha256 = "1s1n74dn53aww6mjb87jcjpmipk2k2ayimimss7kg9c6n15jkqkg";
+      rev = "ce48f42f1fd1d4566503ae26307026c895905a10";
+      sha256 = "08yk47pvyh550iqv6zvrxcjdinn0w9p5al1v49m7p49jfqck3h1m";
     };
     meta.homepage = "https://github.com/JuliaEditorSupport/julia-vim/";
   };
···
 
   lh-brackets = buildVimPluginFrom2Nix {
     pname = "lh-brackets";
-    version = "2021-01-04";
+    version = "2021-01-06";
     src = fetchFromGitHub {
       owner = "LucHermitte";
       repo = "lh-brackets";
-      rev = "7af393f8212759aaea2d2721855fb2f46345ba3e";
-      sha256 = "0wzd1q26bd6b6adaxn9vnr0xd2l8sk73av0b35ga3yv9kfr2j4qb";
+      rev = "547fc9ab14ecf6ecc0d81e8bbb1cc1fec314b6aa";
+      sha256 = "0344ap5fkp1d0g91rv9pn0p28xqz8as48d3m6kxc99w229sj6p2q";
     };
     meta.homepage = "https://github.com/LucHermitte/lh-brackets/";
   };
 
   lh-vim-lib = buildVimPluginFrom2Nix {
     pname = "lh-vim-lib";
-    version = "2020-11-19";
+    version = "2021-01-06";
     src = fetchFromGitHub {
       owner = "LucHermitte";
       repo = "lh-vim-lib";
-      rev = "0edb04acd77b9e5e498314b6345d422d93921ffa";
-      sha256 = "1cndwbwx9pg6550k7j2z0pw91dll0idspd0jpd0kycpxm4330jy9";
+      rev = "65614730a667144a444fbd4a028a81171481c537";
+      sha256 = "1vxm3ym51qa63zbrkdz2pvwafr3kmdxgpxrdwb1g8i7qsxjsvgl1";
     };
     meta.homepage = "https://github.com/LucHermitte/lh-vim-lib/";
   };
···
 
   nlua-nvim = buildVimPluginFrom2Nix {
     pname = "nlua-nvim";
-    version = "2020-11-16";
+    version = "2021-01-05";
     src = fetchFromGitHub {
       owner = "tjdevries";
       repo = "nlua.nvim";
-      rev = "92fdfb1eb791e79ff1d6403dd26b59ce61dd09c6";
-      sha256 = "1ka8k8rxn406glrc0qz8rk3zrxhpdaky040v1a65g5alb50af9hz";
+      rev = "c0e8fbcaf8bcf5571a9e1d780a72094aad3f3094";
+      sha256 = "0q5aw3n4dsszk5iw7qg01xx1rbrr18jh1wqs6k9dd1kcr6yq22rq";
     };
     meta.homepage = "https://github.com/tjdevries/nlua.nvim/";
   };
···
 
   nvim-lspconfig = buildVimPluginFrom2Nix {
     pname = "nvim-lspconfig";
-    version = "2021-01-04";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "neovim";
       repo = "nvim-lspconfig";
-      rev = "384e512a640b2b18f3d2c3e9dcb6e870814ed1eb";
-      sha256 = "1fkmnkvpp27azi3g3iqkrhch0a4q6in16cp29zs0dvgrk7iv0cg1";
+      rev = "fa2ccc10d5a7b390c1d808ddf74dce5158debca4";
+      sha256 = "1mdnk4vvxk9qzcinzw64fck87a3dg5f21jm8203zhgj94ylc851y";
     };
     meta.homepage = "https://github.com/neovim/nvim-lspconfig/";
   };
···
     src = fetchFromGitHub {
       owner = "dstein64";
       repo = "nvim-scrollview";
-      rev = "f729b1dd9077f8b1818752adc7416f357c057325";
-      sha256 = "0fdwgzn329y9mdrl98wl4aa14sh4l0my0kch5gszk5b9872zir69";
+      rev = "99e153bb534f5ec5e24ef6d35366d9b29f409ee3";
+      sha256 = "1p0an1j7qw1rl5hkv6mvqvdzihxanf0vxf2ryih2cnmmys3cw9v1";
     };
     meta.homepage = "https://github.com/dstein64/nvim-scrollview/";
   };
···
 
   nvim-treesitter = buildVimPluginFrom2Nix {
     pname = "nvim-treesitter";
-    version = "2021-01-04";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "nvim-treesitter";
       repo = "nvim-treesitter";
-      rev = "f2c219cddcaf6d7237bdc957c84ef4cdb9072a89";
-      sha256 = "0b2a9rcbp647z620brcchw83dkdsar3d0j881dr0qcxxf496w9cz";
+      rev = "2e8621ff1afa2284de3df316ecd0baf8e9195927";
+      sha256 = "0yb5lf29j3ddi9ia7lld8ps662r7kw2znxhp2pyyjlgnd76m08nr";
     };
     meta.homepage = "https://github.com/nvim-treesitter/nvim-treesitter/";
   };
···
 
   nvim-treesitter-refactor = buildVimPluginFrom2Nix {
     pname = "nvim-treesitter-refactor";
-    version = "2020-10-07";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "nvim-treesitter";
       repo = "nvim-treesitter-refactor";
-      rev = "9d4b9daf2f138a5de538ee094bd899591004f8e2";
-      sha256 = "0ma5zsl70mi92b9y8nhgkppdiqfjj0bl3gklhjv1c3lg7kny7511";
+      rev = "16bbe963d044ec94316679868e0988caa7b5b4c3";
+      sha256 = "0jgasxphwi222ga73y3jh5zq9m95n74331jn8r3nv741lk2g0772";
     };
     meta.homepage = "https://github.com/nvim-treesitter/nvim-treesitter-refactor/";
   };
···
 
   nvim-ts-rainbow = buildVimPluginFrom2Nix {
     pname = "nvim-ts-rainbow";
-    version = "2020-12-18";
+    version = "2021-01-05";
     src = fetchFromGitHub {
       owner = "p00f";
       repo = "nvim-ts-rainbow";
-      rev = "32d4b898989e504345c91ee802f5faeb7d12fc39";
-      sha256 = "1k4c1hsc1gwm6lv5k9lhpqx6dcbyc273aikm9j1q5i21mzrvl15f";
+      rev = "68eee9b031432de6a1964315235d3cf265243a77";
+      sha256 = "0zjhyd02sj17i0yrmffzzja2s0y9fa37v1nvqa17kap9vmcgyh7h";
     };
     meta.homepage = "https://github.com/p00f/nvim-ts-rainbow/";
   };
···
 
   popfix = buildVimPluginFrom2Nix {
     pname = "popfix";
-    version = "2020-12-29";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "RishabhRD";
       repo = "popfix";
-      rev = "3e78c1c638d6330f77989321e1c68c55aa8a5e67";
-      sha256 = "1ahffc58a0ps1hmnaqc1rzvisn2axrcd5wbxi6n7z5hmbx86fw99";
+      rev = "9ab0aa5f186a2a2429c55f1512e2fd8b536183f0";
+      sha256 = "0ks9hxc506ybwrvk5qkl1qkj634ms5icy8cg0w3b1q5qzgz5k0wn";
       fetchSubmodules = true;
     };
     meta.homepage = "https://github.com/RishabhRD/popfix/";
···
 
   tagbar = buildVimPluginFrom2Nix {
     pname = "tagbar";
-    version = "2020-12-21";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "preservim";
       repo = "tagbar";
-      rev = "eaadf90b61fd039415b2e5e8b9c38598e9b2daed";
-      sha256 = "0283cn4cpdgdclmpc21dcwhign03h0mmahpmr34dp8fa286vlirv";
+      rev = "978e1fe761de8be1f4d6c8469deba74a3cc0872f";
+      sha256 = "0y9bd1y23z9w7ibn761yx5wq02liazv5dgxfqyy6xfxr17zvd514";
     };
     meta.homepage = "https://github.com/preservim/tagbar/";
   };
···
 
   telescope-nvim = buildVimPluginFrom2Nix {
     pname = "telescope-nvim";
-    version = "2021-01-05";
+    version = "2021-01-06";
     src = fetchFromGitHub {
       owner = "nvim-telescope";
       repo = "telescope.nvim";
-      rev = "f750159203077b00cecdd9f68c254aa70d10f879";
-      sha256 = "01m5ydj56y87b05ppaxr1697f2ncbm28w6njvd3gh0z3nhdmd69n";
+      rev = "1d6195ff643ed153eb0f233b32f1becc68c79ee6";
+      sha256 = "1ma2m0jx50kdkvdibagqlqqap0phkjnascimfiandpzcsl3r6939";
     };
     meta.homepage = "https://github.com/nvim-telescope/telescope.nvim/";
   };
···
 
   vim-clap = buildVimPluginFrom2Nix {
     pname = "vim-clap";
-    version = "2021-01-01";
+    version = "2021-01-05";
     src = fetchFromGitHub {
       owner = "liuchengxu";
       repo = "vim-clap";
-      rev = "b9ca65dbcc89dfb2702fb2ab0e98c7119f4e6bbf";
-      sha256 = "0j9xh0yf224fsnm9ksml9m8jfx4m9iji0a6h8q0mk8zglvh6qksc";
+      rev = "83cac4972caef144d0e947025ff43af6fd2becac";
+      sha256 = "18cackh5rrkyg7ffhwp4vca6srr1hlj3gximjdwc6krcgq0v0r0s";
     };
     meta.homepage = "https://github.com/liuchengxu/vim-clap/";
   };
···
 
   vim-floaterm = buildVimPluginFrom2Nix {
     pname = "vim-floaterm";
-    version = "2021-01-05";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "voldikss";
       repo = "vim-floaterm";
-      rev = "e8f65534e607d8bd82ba2c4a8ada1adc6cb36c96";
-      sha256 = "010zr13y3016zfd6fqmknqg1ld19n9isfbgwl8hqgfrgjh9mn9p3";
+      rev = "5e218d8387b7ca1ade1c625a1b81d45996cc21ae";
+      sha256 = "1sgdyjwq5h0m6d40aapz9n2z59jc92vpgj04d5ciisifwh54aaga";
     };
     meta.homepage = "https://github.com/voldikss/vim-floaterm/";
   };
···
 
   vim-illuminate = buildVimPluginFrom2Nix {
     pname = "vim-illuminate";
-    version = "2021-01-04";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "RRethy";
       repo = "vim-illuminate";
-      rev = "f52857989c14c2f27d72ffa78d6af906fa436cd1";
-      sha256 = "1sbb3nkd3n3y9r5gs03lmwrmra7j8w8450q444g7b3h5hhx4b92l";
+      rev = "f8d01ab7417be5e3878678acd46e4d17e8d8d9b6";
+      sha256 = "1vnhvnxw7a4v583pw80lqcc9bb9lmcfzm1vhnskxrfxhz01r9ina";
     };
     meta.homepage = "https://github.com/RRethy/vim-illuminate/";
   };
···
 
   vim-snipmate = buildVimPluginFrom2Nix {
     pname = "vim-snipmate";
-    version = "2020-10-02";
+    version = "2021-01-06";
     src = fetchFromGitHub {
       owner = "garbas";
       repo = "vim-snipmate";
-      rev = "68eebf9dabe5c1d1964e78dda188765f224bab34";
-      sha256 = "1mxa373ry17zwszd089k99lbgr5pg46x5dlahpk0l68ksxpkbxir";
+      rev = "51168d7dc184c8234e692cd66e89bc7f95e35d72";
+      sha256 = "1psxnv6y690nx6g3msyxw8gm6z16gxdn92rlngpjirgs513kigin";
     };
     meta.homepage = "https://github.com/garbas/vim-snipmate/";
   };
 
   vim-snippets = buildVimPluginFrom2Nix {
     pname = "vim-snippets";
-    version = "2021-01-04";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "honza";
       repo = "vim-snippets";
-      rev = "6159e8e820656e4370d54ddbf11278bf92794139";
-      sha256 = "1kwdcx429kw39f8fsav3lcnahkbzbdmny1d81pq6c24k1r7hfp1h";
+      rev = "d43498c949a3acf297fd74397a3bc165033f2028";
+      sha256 = "1q0b3xsr1br172n6mj5bfza2lcacznlnwk2sgasxz8bkdq1rk6mi";
     };
     meta.homepage = "https://github.com/honza/vim-snippets/";
   };
···
 
   vim-visual-multi = buildVimPluginFrom2Nix {
     pname = "vim-visual-multi";
-    version = "2021-01-01";
+    version = "2021-01-06";
     src = fetchFromGitHub {
       owner = "mg979";
       repo = "vim-visual-multi";
-      rev = "c27966b82e3ebf39278b53ae600c9763907937d9";
-      sha256 = "15246xx9qixgdw1wff4kka9vcpkirkdbz8j25zhicx3dqvqzzb4c";
+      rev = "d95d4c31a7919f58e9bb89bfc0c3a272461d782d";
+      sha256 = "1xnixwq6rddvs0za76sic3sf5fk0v10cdrsyaz3d6y0g0qmv9cz0";
     };
     meta.homepage = "https://github.com/mg979/vim-visual-multi/";
   };
···
 
   vim-vsnip = buildVimPluginFrom2Nix {
     pname = "vim-vsnip";
-    version = "2021-01-05";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "hrsh7th";
       repo = "vim-vsnip";
-      rev = "879dc259bb3fbb850473982d64c441c16a4daa38";
-      sha256 = "103mws249r6rxg7mc28fv9avk60arn8jxspddvynd27srvzrbif8";
+      rev = "5917d944b259baab85c9c249a8be33a82cd033d3";
+      sha256 = "0gj5qjrb31j93vv8wpqlhdpsgrnkwaxvhvslkjj9m3fnx34gqvdv";
     };
     meta.homepage = "https://github.com/hrsh7th/vim-vsnip/";
   };
···
 
   vimspector = buildVimPluginFrom2Nix {
     pname = "vimspector";
-    version = "2021-01-02";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "puremourning";
       repo = "vimspector";
-      rev = "65708f55e0a1186c76af9a5a1f14e9157cf588b9";
-      sha256 = "1m16i4s89q5ff9qi79qyq34184cfnfbglnfqxg6zsp8pb8kfpiix";
+      rev = "07ea3880acf5977075831c64536e683ddb2fed89";
+      sha256 = "1gkvagird3xa47gicpc739s4c5p5358yvp16fxx2l98jzzi7wvcj";
       fetchSubmodules = true;
     };
     meta.homepage = "https://github.com/puremourning/vimspector/";
···
 
   vimtex = buildVimPluginFrom2Nix {
     pname = "vimtex";
-    version = "2021-01-03";
+    version = "2021-01-07";
     src = fetchFromGitHub {
       owner = "lervag";
       repo = "vimtex";
-      rev = "e5214dd3fe5b2b7f3092d43e58b430032dfebe40";
-      sha256 = "1vni0kyf9cglvsnwgi6nalygj291gb337rdmi0jn0i0x76h0g65p";
+      rev = "d219436e224960b8e4c11db8a1e482ef52f8d63b";
+      sha256 = "00brsffbs6550k876bbgxl7v8d4dqs9vca3ghncm3wcjpjs2qhar";
     };
     meta.homepage = "https://github.com/lervag/vimtex/";
   };

pkgs/misc/vim-plugins/vim-plugin-names

···
 justinj/vim-pico8-syntax
 justinmk/vim-dirvish
 justinmk/vim-sneak
+jvoorhis/coq.vim
 KabbAmine/vCoolor.vim
 KabbAmine/zeavim.vim
 kalbasit/vim-colemak

pkgs/misc/vscode-extensions/default.nix

···
         };
       };
 
+      mechatroner.rainbow-csv = buildVscodeMarketplaceExtension {
+        mktplcRef = {
+          name = "rainbow-csv";
+          publisher = "mechatroner";
+          version = "1.7.1";
+          sha256 = "0w5mijs4ll5qjkpyw7qpn1k40pq8spm0b3q72x150ydbcini5hxw";
+        };
+        meta = {
+          license = stdenv.lib.licenses.mit;
+        };
+      };
+
       ms-azuretools.vscode-docker = buildVscodeMarketplaceExtension {
         mktplcRef = {
           name = "vscode-docker";

pkgs/os-specific/linux/nvidia-x11/default.nix

···
   # Policy: use the highest stable version as the default (on our master).
   stable = if stdenv.hostPlatform.system == "x86_64-linux"
     then generic {
-      version = "455.45.01";
-      sha256_64bit = "6tyMfggvZVQPp/aiSdgwn7VG/mIGb0lUcnAdyMEDoVM=";
-      settingsSha256 = "70ABqnO/heCp/5IztpU0Lo7eZd4n4wUoTlp1xIQ3aCc=";
-      persistencedSha256 = "36sM+djZvm77Gle7dcZ5tppgzQkD4IA0FJgCGsdZRI8=";
+      version = "460.32.03";
+      sha256_64bit = "0qb0f8djys55b7qgvpbwafw5lkwvmcslqz3i2kr3jm354gy248ag";
+      settingsVersion = "460.27.04";
+      settingsSha256 = "1z9ibkhyjqzhhzi3gj88f5jlpc1d76jsncsy6wxpnbdbak8ljkw5";
+      persistencedSha256 = "36sM+djZmv77lGe7cdZ5tppzgkQD4IA0FJgCGsdZRI8=";
     }
     else legacy_390;
 

pkgs/top-level/all-packages.nix

···
     novacomd = callPackage ../development/mobile/webos/novacomd.nix { };
   };
 
+  apprise = with python3Packages; toPythonApplication apprise;
+
   aria2 = callPackage ../tools/networking/aria2 {
     inherit (darwin.apple_sdk.frameworks) Security;
     inherit (python3Packages) sphinx;
···
   heimer = libsForQt5.callPackage ../applications/misc/heimer { };
 
   hello = callPackage ../applications/misc/hello { };
+
+  hello-wayland = callPackage ../applications/graphics/hello-wayland { };
+
   hello-unfree = callPackage ../applications/misc/hello-unfree { };
 
   helmholtz = callPackage ../applications/audio/pd-plugins/helmholtz { };
···
   cadical = callPackage ../applications/science/logic/cadical {};
 
   inherit (callPackage ./coq-packages.nix {
-    inherit (ocaml-ng) ocamlPackages_4_05 ocamlPackages_4_09;
+    inherit (ocaml-ng) ocamlPackages_4_05 ocamlPackages_4_09 ocamlPackages_4_10;
   }) mkCoqPackages
     coqPackages_8_5  coq_8_5
     coqPackages_8_6  coq_8_6

pkgs/top-level/coq-packages.nix

···
 { lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
-, compcert
-}:
-
+, ocamlPackages_4_10, compcert
+}@args:
+let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in
 let
   mkCoqPackages' = self: coq:
     let callPackage = self.callPackage; in {
-      inherit coq;
+      inherit coq lib;
       coqPackages = self;
+
+      mkCoqDerivation = callPackage ../build-support/coq {};
 
       contribs = recurseIntoAttrs
         (callPackage ../development/coq-modules/contribs {});
···
       coq-elpi = callPackage ../development/coq-modules/coq-elpi {};
       coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
       coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
+      coqeal = callPackage ../development/coq-modules/coqeal {};
       coqhammer = callPackage ../development/coq-modules/coqhammer {};
       coqprime = callPackage ../development/coq-modules/coqprime {};
       coquelicot = callPackage ../development/coq-modules/coquelicot {};
···
       iris = callPackage ../development/coq-modules/iris {};
       ltac2 = callPackage ../development/coq-modules/ltac2 {};
       math-classes = callPackage ../development/coq-modules/math-classes { };
-      inherit (callPackage ../development/coq-modules/mathcomp {})
-        mathcomp_ mathcomp-config
-        mathcomp ssreflect
-        mathcomp-ssreflect mathcomp-fingroup mathcomp-algebra
-        mathcomp-solvable mathcomp-field mathcomp-character
-      ;
-      inherit (callPackage ../development/coq-modules/mathcomp/extra.nix { })
-        mathcomp-extra-override mathcomp-extra-config mathcomp-extra
-        current-mathcomp-extra mathcomp-extra-fast mathcomp-extra-all
-        mathcomp-finmap mathcomp-bigenough mathcomp-real-closed
-        mathcomp-analysis multinomials coqeal
-      ;
+      mathcomp = callPackage ../development/coq-modules/mathcomp {};
+      ssreflect          = self.mathcomp.ssreflect;
+      mathcomp-ssreflect = self.mathcomp.ssreflect;
+      mathcomp-fingroup  = self.mathcomp.fingroup;
+      mathcomp-algebra   = self.mathcomp.algebra;
+      mathcomp-solvable  = self.mathcomp.solvable;
+      mathcomp-field     = self.mathcomp.field;
+      mathcomp-character = self.mathcomp.character;
+      mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis {};
+      mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap {};
+      mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {};
+      mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {};
       metalib = callPackage ../development/coq-modules/metalib { };
+      multinomials = callPackage ../development/coq-modules/multinomials {};
       paco = callPackage ../development/coq-modules/paco {};
       paramcoq = callPackage ../development/coq-modules/paramcoq {};
       QuickChick = callPackage ../development/coq-modules/QuickChick {};
···
       VST = callPackage ../development/coq-modules/VST {
         compcert = compcert.override { version = "3.7"; };
       };
-
-      filterPackages = filterCoqPackages;
+      filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
     };
 
-  filterCoqPackages = coq: set:
+  filterCoqPackages = set:
     lib.listToAttrs (
-      lib.concatMap (name:
-        let v = set.${name}; in
-        let p = v.compatibleCoqVersions or (_: true); in
-        lib.optional (p coq.coq-version)
-          (lib.nameValuePair name (
-            if lib.isAttrs v && v.recurseForDerivations or false
-            then filterCoqPackages coq v
-            else v))
+      lib.concatMap (name: let v = set.${name} or null; in
+          lib.optional (! v.meta.coqFilter or false)
+            (lib.nameValuePair name (
+              if lib.isAttrs v && v.recurseForDerivations or false
+              then filterCoqPackages v
+              else v))
       ) (lib.attrNames set)
     );
-
+  mkCoq = version: callPackage ../applications/science/logic/coq {
+    inherit version ocamlPackages_4_05 ocamlPackages_4_09 ocamlPackages_4_10;
+  };
 in rec {
 
   /* The function `mkCoqPackages` takes as input a derivation for Coq and produces
···
    */
   mkCoqPackages = coq:
     let self = lib.makeScope newScope (lib.flip mkCoqPackages' coq); in
-    if coq.dontFilter or false then self else filterCoqPackages coq self;
+    self.filterPackages (! coq.dontFilter or false);
 
-  coq_8_5 = callPackage ../applications/science/logic/coq {
-    ocamlPackages = ocamlPackages_4_05;
-    version = "8.5pl3";
-  };
-  coq_8_6 = callPackage ../applications/science/logic/coq {
-    ocamlPackages = ocamlPackages_4_05;
-    version = "8.6.1";
-  };
-  coq_8_7 = callPackage ../applications/science/logic/coq {
-    ocamlPackages = ocamlPackages_4_09;
-    version = "8.7.2";
-  };
-  coq_8_8 = callPackage ../applications/science/logic/coq {
-    ocamlPackages = ocamlPackages_4_09;
-    version = "8.8.2";
-  };
-  coq_8_9 = callPackage ../applications/science/logic/coq {
-    ocamlPackages = ocamlPackages_4_09;
-    version = "8.9.1";
-  };
-  coq_8_10 = callPackage ../applications/science/logic/coq {
-    ocamlPackages = ocamlPackages_4_09;
-    version = "8.10.2";
-  };
-  coq_8_11 = callPackage ../applications/science/logic/coq {
-    version = "8.11.2";
-  };
-  coq_8_12 = callPackage ../applications/science/logic/coq {
-    version = "8.12.2";
-  };
-  coq_8_13 = callPackage ../applications/science/logic/coq {
-    version = "8.13+beta1";
-  };
+  coq_8_5  = mkCoq "8.5";
+  coq_8_6  = mkCoq "8.6";
+  coq_8_7  = mkCoq "8.7";
+  coq_8_8  = mkCoq "8.8";
+  coq_8_9  = mkCoq "8.9";
+  coq_8_10 = mkCoq "8.10";
+  coq_8_11 = mkCoq "8.11";
+  coq_8_12 = mkCoq "8.12";
+  coq_8_13 = mkCoq "8.13";
 
   coqPackages_8_5 = mkCoqPackages coq_8_5;
   coqPackages_8_6 = mkCoqPackages coq_8_6;

pkgs/top-level/python-packages.nix

···
 
   arabic-reshaper = callPackage ../development/python-modules/arabic-reshaper { };
 
+  archinfo = callPackage ../development/python-modules/archinfo { };
+
   area = callPackage ../development/python-modules/area { };
 
   arelle = callPackage ../development/python-modules/arelle { gui = true; };
···
   milksnake = callPackage ../development/python-modules/milksnake { };
 
   minidb = callPackage ../development/python-modules/minidb { };
+
+  minidump = callPackage ../development/python-modules/minidump { };
 
   minimock = callPackage ../development/python-modules/minimock { };