coq: init at 8.10+β1

This commit is contained in:
Vincent Laporte 2019-05-14 08:31:49 +00:00 committed by Vincent Laporte
parent 1ce94fad33
commit b72daf7117
10 changed files with 24 additions and 10 deletions

View File

@ -8,6 +8,7 @@
{ stdenv, fetchFromGitHub, writeText, pkgconfig { stdenv, fetchFromGitHub, writeText, pkgconfig
, ocamlPackages, ncurses , ocamlPackages, ncurses
, buildIde ? true , buildIde ? true
, glib, gnome3, wrapGAppsHook
, csdp ? null , csdp ? null
, version , version
}: }:
@ -26,12 +27,15 @@ let
"8.8.1" = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk"; "8.8.1" = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk";
"8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd"; "8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd";
"8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh"; "8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh";
"8.10+beta1" = "19wf39i0ap2vakglgdlqxpjd3l1h5w7dp460w8y7nc1y06b2153h";
}."${version}"; }."${version}";
coq-version = coq-version =
let inherit (builtins) concatStringsSep head map; in let inherit (builtins) concatStringsSep head map; in
let inherit (stdenv.lib) take splitString; in let inherit (stdenv.lib) take splitString; in
concatStringsSep "." (take 2 (map head (map (splitString "pl") (splitString "." version)))); concatStringsSep "." (take 2 (map head (map (splitString "pl") (splitString "." version))));
ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; versionAtLeast = stdenv.lib.versionAtLeast coq-version;
ideFlags = stdenv.lib.optionalString (buildIde && !versionAtLeast "8.10")
"-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt";
csdpPatch = if csdp != null then '' csdpPatch = if csdp != null then ''
substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp" substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true" substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
@ -99,7 +103,10 @@ self = stdenv.mkDerivation {
nativeBuildInputs = [ pkgconfig ]; nativeBuildInputs = [ pkgconfig ];
buildInputs = [ ncurses ] ++ (with ocamlPackages; [ ocaml findlib camlp5 num ]) buildInputs = [ ncurses ] ++ (with ocamlPackages; [ ocaml findlib camlp5 num ])
++ stdenv.lib.optional buildIde ocamlPackages.lablgtk; ++ stdenv.lib.optionals buildIde
(if versionAtLeast "8.10"
then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ]
else [ ocamlPackages.lablgtk ]);
postPatch = '' postPatch = ''
UNAME=$(type -tp uname) UNAME=$(type -tp uname)
@ -120,7 +127,9 @@ self = stdenv.mkDerivation {
addEnvHooks "$targetOffset" addCoqPath addEnvHooks "$targetOffset" addCoqPath
''; '';
preConfigure = '' preConfigure = if versionAtLeast "8.10" then ''
patchShebangs dev/tools/
'' else ''
configureFlagsArray=( configureFlagsArray=(
${ideFlags} ${ideFlags}
) )

View File

@ -27,6 +27,6 @@ stdenv.mkDerivation rec {
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
passthru = { passthru = {
compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6"; compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ];
}; };
} }

View File

@ -26,6 +26,6 @@ stdenv.mkDerivation rec {
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
passthru = { passthru = {
compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.5"; compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" ];
}; };
} }

View File

@ -32,6 +32,6 @@ stdenv.mkDerivation rec {
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
passthru = { passthru = {
compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6"; compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ];
}; };
} }

View File

@ -32,7 +32,7 @@ stdenv.mkDerivation rec {
}; };
passthru = { passthru = {
compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6"; compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ];
}; };
} }

View File

@ -24,7 +24,7 @@ stdenv.mkDerivation rec {
}; };
passthru = { passthru = {
compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6"; compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ];
}; };
} }

View File

@ -64,7 +64,7 @@ stdenv.mkDerivation rec {
}; };
passthru = { passthru = {
compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.5"; compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" ];
}; };
} }

View File

@ -28,7 +28,7 @@ stdenv.mkDerivation rec {
}; };
passthru = { passthru = {
compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.7"; compatibleCoqVersions = v: builtins.elem v [ "8.7" "8.8" "8.9" ];
}; };
} }

View File

@ -22457,6 +22457,7 @@ in
coqPackages_8_7 coq_8_7 coqPackages_8_7 coq_8_7
coqPackages_8_8 coq_8_8 coqPackages_8_8 coq_8_8
coqPackages_8_9 coq_8_9 coqPackages_8_9 coq_8_9
coqPackages_8_10 coq_8_10
coqPackages coq coqPackages coq
; ;

View File

@ -97,12 +97,16 @@ in rec {
coq_8_9 = callPackage ../applications/science/logic/coq { coq_8_9 = callPackage ../applications/science/logic/coq {
version = "8.9.0"; version = "8.9.0";
}; };
coq_8_10 = callPackage ../applications/science/logic/coq {
version = "8.10+beta1";
};
coqPackages_8_5 = mkCoqPackages coq_8_5; coqPackages_8_5 = mkCoqPackages coq_8_5;
coqPackages_8_6 = mkCoqPackages coq_8_6; coqPackages_8_6 = mkCoqPackages coq_8_6;
coqPackages_8_7 = mkCoqPackages coq_8_7; coqPackages_8_7 = mkCoqPackages coq_8_7;
coqPackages_8_8 = mkCoqPackages coq_8_8; coqPackages_8_8 = mkCoqPackages coq_8_8;
coqPackages_8_9 = mkCoqPackages coq_8_9; coqPackages_8_9 = mkCoqPackages coq_8_9;
coqPackages_8_10 = mkCoqPackages coq_8_10;
coqPackages = recurseIntoAttrs (lib.mapDerivationAttrset lib.dontDistribute coqPackages = recurseIntoAttrs (lib.mapDerivationAttrset lib.dontDistribute
coqPackages_8_8 coqPackages_8_8
); );