diff options
Diffstat (limited to 'pkgs/development/coq-modules')
29 files changed, 73 insertions, 87 deletions
diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix index 9270609c6b2..0fdcb49d730 100644 --- a/pkgs/development/coq-modules/CoLoR/default.nix +++ b/pkgs/development/coq-modules/CoLoR/default.nix @@ -20,7 +20,7 @@ with lib; mkCoqDerivation { release."1.4.0".rev = "168c6b86c7d3f87ee51791f795a8828b1521589a"; release."1.4.0".sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm"; - extraBuildInputs = [ bignums ]; + propagatedBuildInputs = [ bignums ]; enableParallelBuilding = false; meta = { diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/coq-modules/HoTT/default.nix index 706943cf8d0..f6e9b3daca2 100644 --- a/pkgs/development/coq-modules/HoTT/default.nix +++ b/pkgs/development/coq-modules/HoTT/default.nix @@ -8,7 +8,7 @@ with lib; mkCoqDerivation { release."20170921".rev = "e3557740a699167e6adb1a65855509d55a392fa1"; release."20170921".sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v"; - extraBuildInputs = [ autoconf automake ]; + nativeBuildInputs = [ autoconf automake ]; preConfigure = '' patchShebangs ./autogen.sh diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix index db3227c1770..c2e6a5431c9 100644 --- a/pkgs/development/coq-modules/QuickChick/default.nix +++ b/pkgs/development/coq-modules/QuickChick/default.nix @@ -36,8 +36,7 @@ let recent = lib.versions.isGe "8.7" coq.coq-version; in "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native"; mlPlugin = true; - extraNativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild; - extraBuildInputs = lib.optional recent coq.ocamlPackages.num; + nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild; propagatedBuildInputs = [ ssreflect ] ++ lib.optionals recent [ coq-ext-lib simple-io ]; extraInstallFlags = [ "-f Makefile.coq" ]; diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix index a5dee94d045..8bf8a868023 100644 --- a/pkgs/development/coq-modules/VST/default.nix +++ b/pkgs/development/coq-modules/VST/default.nix @@ -31,7 +31,7 @@ mkCoqDerivation { release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf"; release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0="; releaseRev = v: "v${v}"; - extraBuildInputs = [ ITree ]; + buildInputs = [ ITree ]; propagatedBuildInputs = [ compcert ]; preConfigure = '' diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix index 0001ae1ded4..a53b8199fe9 100644 --- a/pkgs/development/coq-modules/bignums/default.nix +++ b/pkgs/development/coq-modules/bignums/default.nix @@ -5,7 +5,7 @@ with lib; mkCoqDerivation { owner = "coq"; displayVersion = { bignums = ""; }; inherit version; - defaultVersion = if versions.isGe "8.5" coq.coq-version + defaultVersion = if versions.isGe "8.6" coq.coq-version then "${coq.coq-version}.0" else null; release."8.15.0".sha256 = "093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns"; diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix index 092bb58d174..847ef8af23f 100644 --- a/pkgs/development/coq-modules/compcert/default.nix +++ b/pkgs/development/coq-modules/compcert/default.nix @@ -1,4 +1,5 @@ -{ lib, fetchzip, mkCoqDerivation, coq, flocq, compcert +{ lib, fetchzip, mkCoqDerivation +, coq, flocq, compcert , ocamlPackages, fetchpatch, makeWrapper, coq2html , stdenv, tools ? stdenv.cc , version ? null @@ -15,9 +16,9 @@ let compcert = mkCoqDerivation rec { releaseRev = v: "v${v}"; defaultVersion = with versions; switch coq.version [ - { case = range "8.8" "8.11"; out = "3.8"; } + { case = range "8.13" "8.15"; out = "3.10"; } { case = isEq "8.12" ; out = "3.9"; } - { case = range "8.12" "8.15"; out = "3.10"; } + { case = range "8.8" "8.11"; out = "3.8"; } ] null; release = { @@ -48,9 +49,13 @@ let compcert = mkCoqDerivation rec { ''; installTargets = "documentation install"; + installFlags = []; # trust ./configure + preInstall = '' + mkdir -p $out/share/man + mkdir -p $man/share + ''; postInstall = '' # move man into place - mkdir -p $man/share mv $out/share/man/ $man/share/ # move docs into place diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix index 6cb6bb3c813..f604db4ecdf 100644 --- a/pkgs/development/coq-modules/coq-bits/default.nix +++ b/pkgs/development/coq-modules/coq-bits/default.nix @@ -1,34 +1,18 @@ -{ lib, mkCoqDerivation, coq, mathcomp, version ? null }: +{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }: with lib; mkCoqDerivation { pname = "coq-bits"; repo = "bits"; inherit version; - defaultVersion = - if versions.isGe "8.10" coq.version - then "1.1.0" - else if versions.isGe "8.7" coq.version - then "1.0.0" - else null; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.10"; out = "1.1.0"; } + { case = isGe "8.7"; out = "1.0.0"; } + ] null; - release = { - "1.0.0" = { - rev = "1.0.0"; - sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl"; - }; - "1.1.0" = { - rev = "1.1.0"; - sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE="; - }; - }; - - extraBuildInputs = [ mathcomp.ssreflect mathcomp.fingroup ]; - propagatedBuildInputs = [ mathcomp.algebra ]; + release."1.1.0".sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE="; + release."1.0.0".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl"; - installPhase = '' - make -f Makefile CoqMakefile - make -f CoqMakefile COQLIB=$out/lib/coq/${coq.coq-version}/ install - ''; + propagatedBuildInputs = [ mathcomp-algebra ]; meta = { description = "A formalization of bitset operations in Coq"; diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index 55423047caa..03fe8c32d5c 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -7,7 +7,7 @@ with builtins; with lib; let { case = "8.13"; out = { version = "1.13.7"; };} { case = "8.14"; out = { version = "1.13.7"; };} { case = "8.15"; out = { version = "1.14.1"; };} - ] {}); + ] { version = "1.14.1"; } ); in mkCoqDerivation { pname = "elpi"; repo = "coq-elpi"; @@ -48,8 +48,8 @@ in mkCoqDerivation { release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b"; releaseRev = v: "v${v}"; - extraNativeBuildInputs = [ which elpi ]; mlPlugin = true; + propagatedBuildInputs = [ elpi ]; meta = { description = "Coq plugin embedding ELPI."; diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix index 3b8b23618d2..563e2dc22d6 100644 --- a/pkgs/development/coq-modules/coqeal/default.nix +++ b/pkgs/development/coq-modules/coqeal/default.nix @@ -1,6 +1,6 @@ { coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials, mathcomp-real-closed, - lib, which, version ? null }: + lib, version ? null }: with lib; @@ -22,7 +22,6 @@ with lib; release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk"; release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24"; - extraBuildInputs = [ which ]; propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ]; meta = { diff --git a/pkgs/development/coq-modules/coqhammer/default.nix b/pkgs/development/coq-modules/coqhammer/default.nix index 66a3dd222dd..853e77990b6 100644 --- a/pkgs/development/coq-modules/coqhammer/default.nix +++ b/pkgs/development/coq-modules/coqhammer/default.nix @@ -28,8 +28,10 @@ with lib; mkCoqDerivation { release."1.3-coq8.12".sha256 = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8"; release."1.3-coq8.11".sha256 = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b"; release."1.3-coq8.10".sha256 = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd"; - release."1.1.1-coq8.9".sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9"; - release."1.1-coq8.8".sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h"; + release."1.1.1-coq8.9" = { sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9"; + rev = "f8b4d81a213aa1f25afbe53c7c9ca1b15e3d42bc"; }; + release."1.1-coq8.8" = { sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h"; + rev = "c3cb54b4d5f33fab372d33c7189861368a08fa22"; }; release."1.3.1-coq8.13".version = "1.3.1"; release."1.3.1-coq8.12".version = "1.3.1"; diff --git a/pkgs/development/coq-modules/coqprime/default.nix b/pkgs/development/coq-modules/coqprime/default.nix index 46ede02a57e..26988b81e1a 100644 --- a/pkgs/development/coq-modules/coqprime/default.nix +++ b/pkgs/development/coq-modules/coqprime/default.nix @@ -20,7 +20,6 @@ with lib; mkCoqDerivation { release."8.7.2".sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k"; releaseRev = v: "v${v}"; - extraBuildInputs = [ which ]; propagatedBuildInputs = [ bignums ]; meta = with lib; { diff --git a/pkgs/development/coq-modules/coqtail-math/default.nix b/pkgs/development/coq-modules/coqtail-math/default.nix index 3491e6b21f2..a4f7ca405f7 100644 --- a/pkgs/development/coq-modules/coqtail-math/default.nix +++ b/pkgs/development/coq-modules/coqtail-math/default.nix @@ -14,9 +14,7 @@ mkCoqDerivation { release."8.14".sha256 = "sha256:1k8f8idjnx0mf4z479vcx55iz42rjxrbplbznv80m2famxakq03c"; release."20201124".rev = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e"; release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ="; - - extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml findlib ]; - + mlPlugin = true; meta = { license = licenses.lgpl3Only; maintainers = [ maintainers.siraben ]; diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix index 1a6dba9b0c0..09dd65df41d 100644 --- a/pkgs/development/coq-modules/coquelicot/default.nix +++ b/pkgs/development/coq-modules/coquelicot/default.nix @@ -1,4 +1,4 @@ -{ lib, mkCoqDerivation, which, autoconf, +{ lib, mkCoqDerivation, autoconf, coq, ssreflect, version ? null }: with lib; mkCoqDerivation { @@ -16,7 +16,7 @@ with lib; mkCoqDerivation { release."3.0.2".sha256 = "1rqfbbskgz7b1bcpva8wh3v3456sq2364y804f94sc8y5sij23nl"; releaseRev = v: "coquelicot-${v}"; - extraNativeBuildInputs = [ which autoconf ]; + nativeBuildInputs = [ autoconf ]; propagatedBuildInputs = [ ssreflect ]; useMelquiondRemake.logpath = "Coquelicot"; diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix index 7cf6132bf6a..fcc1303e827 100644 --- a/pkgs/development/coq-modules/dpdgraph/default.nix +++ b/pkgs/development/coq-modules/dpdgraph/default.nix @@ -39,9 +39,9 @@ mkCoqDerivation { release."0.6".sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n"; releaseRev = v: "v${v}"; - extraNativeBuildInputs = [ autoreconfHook ]; + nativeBuildInputs = [ autoreconfHook ]; mlPlugin = true; - extraBuildInputs = [ coq.ocamlPackages.ocamlgraph ]; + buildInputs = [ coq.ocamlPackages.ocamlgraph ]; # dpd_compute.ml uses deprecated Pervasives.compare # Versions prior to 0.6.5 do not have the WARN_ERR build flag diff --git a/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix index 47f097a34b2..d94dc03b637 100644 --- a/pkgs/development/coq-modules/fiat/HEAD.nix +++ b/pkgs/development/coq-modules/fiat/HEAD.nix @@ -8,10 +8,10 @@ with lib; mkCoqDerivation rec { inherit version; defaultVersion = if coq.coq-version == "8.5" then "2016-10-24" else null; release."2016-10-24".rev = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a"; - release."2016-10-24".sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64"; + release."2016-10-24".sha256 = "16y57vibq3f5i5avgj80f4i3aw46wdwzx36k5d3pf3qk17qrlrdi"; mlPlugin = true; - extraBuildInputs = [ python27 ]; + buildInputs = [ python27 ]; prePatch = "patchShebangs etc/coq-scripts"; diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix index f13aec883e7..a0f4a3ecae8 100644 --- a/pkgs/development/coq-modules/flocq/default.nix +++ b/pkgs/development/coq-modules/flocq/default.nix @@ -1,4 +1,4 @@ -{ lib, which, autoconf, automake, +{ lib, bash, autoconf, automake, mkCoqDerivation, coq, version ? null }: with lib; mkCoqDerivation { @@ -16,7 +16,7 @@ with lib; mkCoqDerivation { release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj"; releaseRev = v: "flocq-${v}"; - nativeBuildInputs = [ which autoconf ]; + nativeBuildInputs = [ bash autoconf ]; mlPlugin = true; useMelquiondRemake.logpath = "Flocq"; diff --git a/pkgs/development/coq-modules/gappalib/default.nix b/pkgs/development/coq-modules/gappalib/default.nix index 23cbd46743b..903b3518e5d 100644 --- a/pkgs/development/coq-modules/gappalib/default.nix +++ b/pkgs/development/coq-modules/gappalib/default.nix @@ -13,7 +13,7 @@ with lib; mkCoqDerivation { release."1.4.4".sha256 = "114q2hgw64j6kqa9mg3qcp1nlf0ia46z2xadq81fnkxqm856ml7l"; releaseRev = v: "gappalib-coq-${v}"; - extraNativeBuildInputs = [ which autoconf ]; + nativeBuildInputs = [ autoconf ]; mlPlugin = true; propagatedBuildInputs = [ flocq ]; useMelquiondRemake.logpath = "Gappa"; diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/coq-modules/heq/default.nix index 4bf9139b494..c3a815eb5c8 100644 --- a/pkgs/development/coq-modules/heq/default.nix +++ b/pkgs/development/coq-modules/heq/default.nix @@ -1,22 +1,26 @@ {lib, fetchzip, mkCoqDerivation, coq, version ? null }: +let fetcher = {rev, repo, owner, sha256, domain, ...}: + fetchzip { + url = "https://${domain}/${owner}/${repo}/download/${repo}-${rev}.zip"; + inherit sha256; + }; in with lib; mkCoqDerivation { pname = "heq"; repo = "Heq"; - owner = "gil"; - domain = "mpi-sws.org"; + owner = "gil.hur"; + domain = "sf.snu.ac.kr"; inherit version fetcher; defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null; release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74"; mlPlugin = true; - propagatedBuildInputs = [ coq ]; - - extraInstallFlags = [ "COQLIB=$out/lib/coq/${coq.coq-version}" ]; preBuild = "cd src"; + extraInstallFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + meta = { - homepage = "https://www.mpi-sws.org/~gil/Heq/"; + homepage = "https://ropas.snu.ac.kr/~gil.hur/Heq/"; description = "Heq : a Coq library for Heterogeneous Equality"; maintainers = with maintainers; [ jwiegley ]; }; diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix index c0fa2d7c8e0..6f15fc80388 100644 --- a/pkgs/development/coq-modules/hierarchy-builder/default.nix +++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix @@ -1,4 +1,4 @@ -{ lib, mkCoqDerivation, which, coq, coq-elpi, version ? null }: +{ lib, mkCoqDerivation, coq, coq-elpi, version ? null }: with lib; let hb = mkCoqDerivation { pname = "hierarchy-builder"; @@ -17,13 +17,10 @@ with lib; let hb = mkCoqDerivation { release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h"; releaseRev = v: "v${v}"; - extraNativeBuildInputs = [ which ]; - propagatedBuildInputs = [ coq-elpi ]; mlPlugin = true; - installFlags = [ "DESTDIR=$(out)" "COQMF_COQLIB=lib/coq/${coq.coq-version}" ]; extraInstallFlags = [ "VFILES=structures.v" ]; meta = { diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix index 375fae5b074..1a47478bda1 100644 --- a/pkgs/development/coq-modules/interval/default.nix +++ b/pkgs/development/coq-modules/interval/default.nix @@ -1,4 +1,5 @@ -{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, mathcomp-ssreflect, mathcomp-fingroup, bignums ? null, gnuplot_qt, version ? null }: +{ lib, mkCoqDerivation, autoconf, coq, coquelicot, flocq, + mathcomp-ssreflect, mathcomp-fingroup, bignums ? null, gnuplot_qt, version ? null }: mkCoqDerivation rec { pname = "interval"; @@ -20,8 +21,9 @@ mkCoqDerivation rec { release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz"; releaseRev = v: "interval-${v}"; - extraNativeBuildInputs = [ which autoconf ]; - propagatedBuildInputs = [ bignums coquelicot flocq mathcomp-ssreflect mathcomp-fingroup ] + nativeBuildInputs = [ autoconf ]; + propagatedBuildInputs = lib.optional (lib.versions.isGe "8.6" coq.coq-version) bignums + ++ [ coquelicot flocq mathcomp-ssreflect mathcomp-fingroup ] ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ]; useMelquiondRemake.logpath = "Interval"; mlPlugin = true; diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix index 4993a76b4f0..151a0511c80 100644 --- a/pkgs/development/coq-modules/itauto/default.nix +++ b/pkgs/development/coq-modules/itauto/default.nix @@ -17,7 +17,7 @@ mkCoqDerivation rec { ] null; mlPlugin = true; - extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); + nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); enableParallelBuilding = false; meta = { diff --git a/pkgs/development/coq-modules/ltac2/default.nix b/pkgs/development/coq-modules/ltac2/default.nix index 1d0d03fb7f7..c938a7ad027 100644 --- a/pkgs/development/coq-modules/ltac2/default.nix +++ b/pkgs/development/coq-modules/ltac2/default.nix @@ -17,7 +17,6 @@ with lib; mkCoqDerivation { release."0.1-8.7".rev = "v0.1-8.7"; release."0.1-8.7".sha256 = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0"; - nativeBuildInputs = [ which ]; mlPlugin = true; meta = { diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/coq-modules/math-classes/default.nix index 0a78191d8b7..2504e852baf 100644 --- a/pkgs/development/coq-modules/math-classes/default.nix +++ b/pkgs/development/coq-modules/math-classes/default.nix @@ -9,7 +9,7 @@ with lib; mkCoqDerivation { release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby"; release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw"; - extraBuildInputs = [ bignums ]; + propagatedBuildInputs = [ bignums ]; meta = { homepage = "https://math-classes.github.io"; diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index 0f562fec287..a19d8b8dcc7 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -10,9 +10,9 @@ # See the documentation at doc/languages-frameworks/coq.section.md. # ############################################################################ -{ lib, ncurses, which, graphviz, lua, fetchzip, +{ lib, ncurses, graphviz, lua, fetchzip, mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false, - coqPackages, coq, ocamlPackages, version ? null }@args: + coqPackages, coq, version ? null }@args: with builtins // lib; let repo = "math-comp"; @@ -60,8 +60,9 @@ let inherit version pname defaultVersion release releaseRev repo owner; mlPlugin = versions.isLe "8.6" coq.coq-version; - extraNativeBuildInputs = [ which ] ++ optionals withDoc [ graphviz lua ]; - extraBuildInputs = [ ncurses ] ++ mathcomp-deps; + nativeBuildInputs = optionals withDoc [ graphviz lua ]; + buildInputs = [ ncurses ]; + propagatedBuildInputs = mathcomp-deps; buildFlags = optional withDoc "doc"; diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/coq-modules/metacoq/default.nix index 583d8b7adb9..09327f46b86 100644 --- a/pkgs/development/coq-modules/metacoq/default.nix +++ b/pkgs/development/coq-modules/metacoq/default.nix @@ -1,4 +1,4 @@ -{ lib, which, fetchzip, +{ lib, fetchzip, mkCoqDerivation, recurseIntoAttrs, single ? false, coqPackages, coq, equations, version ? null }@args: with builtins // lib; @@ -36,10 +36,8 @@ let derivation = mkCoqDerivation ({ inherit version pname defaultVersion release releaseRev repo owner; - extraNativeBuildInputs = [ which ]; mlPlugin = true; - extraBuildInputs = [ coq.ocamlPackages.zarith ]; - propagatedBuildInputs = [ equations ] ++ metacoq-deps; + propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps; patchPhase = '' patchShebangs ./configure.sh diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix index 26bd38f72df..83333b3e1bf 100644 --- a/pkgs/development/coq-modules/metalib/default.nix +++ b/pkgs/development/coq-modules/metalib/default.nix @@ -13,7 +13,6 @@ with lib; mkCoqDerivation { release."8.10".sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs"; sourceRoot = "source/Metalib"; - installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}"; meta = { license = licenses.mit; diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/coq-modules/semantics/default.nix index e112512ec5c..cbf1469e1f0 100644 --- a/pkgs/development/coq-modules/semantics/default.nix +++ b/pkgs/development/coq-modules/semantics/default.nix @@ -24,8 +24,8 @@ mkCoqDerivation rec { ] null; mlPlugin = true; - extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); - extraBuildInputs = (with coq.ocamlPackages; [ num ]); + nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); + propagatedBuildInputs = (with coq.ocamlPackages; [ num ]); postPatch = '' for p in Make Makefile.coq.local diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/coq-modules/simple-io/default.nix index bcc391c4f72..ca7325711e2 100644 --- a/pkgs/development/coq-modules/simple-io/default.nix +++ b/pkgs/development/coq-modules/simple-io/default.nix @@ -11,11 +11,9 @@ with lib; mkCoqDerivation { ] null; release."1.7.0".sha256 = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci"; release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax"; - extraNativeBuildInputs = (with coq.ocamlPackages; [ cppo zarith ]); - propagatedBuildInputs = [ coq-ext-lib ] - ++ (with coq.ocamlPackages; [ ocaml ocamlbuild ]); - mlPlugin = true; + nativeBuildInputs = [ coq.ocamlPackages.cppo ]; + propagatedBuildInputs = [ coq-ext-lib coq.ocamlPackages.ocamlbuild ]; doCheck = true; checkTarget = "test"; diff --git a/pkgs/development/coq-modules/smtcoq/default.nix b/pkgs/development/coq-modules/smtcoq/default.nix index 0389b45fb5c..ebaebe6974e 100644 --- a/pkgs/development/coq-modules/smtcoq/default.nix +++ b/pkgs/development/coq-modules/smtcoq/default.nix @@ -13,9 +13,11 @@ mkCoqDerivation { { case = isEq "8.13"; out = "itp22"; } ] null; - propagatedBuildInputs = [ trakt cvc4 ] ++ lib.optionals (!stdenv.isDarwin) [ veriT ]; - extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml ocamlbuild ]; - extraBuildInputs = with coq.ocamlPackages; [ findlib num zarith ]; + propagatedBuildInputs = [ trakt cvc4 ] + ++ lib.optionals (!stdenv.isDarwin) [ veriT ] + ++ (with coq.ocamlPackages; [ num zarith ]); + mlPlugin = true; + nativeBuildInputs = with coq.ocamlPackages; [ ocamlbuild ]; meta = { description = "Communication between Coq and SAT/SMT solvers "; |