coqPackages: refactor

3 files changed, 303 insertions, 0 deletions

diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix
new file mode 100644
index 00000000000..7e925e2473e
--- /dev/null
+++ b/pkgs/build-support/coq/default.nix
@@ -0,0 +1,92 @@
+{ 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)
diff --git a/pkgs/build-support/coq/extra-lib.nix b/pkgs/build-support/coq/extra-lib.nix
new file mode 100644
index 00000000000..65b48f51126
--- /dev/null
+++ b/pkgs/build-support/coq/extra-lib.nix
@@ -0,0 +1,145 @@
+{ 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;
+})
diff --git a/pkgs/build-support/coq/meta-fetch/default.nix b/pkgs/build-support/coq/meta-fetch/default.nix
new file mode 100644
index 00000000000..580d58395ef
--- /dev/null
+++ b/pkgs/build-support/coq/meta-fetch/default.nix
@@ -0,0 +1,66 @@
+{ 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")