core/pkgs/build-support/coq/default.nix

{ lib, stdenv, coqPackages, coq, which, fetchzip }@args:

let
  lib = import ./extra-lib.nix { inherit (args) lib; };

  inherit (lib)
    concatStringsSep flip foldl isFunction isString optional optionalAttrs
    optionals optionalString pred remove switch versions;

  inherit (lib.attrsets) removeAttrs;
  inherit (lib.strings) match;

  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)