diff options
author | Alyssa Ross <hi@alyssa.is> | 2021-08-04 10:54:22 +0000 |
---|---|---|
committer | Alyssa Ross <hi@alyssa.is> | 2021-08-04 10:54:22 +0000 |
commit | d2e147bedf251976ed99b94b6c905d6761f7a892 (patch) | |
tree | 9e0c62d61698916fd4627ed98d3d880c8fc0ab2e /pkgs/development/coq-modules | |
parent | 62614cbef7da005c1eda8c9400160f6bcd6546b8 (diff) | |
parent | c464dc811babfe316ed4ab7bbc12351122e69dd7 (diff) | |
download | nixpkgs-d2e147bedf251976ed99b94b6c905d6761f7a892.tar nixpkgs-d2e147bedf251976ed99b94b6c905d6761f7a892.tar.gz nixpkgs-d2e147bedf251976ed99b94b6c905d6761f7a892.tar.bz2 nixpkgs-d2e147bedf251976ed99b94b6c905d6761f7a892.tar.lz nixpkgs-d2e147bedf251976ed99b94b6c905d6761f7a892.tar.xz nixpkgs-d2e147bedf251976ed99b94b6c905d6761f7a892.tar.zst nixpkgs-d2e147bedf251976ed99b94b6c905d6761f7a892.zip |
Merge remote-tracking branch 'nixpkgs/nixos-unstable' into master
Diffstat (limited to 'pkgs/development/coq-modules')
-rw-r--r-- | pkgs/development/coq-modules/QuickChick/default.nix | 19 | ||||
-rw-r--r-- | pkgs/development/coq-modules/VST/default.nix | 21 | ||||
-rw-r--r-- | pkgs/development/coq-modules/category-theory/default.nix | 3 | ||||
-rw-r--r-- | pkgs/development/coq-modules/corn/default.nix | 2 | ||||
-rw-r--r-- | pkgs/development/coq-modules/graph-theory/default.nix | 33 | ||||
-rw-r--r-- | pkgs/development/coq-modules/interval/default.nix | 15 |
6 files changed, 77 insertions, 16 deletions
diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix index 6490391eb63..fcaaaac615e 100644 --- a/pkgs/development/coq-modules/QuickChick/default.nix +++ b/pkgs/development/coq-modules/QuickChick/default.nix @@ -1,10 +1,11 @@ -{ lib, mkCoqDerivation, coq, ssreflect, coq-ext-lib, simple-io }: -with lib; -let recent = versions.isGe "8.7" coq.coq-version; in +{ lib, mkCoqDerivation, coq, ssreflect, coq-ext-lib, simple-io, version ? null }: + +let recent = lib.versions.isGe "8.7" coq.coq-version; in mkCoqDerivation { pname = "QuickChick"; owner = "QuickChick"; - defaultVersion = with versions; switch [ coq.coq-version ssreflect.version ] [ + inherit version; + defaultVersion = with lib; with versions; lib.switch [ coq.coq-version ssreflect.version ] [ { cases = [ "8.13" pred.true ]; out = "1.5.0"; } { cases = [ "8.12" pred.true ]; out = "1.4.0"; } { cases = [ "8.11" pred.true ]; out = "1.3.2"; } @@ -29,19 +30,19 @@ mkCoqDerivation { release."20170512".sha256 = "033ch10i5wmqyw8j6wnr0dlbnibgfpr1vr0c07q3yj6h23xkmqpg"; releaseRev = v: "v${v}"; - preConfigure = optionalString recent + preConfigure = lib.optionalString recent "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native"; mlPlugin = true; - extraBuildInputs = optional recent coq.ocamlPackages.num; + extraBuildInputs = lib.optional recent coq.ocamlPackages.num; propagatedBuildInputs = [ ssreflect ] - ++ optionals recent [ coq-ext-lib simple-io ] - ++ optional recent coq.ocamlPackages.ocamlbuild; + ++ lib.optionals recent [ coq-ext-lib simple-io ] + ++ lib.optional recent coq.ocamlPackages.ocamlbuild; extraInstallFlags = [ "-f Makefile.coq" ]; enableParallelBuilding = false; - meta = { + meta = with lib; { description = "Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck"; maintainers = with maintainers; [ jwiegley ]; }; diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix index 5ee1df77418..1d2a1a3c05f 100644 --- a/pkgs/development/coq-modules/VST/default.nix +++ b/pkgs/development/coq-modules/VST/default.nix @@ -1,4 +1,16 @@ -{ lib, mkCoqDerivation, coq, compcert, version ? null }: +{ lib, mkCoqDerivation, coq, compcert, ITree, version ? null }: + +# A few modules that are not built and installed by default +# but that may be useful to some users. +# They depend on ITree. +let extra_floyd_files = [ + "ASTsize.v" + "io_events.v" + "powerlater.v" + "printf.v" + "quickprogram.v" + ]; +in with lib; mkCoqDerivation { pname = "coq${coq.coq-version}-VST"; @@ -12,9 +24,14 @@ with lib; mkCoqDerivation { ] null; release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0="; releaseRev = v: "v${v}"; + extraBuildInputs = [ ITree ]; propagatedBuildInputs = [ compcert ]; - preConfigure = "patchShebangs util"; + preConfigure = '' + patchShebangs util + substituteInPlace Makefile \ + --replace 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}' + ''; makeFlags = [ "BITSIZE=64" diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix index 339bcb9d6b0..d24cf147930 100644 --- a/pkgs/development/coq-modules/category-theory/default.nix +++ b/pkgs/development/coq-modules/category-theory/default.nix @@ -5,6 +5,8 @@ with lib; mkCoqDerivation { pname = "category-theory"; owner = "jwiegley"; + release."20210730".rev = "d87937faaf7460bcd6985931ac36f551d67e11af"; + release."20210730".sha256 = "04x7433yvibxknk6gy4971yzb4saa3z4dnfy9n6irhyafzlxyf0f"; release."20190414".rev = "706fdb4065cc2302d92ac2bce62cb59713253119"; release."20190414".sha256 = "16lg4xs2wzbdbsn148xiacgl4wq4xwfqjnjkdhfr3w0qh1s81hay"; release."20180709".rev = "3b9ba7b26a64d49a55e8b6ccea570a7f32c11ead"; @@ -12,6 +14,7 @@ with lib; mkCoqDerivation { inherit version; defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.10" "8.13"; out = "20210730"; } { case = range "8.8" "8.9"; out = "20190414"; } { case = range "8.6" "8.7"; out = "20180709"; } ] null; diff --git a/pkgs/development/coq-modules/corn/default.nix b/pkgs/development/coq-modules/corn/default.nix index 6910f487c64..6a3ea81ca0d 100644 --- a/pkgs/development/coq-modules/corn/default.nix +++ b/pkgs/development/coq-modules/corn/default.nix @@ -6,10 +6,12 @@ with lib; mkCoqDerivation rec { defaultVersion = switch coq.coq-version [ { case = "8.6"; out = "8.8.1"; } { case = (versions.range "8.7" "8.12"); out = "8.12.0"; } + { case = (versions.range "8.13" "8.13"); out = "c366d3f01ec1812b145117a4da940518b092d3a6"; } ] null; release = { "8.8.1".sha256 = "0gh32j0f18vv5lmf6nb87nr5450w6ai06rhrnvlx2wwi79gv10wp"; "8.12.0".sha256 = "0b92vhyzn1j6cs84z2182fn82hxxj0bqq7hk6cs4awwb3vc7dkhi"; + "c366d3f01ec1812b145117a4da940518b092d3a6".sha256 = "1wzr7mdsnf1rq7q0dvmv55vxzysy85b00ahwbs868bl7m8fk8x5b"; }; preConfigure = "patchShebangs ./configure.sh"; diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix new file mode 100644 index 00000000000..5607d342a2e --- /dev/null +++ b/pkgs/development/coq-modules/graph-theory/default.nix @@ -0,0 +1,33 @@ +{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap +, hierarchy-builder, version ? null }: + +with lib; + +mkCoqDerivation { + pname = "graph-theory"; + + release."0.9".sha256 = "sha256-Hl3JS9YERD8QQziXqZ9DqLHKp63RKI9HxoFYWSkJQZI="; + + releaseRev = v: "v${v}"; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.13"; out = "0.9"; } + ] null; + + propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap hierarchy-builder ]; + + meta = { + description = "Library of formalized graph theory results in Coq"; + longDescription = '' + A library of formalized graph theory results, including various + standard results from the literature (e.g., Menger’s Theorem, Hall’s + Marriage Theorem, and the excluded minor characterization of + treewidth-two graphs) as well as some more recent results arising from + the study of relation algebra within the ERC CoVeCe project (e.g., + soundness and completeness of an axiomatization of graph isomorphism). + ''; + maintainers = with maintainers; [ siraben ]; + license = licenses.cecill-b; + }; +} diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix index cdb90452365..12fe66b50da 100644 --- a/pkgs/development/coq-modules/interval/default.nix +++ b/pkgs/development/coq-modules/interval/default.nix @@ -1,16 +1,18 @@ -{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, bignums ? null, version ? null }: +{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, bignums ? null, gnuplot_qt, version ? null }: -with lib; mkCoqDerivation { +mkCoqDerivation rec { pname = "interval"; owner = "coqinterval"; domain = "gitlab.inria.fr"; inherit version; - defaultVersion = with versions; switch coq.coq-version [ - { case = isGe "8.8" ; out = "4.1.1"; } + defaultVersion = with lib.versions; lib.switch coq.coq-version [ + { case = isGe "8.8" ; out = "4.3.0"; } { case = range "8.8" "8.12"; out = "4.0.0"; } { case = range "8.7" "8.11"; out = "3.4.2"; } { case = range "8.5" "8.6"; out = "3.3.0"; } ] null; + release."4.3.0".sha256 = "sha256-k8DLC4HYYpHeEEgXUafS8jkaECqlM+/CoYaInmUTYko="; + release."4.2.0".sha256 = "sha256-SD5thgpirs3wmZBICjXGpoefg9AAXyExb5t8tz3iZhE="; release."4.1.1".sha256 = "sha256-h2NJ6sZt1C/88v7W2xyuftEDoyRt3H6kqm5g2hc1aoU="; release."4.0.0".sha256 = "1hhih6zmid610l6c8z3x4yzdzw9jniyjiknd1vpkyb2rxvqm3gzp"; release."3.4.2".sha256 = "07ngix32qarl3pjnm9d0vqc9fdrgm08gy7zp306hwxjyq7h1v7z0"; @@ -18,8 +20,11 @@ with lib; mkCoqDerivation { releaseRev = v: "interval-${v}"; nativeBuildInputs = [ which autoconf ]; - propagatedBuildInputs = [ bignums coquelicot flocq ]; + propagatedBuildInputs = [ bignums coquelicot flocq ] + ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ]; useMelquiondRemake.logpath = "Interval"; + mlPlugin = true; + enableParallelBuilding = true; meta = with lib; { description = "Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant"; |