diff options
Diffstat (limited to 'nixpkgs/pkgs/development/coq-modules')
23 files changed, 66 insertions, 41 deletions
diff --git a/nixpkgs/pkgs/development/coq-modules/CoLoR/default.nix b/nixpkgs/pkgs/development/coq-modules/CoLoR/default.nix index d145586af43b..1346ec92fade 100644 --- a/nixpkgs/pkgs/development/coq-modules/CoLoR/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/CoLoR/default.nix @@ -45,7 +45,7 @@ stdenv.mkDerivation { ''; meta = with stdenv.lib; { - homepage = http://color.inria.fr/; + homepage = "http://color.inria.fr/"; description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant."; maintainers = with maintainers; [ jpas jwiegley ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/HoTT/default.nix b/nixpkgs/pkgs/development/coq-modules/HoTT/default.nix index fb01da8d59cc..7b52838505e2 100644 --- a/nixpkgs/pkgs/development/coq-modules/HoTT/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/HoTT/default.nix @@ -49,7 +49,7 @@ stdenv.mkDerivation rec { ]; meta = with stdenv.lib; { - homepage = http://homotopytypetheory.org/; + homepage = "http://homotopytypetheory.org/"; description = "Homotopy type theory"; maintainers = with maintainers; [ siddharthist ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix b/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix index c1894d3666c6..7f3c77c75e61 100644 --- a/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix @@ -65,7 +65,7 @@ stdenv.mkDerivation { ''; meta = with stdenv.lib; { - homepage = https://github.com/QuickChick/QuickChick; + homepage = "https://github.com/QuickChick/QuickChick"; description = "Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck"; maintainers = with maintainers; [ jwiegley ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/autosubst/default.nix b/nixpkgs/pkgs/development/coq-modules/autosubst/default.nix index ee08af40c51e..9507dc6751ae 100644 --- a/nixpkgs/pkgs/development/coq-modules/autosubst/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/autosubst/default.nix @@ -6,7 +6,7 @@ stdenv.mkDerivation rec { version = "5b40a32e"; src = fetchgit { - url = git://github.com/uds-psl/autosubst.git; + url = "git://github.com/uds-psl/autosubst.git"; rev = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034"; sha256 = "06pcjbngzwqyncvfwzz88j33wvdj9kizxyg5adp7y6186h8an341"; }; @@ -19,7 +19,7 @@ stdenv.mkDerivation rec { installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; meta = with stdenv.lib; { - homepage = https://www.ps.uni-saarland.de/autosubst/; + homepage = "https://www.ps.uni-saarland.de/autosubst/"; description = "Automation for de Bruijn syntax and substitution in Coq"; maintainers = with maintainers; [ jwiegley ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix b/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix index 025a67a1e70b..1178b1558ff7 100644 --- a/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix @@ -27,7 +27,7 @@ stdenv.mkDerivation { name = "coq${coq.coq-version}-category-theory-${param.version}"; src = fetchgit { - url = git://github.com/jwiegley/category-theory.git; + url = "git://github.com/jwiegley/category-theory.git"; inherit (param) rev sha256; }; @@ -41,7 +41,7 @@ stdenv.mkDerivation { ''; meta = with stdenv.lib; { - homepage = https://github.com/jwiegley/category-theory; + homepage = "https://github.com/jwiegley/category-theory"; description = "A formalization of category theory in Coq for personal study and practical work"; maintainers = with maintainers; [ jwiegley ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/coq-bits/default.nix b/nixpkgs/pkgs/development/coq-modules/coq-bits/default.nix index ed6118dbb55d..97fd23208f2f 100644 --- a/nixpkgs/pkgs/development/coq-modules/coq-bits/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/coq-bits/default.nix @@ -25,7 +25,7 @@ stdenv.mkDerivation { ''; meta = with stdenv.lib; { - homepage = https://github.com/coq-community/coq-bits; + homepage = "https://github.com/coq-community/coq-bits"; description = "A formalization of bitset operations in Coq"; license = licenses.asl20; maintainers = with maintainers; [ ptival ]; diff --git a/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix b/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix index 8bbf74b60784..17f9c2c46114 100644 --- a/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix @@ -33,7 +33,7 @@ stdenv.mkDerivation rec { installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; meta = with stdenv.lib; { - homepage = https://github.com/coq-ext-lib/coq-ext-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 ptival ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/coq-extensible-records/default.nix b/nixpkgs/pkgs/development/coq-modules/coq-extensible-records/default.nix index 3b93b6b2de22..531c15287616 100644 --- a/nixpkgs/pkgs/development/coq-modules/coq-extensible-records/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/coq-extensible-records/default.nix @@ -45,7 +45,7 @@ stdenv.mkDerivation rec { ''; meta = with stdenv.lib; { - homepage = https://github.com/gmalecha/coq-extensible-records; + homepage = "https://github.com/gmalecha/coq-extensible-records"; description = "Implementation of extensible records in Coq"; license = licenses.mit; maintainers = with maintainers; [ ptival ]; diff --git a/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix b/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix index e9263fb2be1e..7c86a7d55f34 100644 --- a/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix @@ -34,7 +34,7 @@ stdenv.mkDerivation { name = "coq${coq.coq-version}-coq-haskell-${param.version}"; src = fetchgit { - url = git://github.com/jwiegley/coq-haskell.git; + url = "git://github.com/jwiegley/coq-haskell.git"; inherit (param) rev sha256; }; @@ -48,7 +48,7 @@ stdenv.mkDerivation { ''; meta = with stdenv.lib; { - homepage = https://github.com/jwiegley/coq-haskell; + homepage = "https://github.com/jwiegley/coq-haskell"; description = "A library for formalizing Haskell types and functions in Coq"; maintainers = with maintainers; [ jwiegley ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix b/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix index 83a505017fbc..7d9ec5e7312b 100644 --- a/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix @@ -3,17 +3,25 @@ let params = { "8.8" = { + version = "1.1"; sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h"; + buildInputs = [ coq.ocamlPackages.camlp5 ]; }; "8.9" = { - sha256 = "0hmqwsry8ldg4g4hhwg4b84dgzibpdrg1wwsajhlyqfx3fb3n3b5"; + version = "1.1.1"; + sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9"; + buildInputs = [ coq.ocamlPackages.camlp5 ]; + }; + "8.10" = { + version = "1.1.1"; + sha256 = "0b6r7bsygl1axbqybkhkr7zlwcd51ski5ql52994klrrxvjd58df"; }; }; param = params.${coq.coq-version}; in stdenv.mkDerivation rec { - version = "1.1"; + inherit (param) version; name = "coq${coq.coq-version}-coqhammer-${version}"; src = fetchFromGitHub { @@ -31,8 +39,8 @@ stdenv.mkDerivation rec { ''; buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ - ocaml findlib camlp5 - ]); + ocaml findlib + ]) ++ (param.buildInputs or []); preInstall = '' mkdir -p $out/bin diff --git a/nixpkgs/pkgs/development/coq-modules/coquelicot/default.nix b/nixpkgs/pkgs/development/coq-modules/coquelicot/default.nix index 3b916b5e40bb..2eb3021ada73 100644 --- a/nixpkgs/pkgs/development/coq-modules/coquelicot/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/coquelicot/default.nix @@ -29,7 +29,7 @@ stdenv.mkDerivation { installPhase = "./remake install"; meta = { - homepage = http://coquelicot.saclay.inria.fr/; + homepage = "http://coquelicot.saclay.inria.fr/"; description = "A Coq library for Reals"; license = stdenv.lib.licenses.lgpl3; maintainers = [ stdenv.lib.maintainers.vbgl ]; diff --git a/nixpkgs/pkgs/development/coq-modules/corn/default.nix b/nixpkgs/pkgs/development/coq-modules/corn/default.nix index 97bb884c92e2..14ff74506f37 100644 --- a/nixpkgs/pkgs/development/coq-modules/corn/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/corn/default.nix @@ -24,7 +24,7 @@ stdenv.mkDerivation rec { installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; meta = { - homepage = http://c-corn.github.io/; + homepage = "http://c-corn.github.io/"; license = stdenv.lib.licenses.gpl2; description = "A Coq library for constructive analysis"; maintainers = [ stdenv.lib.maintainers.vbgl ]; diff --git a/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix b/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix index 300c5a9f4482..689745003df2 100644 --- a/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix @@ -36,6 +36,8 @@ let params = { param = params.${coq.coq-version}; in +let hasWarning = stdenv.lib.versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in + stdenv.mkDerivation { name = "coq${coq.coq-version}-dpdgraph-${param.version}"; src = fetchFromGitHub { @@ -49,6 +51,14 @@ stdenv.mkDerivation { buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml camlp5 findlib ocamlgraph ]); + # dpd_compute.ml uses deprecated Pervasives.compare + # Versions prior to 0.6.5 do not have the WARN_ERR build flag + preConfigure = stdenv.lib.optionalString hasWarning '' + substituteInPlace Makefile.in --replace "-warn-error +a " "" + ''; + + buildFlags = stdenv.lib.optional hasWarning "WARN_ERR="; + preInstall = '' mkdir -p $out/bin ''; @@ -61,7 +71,7 @@ stdenv.mkDerivation { meta = { description = "Build dependency graphs between Coq objects"; license = stdenv.lib.licenses.lgpl21; - homepage = https://github.com/Karmaki/coq-dpdgraph/; + homepage = "https://github.com/Karmaki/coq-dpdgraph/"; maintainers = with stdenv.lib.maintainers; [ vbgl ]; platforms = coq.meta.platforms; }; diff --git a/nixpkgs/pkgs/development/coq-modules/equations/default.nix b/nixpkgs/pkgs/development/coq-modules/equations/default.nix index 9ea9ac216718..c1177dc9789f 100644 --- a/nixpkgs/pkgs/development/coq-modules/equations/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/equations/default.nix @@ -54,7 +54,7 @@ stdenv.mkDerivation rec { installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; meta = with stdenv.lib; { - homepage = https://mattam82.github.io/Coq-Equations/; + homepage = "https://mattam82.github.io/Coq-Equations/"; description = "A plugin for Coq to add dependent pattern-matching"; maintainers = with maintainers; [ jwiegley ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/fiat/HEAD.nix b/nixpkgs/pkgs/development/coq-modules/fiat/HEAD.nix index 4abaec6528a9..fd3ade0c64b5 100644 --- a/nixpkgs/pkgs/development/coq-modules/fiat/HEAD.nix +++ b/nixpkgs/pkgs/development/coq-modules/fiat/HEAD.nix @@ -27,7 +27,7 @@ stdenv.mkDerivation rec { ''; meta = with stdenv.lib; { - homepage = http://plv.csail.mit.edu/fiat/; + homepage = "http://plv.csail.mit.edu/fiat/"; description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications"; maintainers = with maintainers; [ jwiegley ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/flocq/default.nix b/nixpkgs/pkgs/development/coq-modules/flocq/default.nix index d9ad7d6e3be1..e0c32bc430ed 100644 --- a/nixpkgs/pkgs/development/coq-modules/flocq/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/flocq/default.nix @@ -36,7 +36,7 @@ stdenv.mkDerivation rec { ''; meta = with stdenv.lib; { - homepage = http://flocq.gforge.inria.fr/; + homepage = "http://flocq.gforge.inria.fr/"; description = "A floating-point formalization for the Coq system"; license = licenses.lgpl3; maintainers = with maintainers; [ jwiegley ]; diff --git a/nixpkgs/pkgs/development/coq-modules/gappalib/default.nix b/nixpkgs/pkgs/development/coq-modules/gappalib/default.nix index c610039eeec9..c432d2175ece 100644 --- a/nixpkgs/pkgs/development/coq-modules/gappalib/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/gappalib/default.nix @@ -3,7 +3,7 @@ stdenv.mkDerivation { name = "coq${coq.coq-version}-gappalib-1.4.1"; src = fetchurl { - url = https://gforge.inria.fr/frs/download.php/file/37917/gappalib-coq-1.4.1.tar.gz; + url = "https://gforge.inria.fr/frs/download.php/file/37917/gappalib-coq-1.4.1.tar.gz"; sha256 = "0d3f23a871haglg8hq1jgxz3y5nryiwy12b5xfnfjn279jfqqjw4"; }; @@ -18,7 +18,7 @@ stdenv.mkDerivation { meta = { description = "Coq support library for Gappa"; license = stdenv.lib.licenses.lgpl21; - homepage = http://gappa.gforge.inria.fr/; + homepage = "http://gappa.gforge.inria.fr/"; maintainers = [ stdenv.lib.maintainers.vbgl ]; inherit (coq.meta) platforms; }; diff --git a/nixpkgs/pkgs/development/coq-modules/heq/default.nix b/nixpkgs/pkgs/development/coq-modules/heq/default.nix index 5d3c94c5f5c8..d0445c83ca59 100644 --- a/nixpkgs/pkgs/development/coq-modules/heq/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/heq/default.nix @@ -18,7 +18,7 @@ stdenv.mkDerivation rec { installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}" ]; meta = with stdenv.lib; { - homepage = https://www.mpi-sws.org/~gil/Heq/; + homepage = "https://www.mpi-sws.org/~gil/Heq/"; description = "Heq : a Coq library for Heterogeneous Equality"; maintainers = with maintainers; [ jwiegley ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/interval/default.nix b/nixpkgs/pkgs/development/coq-modules/interval/default.nix index 73a0a07f704c..9e78a9f38829 100644 --- a/nixpkgs/pkgs/development/coq-modules/interval/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/interval/default.nix @@ -30,7 +30,7 @@ stdenv.mkDerivation { installPhase = "./remake install"; meta = with stdenv.lib; { - homepage = http://coq-interval.gforge.inria.fr/; + homepage = "http://coq-interval.gforge.inria.fr/"; description = "Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant"; license = licenses.cecill-c; maintainers = with maintainers; [ vbgl ]; diff --git a/nixpkgs/pkgs/development/coq-modules/math-classes/default.nix b/nixpkgs/pkgs/development/coq-modules/math-classes/default.nix index 7aad4261fd32..9ab77418cce1 100644 --- a/nixpkgs/pkgs/development/coq-modules/math-classes/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/math-classes/default.nix @@ -17,7 +17,7 @@ stdenv.mkDerivation rec { installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; meta = with stdenv.lib; { - homepage = https://math-classes.github.io; + homepage = "https://math-classes.github.io"; description = "A library of abstract interfaces for mathematical structures in Coq."; maintainers = with maintainers; [ siddharthist jwiegley ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/metalib/default.nix b/nixpkgs/pkgs/development/coq-modules/metalib/default.nix index c196bdbcd766..a0268a543a5a 100644 --- a/nixpkgs/pkgs/development/coq-modules/metalib/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/metalib/default.nix @@ -6,7 +6,7 @@ stdenv.mkDerivation rec { version = "20170713"; src = fetchgit { - url = https://github.com/plclub/metalib.git; + url = "https://github.com/plclub/metalib.git"; rev = "44e40aa082452dd333fc1ca2d2cc55311519bd52"; sha256 = "1pra0nvx69q8d4bvpcvh9ngic1cy6z1chi03x56nisfqnc61b6y9"; }; @@ -16,7 +16,7 @@ stdenv.mkDerivation rec { pname = "lngen"; version = "0.0.1"; src = fetchgit { - url = https://github.com/plclub/lngen; + url = "https://github.com/plclub/lngen"; rev = "ea73ad315de33afd25f87ca738c71f358f1cd51c"; sha256 = "1a0sj8n3lmsl1wlnqfy176k9lb9s8rl422bvg3ihl2i70ql8wisd"; }; @@ -24,7 +24,7 @@ stdenv.mkDerivation rec { isExecutable = true; libraryHaskellDepends = [ base containers mtl parsec syb ]; executableHaskellDepends = [ base ]; - homepage = https://github.com/plclub/lngen; + homepage = "https://github.com/plclub/lngen"; description = "Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott"; license = stdenv.lib.licenses.mit; }; @@ -43,7 +43,7 @@ stdenv.mkDerivation rec { ''; meta = with stdenv.lib; { - homepage = https://github.com/plclub/metalib; + homepage = "https://github.com/plclub/metalib"; license = licenses.mit; maintainers = [ maintainers.jwiegley ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/paco/default.nix b/nixpkgs/pkgs/development/coq-modules/paco/default.nix index 4c0ca4673005..9d8a7a315a55 100644 --- a/nixpkgs/pkgs/development/coq-modules/paco/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/paco/default.nix @@ -47,7 +47,7 @@ stdenv.mkDerivation rec { ''; meta = with stdenv.lib; { - homepage = http://plv.mpi-sws.org/paco/; + homepage = "http://plv.mpi-sws.org/paco/"; description = "A Coq library implementing parameterized coinduction"; maintainers = with maintainers; [ jwiegley ptival ]; platforms = coq.meta.platforms; diff --git a/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix b/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix index a57d1bc9088d..67e420b4e89e 100644 --- a/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix +++ b/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix @@ -3,33 +3,40 @@ let params = { "8.7" = { - version = "1.1.1+coq8.7"; - sha256 = "1i7b5pkx46zf9il2xikbp3rhpnh3wdfbhw5yxcf9yk28ky9s0a0l"; + sha256 = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj"; + buildInputs = [ coq.ocamlPackages.camlp5 ]; }; "8.8" = { - version = "1.1.1"; - sha256 = "0b07zvgm9cx6j2d9631zmqjs6sf30kiqg6k15xk3km7n80d53wfh"; + sha256 = "0rc4lshqvnfdsph98gnscvpmlirs9wx91qcvffggg73xw0p1g9s0"; + buildInputs = [ coq.ocamlPackages.camlp5 ]; }; "8.9" = { - version = "1.1.1+coq8.9"; - sha256 = "002xabhjlph394vydw3dx8ipv5ry2nq3py4440bk9a18ljx0w6ll"; + sha256 = "1jjzgpff09xjn9kgp7w69r096jkj0x2ksng3pawrmhmn7clwivbk"; + buildInputs = [ coq.ocamlPackages.camlp5 ]; + }; + "8.10" = { + sha256 = "1lq1mw15w4yky79qg3rm0mpzqi2ir51b6ak04ismrdr7ixky49y8"; + }; + "8.11" = { + sha256 = "09c6813988nvq4fpa45s33k70plnhxsblhm7cxxkg0i37mhvigsa"; }; }; param = params.${coq.coq-version}; in stdenv.mkDerivation rec { - inherit (param) version; + version = "1.1.2"; name = "coq${coq.coq-version}-paramcoq-${version}"; src = fetchFromGitHub { owner = "coq-community"; repo = "paramcoq"; - rev = "v${version}"; + rev = "v${version}+coq${coq.coq-version}"; inherit (param) sha256; }; buildInputs = [ coq ] - ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]) + ++ (with coq.ocamlPackages; [ ocaml findlib ]) + ++ (param.buildInputs or []) ; installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; |