JakeHillion/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Merge pull request #20025 from vbgl/coq-8.5pl3

Browse Source 
Coq: 8.5pl2 -> 8.5pl3
This commit is contained in:
John Wiegley 2016-11-03 10:38:45 -07:00 committed by GitHub
commit 4008300243
4 changed files with 40 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
pkgs/applications/science/logic/coq/8.5.nix
View File

@ -2,11 +2,22 @@
# - The csdp program used for the Micromega tactic is statically referenced.
# However, coq can build without csdp by setting it to null.
# In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found.
# - The patch-level version can be specified through the `pl` argument to
# the derivation; it defaults to the greatest.
{stdenv, fetchurl, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}:
{ stdenv, fetchurl, writeText, pkgconfig
, ocaml, findlib, camlp5, ncurses
, lablgtk ? null, csdp ? null
, pl ? "3"
}:
let
version = "8.5pl2";
version = "8.5pl${pl}";
sha256 = {
"1" = "1w2xvm6w16khfn63bp95s25hnkn2ny3w0yqg3lq63gp11aqpbyjb";
"2" = "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3";
"3" = "0fyk2a4fpifibq8y8jhx1891k55qnsnlygglch64sva0bph94nrh";
}."${pl}";
coq-version = "8.5";
buildIde = lablgtk != null;
ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
@ -24,7 +35,7 @@ stdenv.mkDerivation {
src = fetchurl {
url = "http://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz";
sha256 = "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3";
inherit sha256;
};
buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ];
@ -34,7 +45,7 @@ stdenv.mkDerivation {
RM=$(type -tp rm)
substituteInPlace configure --replace "/bin/uname" "$UNAME"
substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
substituteInPlace configure.ml --replace "if arch = \"Darwin\" || arch = \"FreeBSD\" then \"md5" "if arch = \"Darwinx\" then \"md5"
substituteInPlace configure.ml --replace '"md5 -q"' '"md5sum"'
${csdpPatch}
'';
@ -57,7 +68,11 @@ stdenv.mkDerivation {
prefixKey = "-prefix ";
buildFlags = "revision coq coqide";
buildFlags = "revision coq coqide bin/votour";
postInstall = ''
cp bin/votour $out/bin/
'';
meta = with stdenv.lib; {
description = "Coq proof assistant";

1
pkgs/development/compilers/compcert/default.nix
View File

@ -19,6 +19,7 @@ stdenv.mkDerivation rec {
enableParallelBuilding = true;
configurePhase = ''
substituteInPlace ./configure --replace pl2 pl3
substituteInPlace ./configure --replace '{toolprefix}gcc' '{toolprefix}cc'
./configure -prefix $out -toolprefix ${tools}/bin/ '' +
(if stdenv.isDarwin then "ia32-macosx" else "ia32-linux");

22
pkgs/top-level/all-packages.nix
View File

@ -16487,13 +16487,27 @@ in
aspino = callPackage ../applications/science/logic/aspino {};
inherit (ocaml-ng.ocamlPackages_4_01_0) coq;
coq = callPackage ../applications/science/logic/coq {
inherit (ocamlPackages_4_01_0) ocaml findlib lablgtk;
camlp5 = ocamlPackages_4_01_0.camlp5_transitional;
};
inherit (ocamlPackages) coq_HEAD;
coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {
inherit (ocamlPackages) ocaml findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;
};
inherit (ocamlPackages) coq_8_5;
coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix {
inherit (ocamlPackages) ocaml findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;
};
inherit (ocaml-ng.ocamlPackages_3_12_1) coq_8_3;
coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
make = pkgs.gnumake3;
inherit (ocamlPackages_3_12_1) ocaml findlib;
camlp5 = ocamlPackages_3_12_1.camlp5_transitional;
lablgtk = ocamlPackages_3_12_1.lablgtk_2_14;
};
mkCoqPackages_8_4 = self: let callPackage = newScope self; in {

20
pkgs/top-level/ocaml-packages.nix
View File

@ -630,7 +630,7 @@ let
then { tools = pkgs.pkgsi686Linux.stdenv.cc; }
else {}
) // {
coq = coq_8_5;
coq = pkgs.coq_8_5;
});
haxe = callPackage ../development/compilers/haxe { };
@ -672,24 +672,6 @@ let
enableX11 = config.unison.enableX11 or true;
};
coq = callPackage ../applications/science/logic/coq {
camlp5 = camlp5_transitional;
};
coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {
camlp5 = camlp5_transitional;
};
coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix {
camlp5 = camlp5_transitional;
};
coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
make = pkgs.gnumake3;
camlp5 = camlp5_transitional;
lablgtk = lablgtk_2_14;
};
hol_light = callPackage ../applications/science/logic/hol_light {
camlp5 = camlp5_strict;
};