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

156 lines
5.2 KiB
Nix
Raw Normal View History

2024-05-02 00:46:19 +00:00
{ lib, stdenv, coqPackages, coq, which, fetchzip }@args:
let
2024-05-13 21:24:10 +00:00
lib = import ./extra-lib.nix { inherit (args) lib; };
2024-05-02 00:46:19 +00:00
inherit (lib)
2024-05-13 21:24:10 +00:00
concatStringsSep flip foldl isFunction isString optional optionalAttrs
optionals optionalString pred remove switch versions;
2024-05-02 00:46:19 +00:00
inherit (lib.attrsets) removeAttrs;
inherit (lib.strings) match;
isGitHubDomain = d: match "^github.*" d != null;
isGitLabDomain = d: match "^gitlab.*" d != null;
2024-05-13 21:24:10 +00:00
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:
2024-05-02 00:46:19 +00:00
let
args-to-remove = foldl (flip remove) ([
2024-05-13 21:24:10 +00:00
"version"
"fetcher"
"repo"
"owner"
"domain"
"releaseRev"
"displayVersion"
"defaultVersion"
"useMelquiondRemake"
2024-05-02 00:46:19 +00:00
"release"
2024-05-13 21:24:10 +00:00
"buildInputs"
"nativeBuildInputs"
"extraBuildInputs"
"extraNativeBuildInputs"
"overrideBuildInputs"
"overrideNativeBuildInputs"
2024-05-02 00:46:19 +00:00
"namePrefix"
2024-05-13 21:24:10 +00:00
"meta"
"useDuneifVersion"
"useDune"
"opam-name"
"extraInstallFlags"
"setCOQBIN"
"mlPlugin"
"dropAttrs"
"dropDerivationAttrs"
"keepAttrs"
] ++ dropAttrs) keepAttrs;
fetch = import ../coq/meta-fetch/default.nix { inherit lib stdenv fetchzip; }
({
2024-05-02 00:46:19 +00:00
inherit release releaseRev;
location = { inherit domain owner repo; };
2024-05-13 21:24:10 +00:00
} // optionalAttrs (args ? fetcher) { inherit fetcher; });
2024-05-02 00:46:19 +00:00
fetched = fetch (if version != null then version else defaultVersion);
display-pkg = n: sep: v:
2024-05-13 21:24:10 +00:00
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);
}
2024-05-02 00:46:19 +00:00
] "") + 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);
2024-05-13 21:24:10 +00:00
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" ];
2024-05-02 00:46:19 +00:00
2024-05-13 21:24:10 +00:00
in stdenv.mkDerivation (removeAttrs ({
2024-05-02 00:46:19 +00:00
name = prefix-name + (display-pkg pname "-" fetched.version);
inherit (fetched) version src;
2024-05-13 21:24:10 +00:00
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);
2024-05-02 00:46:19 +00:00
inherit enableParallelBuilding;
2024-05-13 21:24:10 +00:00
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 { });
2024-05-02 00:46:19 +00:00
2024-05-13 21:24:10 +00:00
} // (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)