JakeHillion/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
82dba95079
nixpkgs/pkgs/development/coq-modules/ssreflect/default.nix

26 lines
557 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
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-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
else throw "No ssreflect package for Coq version ${coq.coq-version}"
Reference in New Issue Copy Permalink