pkgs/build-support/coq/default.nix

   1 { lib, stdenv, coqPackages, coq, which, fetchzip, fetchurl }@args:
   2
   3 let
   4   lib = import ./extra-lib.nix {
   5     inherit (args) lib;
   6   };
   7
   8   inherit (lib)
   9     concatStringsSep
  10     flip
  11     foldl
  12     isFunction
  13     isString
  14     optional
  15     optionalAttrs
  16     optionals
  17     optionalString
  18     pred
  19     remove
  20     switch
  21     versions
  22     ;
  23
  24   inherit (lib.attrsets) removeAttrs;
  25   inherit (lib.strings) match;
  26
  27   isGitHubDomain = d: match "^github.*" d != null;
  28   isGitLabDomain = d: match "^gitlab.*" d != null;
  29 in
  30
  31 { pname,
  32   version ? null,
  33   fetcher ? null,
  34   owner ? "coq-community",
  35   domain ? "github.com",
  36   repo ? pname,
  37   defaultVersion ? null,
  38   releaseRev ? (v: v),
  39   displayVersion ? {},
  40   release ? {},
  41   buildInputs ? [],
  42   nativeBuildInputs ? [],
  43   extraBuildInputs ? [],
  44   extraNativeBuildInputs ? [],
  45   overrideBuildInputs ? [],
  46   overrideNativeBuildInputs ? [],
  47   namePrefix ? [ "coq" ],
  48   enableParallelBuilding ? true,
  49   extraInstallFlags ? [],
  50   setCOQBIN ? true,
  51   mlPlugin ? false,
  52   useMelquiondRemake ? null,
  53   dropAttrs ? [],
  54   keepAttrs ? [],
  55   dropDerivationAttrs ? [],
  56   useDuneifVersion ? (x: false),
  57   useDune ? false,
  58   opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])),
  59   ...
  60 }@args:
  61 let
  62   args-to-remove = foldl (flip remove) ([
  63     "version" "fetcher" "repo" "owner" "domain" "releaseRev"
  64     "displayVersion" "defaultVersion" "useMelquiondRemake"
  65     "release"
  66     "buildInputs" "nativeBuildInputs"
  67     "extraBuildInputs" "extraNativeBuildInputs"
  68     "overrideBuildInputs" "overrideNativeBuildInputs"
  69     "namePrefix"
  70     "meta" "useDuneifVersion" "useDune" "opam-name"
  71     "extraInstallFlags" "setCOQBIN" "mlPlugin"
  72     "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
  73   fetch = import ../coq/meta-fetch/default.nix
  74     { inherit lib stdenv fetchzip fetchurl; } ({
  75       inherit release releaseRev;
  76       location = { inherit domain owner repo; };
  77     } // optionalAttrs (args?fetcher) {inherit fetcher;});
  78   fetched = fetch (if version != null then version else defaultVersion);
  79   display-pkg = n: sep: v:
  80     let d = displayVersion.${n} or (if sep == "" then ".." else true); in
  81     n + optionalString (v != "" && v != null) (switch d [
  82       { case = true;       out = sep + v; }
  83       { case = ".";        out = sep + versions.major v; }
  84       { case = "..";       out = sep + versions.majorMinor v; }
  85       { case = "...";      out = sep + versions.majorMinorPatch v; }
  86       { case = isFunction; out = optionalString (d v != "") (sep + d v); }
  87       { case = isString;   out = optionalString (d != "") (sep + d); }
  88     ] "") + optionalString (v == null) "-broken";
  89   append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-";
  90   prefix-name = foldl append-version "" namePrefix;
  91   useDune = args.useDune or (useDuneifVersion fetched.version);
  92   coqlib-flags = switch coq.coq-version [
  93     { case = v: versions.isLe "8.6" v && v != "dev" ;
  94       out = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; }
  95   ] [ "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib"
  96       "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" ];
  97   docdir-flags = switch coq.coq-version [
  98     { case = v: versions.isLe "8.6" v && v != "dev";
  99       out = [ "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ]; }
 100   ] [ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ];
 101 in
 102
 103 stdenv.mkDerivation (removeAttrs ({
 104
 105   name = prefix-name + (display-pkg pname "-" fetched.version);
 106
 107   inherit (fetched) version src;
 108
 109   nativeBuildInputs = args.overrideNativeBuildInputs
 110     or ([ which ]
 111         ++ optional useDune coq.ocamlPackages.dune_3
 112         ++ optionals (useDune || mlPlugin) [ coq.ocamlPackages.ocaml coq.ocamlPackages.findlib ]
 113         ++ (args.nativeBuildInputs or []) ++ extraNativeBuildInputs);
 114   buildInputs = args.overrideBuildInputs
 115     or ([ coq ] ++ (args.buildInputs or []) ++ extraBuildInputs);
 116   inherit enableParallelBuilding;
 117
 118   meta = ({ platforms = coq.meta.platforms; } //
 119     (switch domain [{
 120         case = pred.union isGitHubDomain isGitLabDomain;
 121         out = { homepage = "https://${domain}/${owner}/${repo}"; };
 122       }] {}) //
 123     optionalAttrs (fetched.broken or false) { coqFilter = true; broken = true; }) //
 124     (args.meta or {}) ;
 125
 126 }
 127 // (optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; })
 128 // (optionalAttrs (!args?installPhase && !args?useMelquiondRemake) {
 129   installFlags =
 130     coqlib-flags ++ docdir-flags ++
 131     extraInstallFlags;
 132 })
 133 // (optionalAttrs useDune {
 134   buildPhase = ''
 135     runHook preBuild
 136     dune build -p ${opam-name} ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
 137     runHook postBuild
 138   '';
 139   installPhase = ''
 140     runHook preInstall
 141     dune install --prefix=$out --libdir $OCAMLFIND_DESTDIR ${opam-name}
 142     mkdir $out/lib/coq/
 143     mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
 144     runHook postInstall
 145   '';
 146 })
 147 // (optionalAttrs (args?useMelquiondRemake) rec {
 148   COQUSERCONTRIB = "$out/lib/coq/${coq.coq-version}/user-contrib";
 149   preConfigurePhases = [ "autoconf" ];
 150   configureFlags = [ "--libdir=${COQUSERCONTRIB}/${useMelquiondRemake.logpath or ""}" ];
 151   buildPhase = "./remake -j$NIX_BUILD_CORES";
 152   installPhase = "./remake install";
 153 })
 154 // (removeAttrs args args-to-remove)) dropDerivationAttrs)