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/wip/yesman
parent
fde68228d9
commit
c30c5f7cf3
@ -0,0 +1,24 @@ |
||||
{stdenv, fetchurl, coq}: |
||||
|
||||
stdenv.mkDerivation { |
||||
|
||||
name = "coq-containers-${coq.coq-version}"; |
||||
|
||||
src = fetchurl { |
||||
url = http://coq.inria.fr/pylons/contribs/files/Containers/v8.4/Containers.tar.gz; |
||||
sha256 = "1y9x2lwrskv2231z9ac3kv4bmg6h1415xpp4gl7v5w90ba6p6w8w"; |
||||
}; |
||||
|
||||
buildInputs = [ coq.ocaml coq.camlp5 ]; |
||||
propagatedBuildInputs = [ coq ]; |
||||
|
||||
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; |
||||
|
||||
meta = with stdenv.lib; { |
||||
homepage = http://coq.inria.fr/pylons/pylons/contribs/view/Containers/v8.4; |
||||
description = "A typeclass-based Coq library of finite sets/maps"; |
||||
maintainers = with maintainers; [ vbgl ]; |
||||
platforms = coq.meta.platforms; |
||||
}; |
||||
|
||||
} |
@ -0,0 +1,24 @@ |
||||
{stdenv, fetchurl, coq, ssreflect}: |
||||
|
||||
stdenv.mkDerivation { |
||||
|
||||
name = "coq-mathcomp-1.5"; |
||||
|
||||
src = fetchurl { |
||||
url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.tar.gz; |
||||
sha256 = "1297svwi18blrlyd8vsqilar2h5nfixlvlifdkbx47aljq4m5bam"; |
||||
}; |
||||
|
||||
propagatedBuildInputs = [ coq ssreflect ]; |
||||
|
||||
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; |
||||
|
||||
meta = with stdenv.lib; { |
||||
homepage = http://ssr.msr-inria.inria.fr/; |
||||
license = licenses.cecill-b; |
||||
maintainers = [ maintainers.vbgl ]; |
||||
platforms = coq.meta.platforms; |
||||
hydraPlatforms = []; |
||||
}; |
||||
|
||||
} |
@ -0,0 +1,26 @@ |
||||
{stdenv, fetchurl, coq}: |
||||
|
||||
assert coq.coq-version == "8.4"; |
||||
|
||||
stdenv.mkDerivation { |
||||
|
||||
name = "coq-ssreflect-1.5"; |
||||
|
||||
src = fetchurl { |
||||
url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz; |
||||
sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds"; |
||||
}; |
||||
|
||||
buildInputs = [ coq.ocaml coq.camlp5 ]; |
||||
propagatedBuildInputs = [ coq ]; |
||||
|
||||
installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; |
||||
|
||||
meta = with stdenv.lib; { |
||||
homepage = http://ssr.msr-inria.inria.fr/; |
||||
license = licenses.cecill-b; |
||||
maintainers = with maintainers; [ vbgl ]; |
||||
platforms = coq.meta.platforms; |
||||
}; |
||||
|
||||
} |
Loading…
Reference in new issue