alioth/nixpkgs
3
0
Fork 0
forked from mirrors/nixpkgs
Code Releases Activity
nixpkgs/pkgs/development/coq-modules/ssreflect/default.nix

40 lines
951 B
Nix
Raw Normal View History

coq-ssreflect: refactor
2015-05-28 15:09:05 +01:00
{ callPackage, fetchurl, coq }:
Adds three coq libraries: containers, mathcomp, ssreflect Containers is a reimplementation of the FSets/FMaps library from the standard library, using typeclasses. Homepage: http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4 The Mathematical Components (mathcomp) contains advanced theory files covering a wide spectrum of mathematics. Homepage: http://ssr.msr-inria.inria.fr/ Ssreflect is a proof language (plugin for Coq) and a small set of core theory libraries about boolean, natural numbers, sequences, decidable equality and finite types. Homepage: http://ssr.msr-inria.inria.fr/
2014-09-28 12:43:48 +01:00
coq-ssreflect: refactor
2015-05-28 15:09:05 +01:00
if coq.coq-version == "8.4" then
Adds three coq libraries: containers, mathcomp, ssreflect Containers is a reimplementation of the FSets/FMaps library from the standard library, using typeclasses. Homepage: http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4 The Mathematical Components (mathcomp) contains advanced theory files covering a wide spectrum of mathematics. Homepage: http://ssr.msr-inria.inria.fr/ Ssreflect is a proof language (plugin for Coq) and a small set of core theory libraries about boolean, natural numbers, sequences, decidable equality and finite types. Homepage: http://ssr.msr-inria.inria.fr/
2014-09-28 12:43:48 +01:00
coq-ssreflect: refactor
2015-05-28 15:09:05 +01:00
callPackage ./generic.nix {
Adds three coq libraries: containers, mathcomp, ssreflect Containers is a reimplementation of the FSets/FMaps library from the standard library, using typeclasses. Homepage: http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4 The Mathematical Components (mathcomp) contains advanced theory files covering a wide spectrum of mathematics. Homepage: http://ssr.msr-inria.inria.fr/ Ssreflect is a proof language (plugin for Coq) and a small set of core theory libraries about boolean, natural numbers, sequences, decidable equality and finite types. Homepage: http://ssr.msr-inria.inria.fr/
2014-09-28 12:43:48 +01:00
coq_8_6: 8.6 is now default, 8.4 optional, updated mathcomp/ssreflect Addresses #14829
2016-12-22 18:34:56 +00:00
name = "coq-ssreflect-1.6-${coq.coq-version}";
Adds three coq libraries: containers, mathcomp, ssreflect Containers is a reimplementation of the FSets/FMaps library from the standard library, using typeclasses. Homepage: http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4 The Mathematical Components (mathcomp) contains advanced theory files covering a wide spectrum of mathematics. Homepage: http://ssr.msr-inria.inria.fr/ Ssreflect is a proof language (plugin for Coq) and a small set of core theory libraries about boolean, natural numbers, sequences, decidable equality and finite types. Homepage: http://ssr.msr-inria.inria.fr/
2014-09-28 12:43:48 +01:00
src = fetchurl {
coqPackages.mathcomp,ssreflect: 1.5 -> 1.6 See the INSTALL file in the mathcomp package for instructions on upgrading projects from 1.5 to 1.6. The 1.6 version works with both Coq 8.4 and 8.5.
2015-12-20 19:12:23 +00:00
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
Adds three coq libraries: containers, mathcomp, ssreflect Containers is a reimplementation of the FSets/FMaps library from the standard library, using typeclasses. Homepage: http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4 The Mathematical Components (mathcomp) contains advanced theory files covering a wide spectrum of mathematics. Homepage: http://ssr.msr-inria.inria.fr/ Ssreflect is a proof language (plugin for Coq) and a small set of core theory libraries about boolean, natural numbers, sequences, decidable equality and finite types. Homepage: http://ssr.msr-inria.inria.fr/
2014-09-28 12:43:48 +01:00
};
coq-ssreflect: refactor
2015-05-28 15:09:05 +01:00
}
coq-ssreflect: also build and install the documentation
2015-05-28 13:10:39 +01:00
coq-ssreflect: refactor
2015-05-28 15:09:05 +01:00
else if coq.coq-version == "8.5" then
Adds three coq libraries: containers, mathcomp, ssreflect Containers is a reimplementation of the FSets/FMaps library from the standard library, using typeclasses. Homepage: http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4 The Mathematical Components (mathcomp) contains advanced theory files covering a wide spectrum of mathematics. Homepage: http://ssr.msr-inria.inria.fr/ Ssreflect is a proof language (plugin for Coq) and a small set of core theory libraries about boolean, natural numbers, sequences, decidable equality and finite types. Homepage: http://ssr.msr-inria.inria.fr/
2014-09-28 12:43:48 +01:00
coq-ssreflect: refactor
2015-05-28 15:09:05 +01:00
callPackage ./generic.nix {
coqPackages.ssreflect, more: build ssrcoq binary, add maintainer
2014-10-13 22:10:19 +01:00
coq_8_6: 8.6 is now default, 8.4 optional, updated mathcomp/ssreflect Addresses #14829
2016-12-22 18:34:56 +00:00
name = "coq-ssreflect-1.6-${coq.coq-version}";
coq-ssreflect: refactor
2015-05-28 15:09:05 +01:00
src = fetchurl {
coqPackages.mathcomp,ssreflect: 1.5 -> 1.6 See the INSTALL file in the mathcomp package for instructions on upgrading projects from 1.5 to 1.6. The 1.6 version works with both Coq 8.4 and 8.5.
2015-12-20 19:12:23 +00:00
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
Adds three coq libraries: containers, mathcomp, ssreflect Containers is a reimplementation of the FSets/FMaps library from the standard library, using typeclasses. Homepage: http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4 The Mathematical Components (mathcomp) contains advanced theory files covering a wide spectrum of mathematics. Homepage: http://ssr.msr-inria.inria.fr/ Ssreflect is a proof language (plugin for Coq) and a small set of core theory libraries about boolean, natural numbers, sequences, decidable equality and finite types. Homepage: http://ssr.msr-inria.inria.fr/
2014-09-28 12:43:48 +01:00
};
}
coq-ssreflect: refactor
2015-05-28 15:09:05 +01:00
coq_8_6: 8.6 is now default, 8.4 optional, updated mathcomp/ssreflect Addresses #14829
2016-12-22 18:34:56 +00:00
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";
};
}
coq-ssreflect: refactor
2015-05-28 15:09:05 +01:00
else throw "No ssreflect package for Coq version ${coq.coq-version}"
Copy permalink