summary refs log tree commit diff
path: root/pkgs/build-support/coq/default.nix
blob: eb045ddf6865abbd5a8aa0f360807da06f9e50b1 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
{ lib, stdenv, coqPackages, coq, which, 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 ? {},
  buildInputs ? [],
  nativeBuildInputs ? [],
  extraBuildInputs ? [],
  extraNativeBuildInputs ? [],
  overrideBuildInputs ? [],
  overrideNativeBuildInputs ? [],
  namePrefix ? [ "coq" ],
  enableParallelBuilding ? true,
  extraInstallFlags ? [],
  setCOQBIN ? true,
  mlPlugin ? false,
  useMelquiondRemake ? null,
  dropAttrs ? [],
  keepAttrs ? [],
  dropDerivationAttrs ? [],
  useDuneifVersion ? (x: false),
  useDune ? false,
  opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])),
  ...
}@args:
let
  args-to-remove = foldl (flip remove) ([
    "version" "fetcher" "repo" "owner" "domain" "releaseRev"
    "displayVersion" "defaultVersion" "useMelquiondRemake"
    "release"
    "buildInputs" "nativeBuildInputs"
    "extraBuildInputs" "extraNativeBuildInputs"
    "overrideBuildInputs" "overrideNativeBuildInputs"
    "namePrefix"
    "meta" "useDuneifVersion" "useDune" "opam-name"
    "extraInstallFlags" "setCOQBIN" "mlPlugin"
    "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
  fetch = import ../coq/meta-fetch/default.nix
    { inherit lib stdenv fetchzip; } ({
      inherit release releaseRev;
      location = { inherit domain owner repo; };
    } // optionalAttrs (args?fetcher) {inherit fetcher;});
  fetched = fetch (if version != null then version else defaultVersion);
  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;
  useDune = args.useDune or (useDuneifVersion fetched.version);
  coqlib-flags = switch coq.coq-version [
    { case = v: versions.isLe "8.6" v && v != "dev" ;
      out = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; }
  ] [ "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib"
      "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" ];
  docdir-flags = switch coq.coq-version [
    { case = v: versions.isLe "8.6" v && v != "dev";
      out = [ "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ]; }
  ] [ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ];
in

stdenv.mkDerivation (removeAttrs ({

  name = prefix-name + (display-pkg pname "-" fetched.version);

  inherit (fetched) version src;

  nativeBuildInputs = args.overrideNativeBuildInputs
    or ([ which ]
        ++ optional useDune coq.ocamlPackages.dune_3
        ++ optionals (useDune || mlPlugin) [ coq.ocamlPackages.ocaml coq.ocamlPackages.findlib ]
        ++ (args.nativeBuildInputs or []) ++ extraNativeBuildInputs);
  buildInputs = args.overrideBuildInputs
    or ([ coq ] ++ (args.buildInputs or []) ++ 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 =
    coqlib-flags ++ docdir-flags ++
    extraInstallFlags;
})
// (optionalAttrs useDune {
  buildPhase = ''
    runHook preBuild
    dune build -p ${opam-name} ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
    runHook postBuild
  '';
  installPhase = ''
    runHook preInstall
    dune install ${opam-name} --prefix=$out
    mv $out/lib/coq $out/lib/TEMPORARY
    mkdir $out/lib/coq/
    mv $out/lib/TEMPORARY $out/lib/coq/${coq.coq-version}
    runHook postInstall
  '';
})
// (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)