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

coq_8_6: 8.6 is now default, 8.4 optional, updated mathcomp/ssreflect

Browse Source 
Addresses #14829
This commit is contained in:
John Wiegley 2016-12-22 10:34:56 -08:00
parent 603dbfc5a9
commit 4888bfecc2
No known key found for this signature in database
GPG Key ID: C144D8F4F19FE630
6 changed files with 82 additions and 84 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

0
pkgs/applications/science/logic/coq/default.nix → pkgs/applications/science/logic/coq/8.4.nix
View File

31
pkgs/development/coq-modules/mathcomp/default.nix
View File

@ -1,24 +1,39 @@
{ callPackage, coq, fetchurl }: { callPackage, fetchurl, coq }:
let src =
if coq.coq-version == "8.4" then if coq.coq-version == "8.4" then
fetchurl { callPackage ./generic.nix {
name = "coq-mathcomp-1.6-${coq.coq-version}";
src = fetchurl {
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz; url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8"; sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
};
} }
else if coq.coq-version == "8.5" then else if coq.coq-version == "8.5" then
fetchurl { callPackage ./generic.nix {
name = "coq-mathcomp-1.6-${coq.coq-version}";
src = fetchurl {
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz; url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8"; sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
};
} }
else throw "No mathcomp package for Coq version ${coq.coq-version}"; else if coq.coq-version == "8.6" then
in
callPackage ./generic.nix { callPackage ./generic.nix {
inherit src;
name = "coq-mathcomp-1.6.1-${coq.coq-version}";
src = fetchurl {
url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw";
};
} }
else throw "No ssreflect package for Coq version ${coq.coq-version}"

5
pkgs/development/coq-modules/mathcomp/generic.nix
View File

@ -1,12 +1,11 @@
{ stdenv, fetchurl, coq, ssreflect, ncurses, which { stdenv, fetchurl, coq, ssreflect, ncurses, which
, graphviz, ocamlPackages, withDoc ? false , graphviz, ocamlPackages, withDoc ? false
, src , src, name
}: }:
stdenv.mkDerivation { stdenv.mkDerivation {
name = "coq-mathcomp-1.6-${coq.coq-version}"; inherit name;
inherit src; inherit src;
nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ]; nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];

14
pkgs/development/coq-modules/ssreflect/default.nix
View File

@ -4,6 +4,7 @@ if coq.coq-version == "8.4" then
callPackage ./generic.nix { callPackage ./generic.nix {
name = "coq-ssreflect-1.6-${coq.coq-version}";
src = fetchurl { src = fetchurl {
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz; url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8"; sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
@ -15,6 +16,7 @@ else if coq.coq-version == "8.5" then
callPackage ./generic.nix { callPackage ./generic.nix {
name = "coq-ssreflect-1.6-${coq.coq-version}";
src = fetchurl { src = fetchurl {
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz; url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8"; sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
@ -22,4 +24,16 @@ callPackage ./generic.nix {
} }
else if coq.coq-version == "8.6" then
callPackage ./generic.nix {
name = "coq-ssreflect-1.6.1-${coq.coq-version}";
src = fetchurl {
url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw";
};
}
else throw "No ssreflect package for Coq version ${coq.coq-version}" else throw "No ssreflect package for Coq version ${coq.coq-version}"

5
pkgs/development/coq-modules/ssreflect/generic.nix
View File

@ -1,12 +1,11 @@
{ stdenv, fetchurl, coq, ncurses, which { stdenv, fetchurl, coq, ncurses, which
, graphviz, withDoc ? false , graphviz, withDoc ? false
, src, patches ? [] , src, name, patches ? []
}: }:
stdenv.mkDerivation { stdenv.mkDerivation {
name = "coq-ssreflect-1.6-${coq.coq-version}"; inherit name;
inherit src; inherit src;
nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ]; nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];

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

@ -6603,7 +6603,9 @@ in
valkyrie = callPackage ../development/tools/analysis/valkyrie { }; valkyrie = callPackage ../development/tools/analysis/valkyrie { };
inherit (ocaml-ng.ocamlPackages_4_02) verasco; verasco = ocaml-ng.ocamlPackages_4_02.verasco.override {
coq = coq_8_4;
};
visualvm = callPackage ../development/tools/java/visualvm { }; visualvm = callPackage ../development/tools/java/visualvm { };
@ -16716,38 +16718,34 @@ in
aspino = callPackage ../applications/science/logic/aspino {}; aspino = callPackage ../applications/science/logic/aspino {};
coq = callPackage ../applications/science/logic/coq {
inherit (ocamlPackages_4_01_0) ocaml findlib lablgtk;
camlp5 = ocamlPackages_4_01_0.camlp5_transitional;
};
coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {
inherit (ocamlPackages) ocaml findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;
};
coq_8_6 = callPackage ../applications/science/logic/coq/8.6.nix {
inherit (ocamlPackages) ocaml findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;
};
coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix {
inherit (ocamlPackages) ocaml findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;
};
coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix { coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
make = pkgs.gnumake3; make = pkgs.gnumake3;
inherit (ocamlPackages_3_12_1) ocaml findlib; inherit (ocamlPackages_3_12_1) ocaml findlib;
camlp5 = ocamlPackages_3_12_1.camlp5_transitional; camlp5 = ocamlPackages_3_12_1.camlp5_transitional;
lablgtk = ocamlPackages_3_12_1.lablgtk_2_14; lablgtk = ocamlPackages_3_12_1.lablgtk_2_14;
}; };
coq_8_4 = callPackage ../applications/science/logic/coq/8.4.nix {
inherit (ocamlPackages_4_01_0) ocaml findlib lablgtk;
camlp5 = ocamlPackages_4_01_0.camlp5_transitional;
};
coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix {
inherit (ocamlPackages) ocaml findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;
};
coq_8_6 = callPackage ../applications/science/logic/coq/8.6.nix {
inherit (ocamlPackages) ocaml findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;
};
coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {
inherit (ocamlPackages) ocaml findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;
};
coq = coq_8_6;
mkCoqPackages_8_4 = self: let callPackage = newScope self; in { mkCoqPackages_8_4 = self: let callPackage = newScope self; in {
inherit callPackage; inherit callPackage;
coq = coq_8_4;
bedrock = callPackage ../development/coq-modules/bedrock {}; coqPackages = coqPackages_8_4;
contribs = contribs =
let contribs = let contribs =
@ -16757,86 +16755,59 @@ in
in in
recurseIntoAttrs contribs; recurseIntoAttrs contribs;
bedrock = callPackage ../development/coq-modules/bedrock {};
coqExtLib = callPackage ../development/coq-modules/coq-ext-lib {}; coqExtLib = callPackage ../development/coq-modules/coq-ext-lib {};
coqeal = callPackage ../development/coq-modules/coqeal {}; coqeal = callPackage ../development/coq-modules/coqeal {};
coquelicot = callPackage ../development/coq-modules/coquelicot {}; coquelicot = callPackage ../development/coq-modules/coquelicot {};
domains = callPackage ../development/coq-modules/domains {}; domains = callPackage ../development/coq-modules/domains {};
fiat = callPackage ../development/coq-modules/fiat {}; fiat = callPackage ../development/coq-modules/fiat {};
fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {}; fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
flocq = callPackage ../development/coq-modules/flocq {}; flocq = callPackage ../development/coq-modules/flocq {};
heq = callPackage ../development/coq-modules/heq {}; heq = callPackage ../development/coq-modules/heq {};
interval = callPackage ../development/coq-modules/interval {}; interval = callPackage ../development/coq-modules/interval {};
mathcomp = callPackage ../development/coq-modules/mathcomp {}; mathcomp = callPackage ../development/coq-modules/mathcomp {};
paco = callPackage ../development/coq-modules/paco {}; paco = callPackage ../development/coq-modules/paco {};
QuickChick = callPackage ../development/coq-modules/QuickChick {}; QuickChick = callPackage ../development/coq-modules/QuickChick {};
ssreflect = callPackage ../development/coq-modules/ssreflect {}; ssreflect = callPackage ../development/coq-modules/ssreflect {};
tlc = callPackage ../development/coq-modules/tlc {}; tlc = callPackage ../development/coq-modules/tlc {};
unimath = callPackage ../development/coq-modules/unimath {}; unimath = callPackage ../development/coq-modules/unimath {};
ynot = callPackage ../development/coq-modules/ynot {}; ynot = callPackage ../development/coq-modules/ynot {};
}; };
mkCoqPackages_8_5 = self: let callPackage = newScope self; in rec { mkCoqPackages_8_5 = self: let callPackage = newScope self; in rec {
inherit callPackage; inherit callPackage;
coq = coq_8_5; coq = coq_8_5;
coqPackages = coqPackages_8_5;
coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {}; coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
coquelicot = callPackage ../development/coq-modules/coquelicot {}; coquelicot = callPackage ../development/coq-modules/coquelicot {};
dpdgraph = callPackage ../development/coq-modules/dpdgraph {}; dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
flocq = callPackage ../development/coq-modules/flocq {}; flocq = callPackage ../development/coq-modules/flocq {};
interval = callPackage ../development/coq-modules/interval {}; interval = callPackage ../development/coq-modules/interval {};
mathcomp = callPackage ../development/coq-modules/mathcomp { }; mathcomp = callPackage ../development/coq-modules/mathcomp { };
ssreflect = callPackage ../development/coq-modules/ssreflect { }; ssreflect = callPackage ../development/coq-modules/ssreflect { };
fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {}; fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
}; };
mkCoqPackages_8_6 = self: let callPackage = newScope self; in rec { mkCoqPackages_8_6 = self: let callPackage = newScope self; in rec {
inherit callPackage; inherit callPackage;
coq = coq_8_6; coq = coq_8_6;
coqPackages = coqPackages_8_6;
coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {}; coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
coquelicot = callPackage ../development/coq-modules/coquelicot {}; coquelicot = callPackage ../development/coq-modules/coquelicot {};
dpdgraph = callPackage ../development/coq-modules/dpdgraph {}; dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
flocq = callPackage ../development/coq-modules/flocq {}; flocq = callPackage ../development/coq-modules/flocq {};
interval = callPackage ../development/coq-modules/interval {}; interval = callPackage ../development/coq-modules/interval {};
mathcomp = callPackage ../development/coq-modules/mathcomp { };
ssreflect = callPackage ../development/coq-modules/ssreflect { };
fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {}; fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
}; };
coqPackages = mkCoqPackages_8_4 coqPackages; coqPackages_8_4 = mkCoqPackages_8_4 coqPackages_8_4;
coqPackages_8_5 = mkCoqPackages_8_5 coqPackages_8_5; coqPackages_8_5 = mkCoqPackages_8_5 coqPackages_8_5;
coqPackages_8_6 = mkCoqPackages_8_6 coqPackages_8_6; coqPackages_8_6 = mkCoqPackages_8_6 coqPackages_8_6;
coqPackages = coqPackages_8_6;
cryptoverif = callPackage ../applications/science/logic/cryptoverif { }; cryptoverif = callPackage ../applications/science/logic/cryptoverif { };