parent
0a259ea888
commit
904bee0c46
@ -0,0 +1,26 @@ |
||||
{stdenv, fetchgit, coq}: |
||||
|
||||
stdenv.mkDerivation rec { |
||||
|
||||
name = "coq-ext-lib-${coq.coq-version}-${version}"; |
||||
version = "c2c71a2a"; |
||||
|
||||
src = fetchgit { |
||||
url = git://github.com/coq-ext-lib/coq-ext-lib.git; |
||||
rev = "c2c71a2a90ac87f2ceb311a6da53a6796b916816"; |
||||
sha256 = "01sihw3nmvvpc8viwyr01qnqifdcmlg016034xmrfmv863yp8c4g"; |
||||
}; |
||||
|
||||
buildInputs = [ coq.ocaml coq.camlp5 ]; |
||||
propagatedBuildInputs = [ coq ]; |
||||
|
||||
installFlags = "COQLIB=$out/lib/coq/${coq.coq-version}"; |
||||
|
||||
meta = with stdenv.lib; { |
||||
homepage = https://github.com/coq-ext-lib/coq-ext-lib; |
||||
description = "A collection of theories and plugins that may be useful in other Coq developments"; |
||||
maintainers = with maintainers; [ jwiegley ]; |
||||
platforms = coq.meta.platforms; |
||||
}; |
||||
|
||||
} |
@ -0,0 +1,27 @@ |
||||
{stdenv, fetchurl, coq, unzip}: |
||||
|
||||
stdenv.mkDerivation rec { |
||||
|
||||
name = "coq-heq-${coq.coq-version}-${version}"; |
||||
version = "0.92"; |
||||
|
||||
src = fetchurl { |
||||
url = "https://www.mpi-sws.org/~gil/Heq/download/Heq-${version}.zip"; |
||||
sha256 = "03y71c4qs6cmy3s2hjs05g7pcgk9sqma6flj15394yyxbvr9is1p"; |
||||
}; |
||||
|
||||
buildInputs = [ coq.ocaml coq.camlp5 unzip ]; |
||||
propagatedBuildInputs = [ coq ]; |
||||
|
||||
preBuild = "cd src"; |
||||
|
||||
installFlags = "COQLIB=$out/lib/coq/${coq.coq-version}"; |
||||
|
||||
meta = with stdenv.lib; { |
||||
homepage = https://www.mpi-sws.org/~gil/Heq/; |
||||
description = "Heq : a Coq library for Heterogeneous Equality"; |
||||
maintainers = with maintainers; [ jwiegley ]; |
||||
platforms = coq.meta.platforms; |
||||
}; |
||||
|
||||
} |
@ -0,0 +1,31 @@ |
||||
{stdenv, fetchurl, coq, unzip}: |
||||
|
||||
stdenv.mkDerivation rec { |
||||
|
||||
name = "coq-paco-${coq.coq-version}-${version}"; |
||||
version = "1.2.7"; |
||||
|
||||
src = fetchurl { |
||||
url = "http://plv.mpi-sws.org/paco/paco-${version}.zip"; |
||||
sha256 = "010fs74c0cmb9sz5dmrgzg4pmb2mgwia4gm0g9l7j2fq5xxcschb"; |
||||
}; |
||||
|
||||
buildInputs = [ coq.ocaml coq.camlp5 unzip ]; |
||||
propagatedBuildInputs = [ coq ]; |
||||
|
||||
preBuild = "cd src"; |
||||
|
||||
installPhase = '' |
||||
COQLIB=$out/lib/coq/${coq.coq-version}/ |
||||
mkdir -p $COQLIB/user-contrib/Paco |
||||
cp -pR *.vo $COQLIB/user-contrib/Paco |
||||
''; |
||||
|
||||
meta = with stdenv.lib; { |
||||
homepage = http://plv.mpi-sws.org/paco/; |
||||
description = "Paco is a Coq library implementing parameterized coinduction"; |
||||
maintainers = with maintainers; [ jwiegley ]; |
||||
platforms = coq.meta.platforms; |
||||
}; |
||||
|
||||
} |
@ -0,0 +1,33 @@ |
||||
{stdenv, fetchgit, coq}: |
||||
|
||||
stdenv.mkDerivation rec { |
||||
|
||||
name = "coq-ynot-${coq.coq-version}-${version}"; |
||||
version = "ce1a9806"; |
||||
|
||||
src = fetchgit { |
||||
url = git://github.com/Ptival/ynot.git; |
||||
rev = "ce1a9806c26ffc6e7def41da50a9aac1433cb2f8"; |
||||
sha256 = "1pcmcl5zamiimkcg1xvynxnfbv439y02vg1mnz79hqq9mnjyfnpw"; |
||||
}; |
||||
|
||||
buildInputs = [ coq.ocaml coq.camlp5 ]; |
||||
propagatedBuildInputs = [ coq ]; |
||||
|
||||
preBuild = "cd src"; |
||||
|
||||
installPhase = '' |
||||
COQLIB=$out/lib/coq/${coq.coq-version}/ |
||||
mkdir -p $COQLIB/user-contrib/Ynot |
||||
cp -pR coq/*.vo $COQLIB/user-contrib/Ynot |
||||
''; |
||||
|
||||
meta = with stdenv.lib; { |
||||
homepage = http://ynot.cs.harvard.edu/; |
||||
description = "Ynot is a library for writing and verifying imperative programs"; |
||||
maintainers = with maintainers; [ jwiegley ]; |
||||
platforms = coq.meta.platforms; |
||||
broken = true; # does not work with Coq 8.4pl4 |
||||
}; |
||||
|
||||
} |
Loading…
Reference in new issue