diff options
34 files changed, 113 insertions, 128 deletions
diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md index 11777b5eef42e..9a692104a0417 100644 --- a/doc/languages-frameworks/coq.section.md +++ b/doc/languages-frameworks/coq.section.md @@ -29,19 +29,14 @@ The recommended way of defining a derivation for a Coq library, is to use the `c * `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags, * `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers, * `namePrefix` (optional, defaults to `[ "coq" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`, -* `nativeBuildInputs` (optional), is a list of executables that are required to build the current derivation, in addition to the default ones (namely `which`, `dune` and `ocaml` depending on whether `useDune2`, `useDune2ifVersion` and `mlPlugin` are set). -* `extraNativeBuildInputs` (optional, deprecated), an additional list of derivation to add to `nativeBuildInputs`, -* `overrideNativeBuildInputs` (optional) replaces the default list of derivation to which `nativeBuildInputs` and `extraNativeBuildInputs` adds extra elements, -* `buildInputs` (optional), is a list of libraries and dependencies that are required to build and run the current derivation, in addition to the default one `[ coq ]`, -* `extraBuildInputs` (optional, deprecated), an additional list of derivation to add to `buildInputs`, -* `overrideBuildInputs` (optional) replaces the default list of derivation to which `buildInputs` and `extraBuildInputs` adds extras elements, -* `propagatedBuildInputs` (optional) is passed as is to `mkDerivation`, we recommend to use this for Coq libraries and Coq plugin dependencies, as this makes sure the paths of the compiled libraries and plugins will always be added to the build environements of subsequent derivation, which is necessary for Coq packages to work correctly, -* `mlPlugin` (optional, defaults to `false`). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to `true`. For a finer grain control, the `coq.ocamlPackages` attribute can be used in `nativeBuildInputs`, `buildInputs`, and `propagatedBuildInputs` to depend on the same package set Coq was built against. -* `useDune2ifVersion` (optional, default to `(x: false)` uses Dune2 to build the package if the provided predicate evaluates to true on the version, e.g. `useDune2ifVersion = versions.isGe "1.1"` will use dune if the version of the package is greater or equal to `"1.1"`, +* `extraNativeBuildInputs` (optional), by default `nativeBuildInputs` just contains `coq`, this allows to add more native build inputs, `nativeBuildInputs` are executables and `buildInputs` are libraries and dependencies, +* `extraBuildInputs` (optional), this allows to add more build inputs, +* `mlPlugin` (optional, defaults to `false`). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to `true`. For a finer grain control, the `coq.ocamlPackages` attribute can be used in `extraBuildInputs` to depend on the same package set Coq was built against. +* `useDune2ifVersion` (optional, default to `(x: false)` uses Dune2 to build the package if the provided predicate evaluates to true on the version, e.g. `useDune2if = versions.isGe "1.1"` will use dune if the version of the package is greater or equal to `"1.1"`, * `useDune2` (optional, defaults to `false`) uses Dune2 to build the package if set to true, the presence of this attribute overrides the behavior of the previous one. * `opam-name` (optional, defaults to concatenating with a dash separator the components of `namePrefix` and `pname`), name of the Dune package to build. * `enableParallelBuilding` (optional, defaults to `true`), since it is activated by default, we provide a way to disable it. -* `extraInstallFlags` (optional), allows to extend `installFlags` which initializes the variables `DESTDIR` and `COQMF_COQLIB` so as to install in the proper subdirectory. Indeed Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation. +* `extraInstallFlags` (optional), allows to extend `installFlags` which initializes the variable `COQMF_COQLIB` so as to install in the proper subdirectory. Indeed Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation. * `setCOQBIN` (optional, defaults to `true`), by default, the environment variable `$COQBIN` is set to the current Coq's binary, but one can disable this behavior by setting it to `false`, * `useMelquiondRemake` (optional, default to `null`) is an attribute set, which, if given, overloads the `preConfigurePhases`, `configureFlags`, `buildPhase`, and `installPhase` attributes of the derivation for a specific use in libraries using `remake` as set up by Guillaume Melquiond for `flocq`, `gappalib`, `interval`, and `coquelicot` (see the corresponding derivation for concrete examples of use of this option). For backward compatibility, the attribute `useMelquiondRemake.logpath` must be set to the logical root of the library (otherwise, one can pass `useMelquiondRemake = {}` to activate this without backward compatibility). * `dropAttrs`, `keepAttrs`, `dropDerivationAttrs` are all optional and allow to tune which attribute is added or removed from the final call to `mkDerivation`. diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 58edf0a0039a4..c078287b85ee3 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -70,9 +70,9 @@ let { case = range "8.7" "8.10"; out = ocamlPackages_4_09; } { case = range "8.5" "8.6"; out = ocamlPackages_4_05; } ] ocamlPackages_4_12; - ocamlNativeBuildInputs = [ ocamlPackages.ocaml ] + ocamlNativeBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ] ++ optional (coqAtLeast "8.14") ocamlPackages.dune_2; - ocamlBuildInputs = [ ocamlPackages.findlib ] + ocamlBuildInputs = [] ++ optional (!coqAtLeast "8.10") ocamlPackages.camlp5 ++ optional (!coqAtLeast "8.13") ocamlPackages.num ++ optional (coqAtLeast "8.13") ocamlPackages.zarith; @@ -136,15 +136,13 @@ self = stdenv.mkDerivation { ++ optional buildIde copyDesktopItems ++ optional (buildIde && coqAtLeast "8.10") wrapGAppsHook ++ optional (!coqAtLeast "8.6") gnumake42; - buildInputs = [ ncurses ] + buildInputs = [ ncurses ] ++ ocamlBuildInputs ++ optionals buildIde (if coqAtLeast "8.10" then [ ocamlPackages.lablgtk3-sourceview3 glib gnome.adwaita-icon-theme ] else [ ocamlPackages.lablgtk ]) ; - propagatedBuildInputs = ocamlBuildInputs; - postPatch = '' UNAME=$(type -tp uname) RM=$(type -tp rm) diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix index 70c62c659a2d2..a681bbda5575d 100644 --- a/pkgs/build-support/coq/default.nix +++ b/pkgs/build-support/coq/default.nix @@ -1,4 +1,4 @@ -{ lib, stdenv, coqPackages, coq, which, fetchzip }@args: +{ lib, stdenv, coqPackages, coq, fetchzip }@args: let lib = import ./extra-lib.nix {inherit (args) lib;}; in with builtins; with lib; let @@ -15,12 +15,8 @@ in releaseRev ? (v: v), displayVersion ? {}, release ? {}, - buildInputs ? [], - nativeBuildInputs ? [], extraBuildInputs ? [], extraNativeBuildInputs ? [], - overrideBuildInputs ? [], - overrideNativeBuildInputs ? [], namePrefix ? [ "coq" ], enableParallelBuilding ? true, extraInstallFlags ? [], @@ -39,11 +35,7 @@ let args-to-remove = foldl (flip remove) ([ "version" "fetcher" "repo" "owner" "domain" "releaseRev" "displayVersion" "defaultVersion" "useMelquiondRemake" - "release" - "buildInputs" "nativeBuildInputs" - "extraBuildInputs" "extraNativeBuildInputs" - "overrideBuildInputs" "overrideNativeBuildInputs" - "namePrefix" + "release" "extraBuildInputs" "extraNativeBuildInputs" "extraPropagatedBuildInputs" "namePrefix" "meta" "useDune2ifVersion" "useDune2" "opam-name" "extraInstallFlags" "setCOQBIN" "mlPlugin" "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs; @@ -65,16 +57,9 @@ let ] "") + optionalString (v == null) "-broken"; append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-"; prefix-name = foldl append-version "" namePrefix; + var-coqlib-install = + (optionalString (versions.isGe "8.7" coq.coq-version || coq.coq-version == "dev") "COQMF_") + "COQLIB"; useDune2 = args.useDune2 or (useDune2ifVersion fetched.version); - coqlib-flags = switch coq.coq-version [ - { case = v: versions.isLe "8.6" v && v != "dev" ; - out = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; } - ] [ "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib" - "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" ]; - docdir-flags = switch coq.coq-version [ - { case = v: versions.isLe "8.6" v && v != "dev"; - out = [ "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ]; } - ] [ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ]; in stdenv.mkDerivation (removeAttrs ({ @@ -83,12 +68,12 @@ stdenv.mkDerivation (removeAttrs ({ inherit (fetched) version src; - nativeBuildInputs = args.overrideNativeBuildInputs - or ([ which ] ++ optional useDune2 coq.ocamlPackages.dune_2 - ++ optional (useDune2 || mlPlugin) coq.ocaml - ++ (args.nativeBuildInputs or []) ++ extraNativeBuildInputs); - buildInputs = args.overrideBuildInputs - or ([ coq ] ++ (args.buildInputs or []) ++ extraBuildInputs); + nativeBuildInputs = [ coq ] + ++ optionals useDune2 [coq.ocaml coq.ocamlPackages.dune_2] + ++ optionals mlPlugin coq.ocamlNativeBuildInputs + ++ extraNativeBuildInputs; + buildInputs = optionals mlPlugin coq.ocamlBuildInputs + ++ extraBuildInputs; inherit enableParallelBuilding; meta = ({ platforms = coq.meta.platforms; } // @@ -103,7 +88,9 @@ stdenv.mkDerivation (removeAttrs ({ // (optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; }) // (optionalAttrs (!args?installPhase && !args?useMelquiondRemake) { installFlags = - [ "DESTDIR=$(out)" ] ++ coqlib-flags ++ docdir-flags ++ + [ "${var-coqlib-install}=$(out)/lib/coq/${coq.coq-version}/" ] ++ + optional (match ".*doc$" (args.installTargets or "") != null) + "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ++ extraInstallFlags; }) // (optionalAttrs useDune2 { diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix index 0fdcb49d73008..9270609c6b2fa 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"; - propagatedBuildInputs = [ bignums ]; + extraBuildInputs = [ bignums ]; enableParallelBuilding = false; meta = { diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/coq-modules/HoTT/default.nix index f6e9b3daca2db..706943cf8d024 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"; - nativeBuildInputs = [ autoconf automake ]; + extraBuildInputs = [ 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 c2e6a5431c918..db3227c1770e0 100644 --- a/pkgs/development/coq-modules/QuickChick/default.nix +++ b/pkgs/development/coq-modules/QuickChick/default.nix @@ -36,7 +36,8 @@ let recent = lib.versions.isGe "8.7" coq.coq-version; in "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native"; mlPlugin = true; - nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild; + extraNativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild; + extraBuildInputs = lib.optional recent coq.ocamlPackages.num; 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 8bf8a8680237d..a5dee94d045dc 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}"; - buildInputs = [ ITree ]; + extraBuildInputs = [ ITree ]; propagatedBuildInputs = [ compcert ]; preConfigure = '' diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix index a53b8199fe96e..0001ae1ded4d8 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.6" coq.coq-version + defaultVersion = if versions.isGe "8.5" 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 5d2eb4433e6b1..092bb58d174fa 100644 --- a/pkgs/development/coq-modules/compcert/default.nix +++ b/pkgs/development/coq-modules/compcert/default.nix @@ -1,5 +1,5 @@ { lib, fetchzip, mkCoqDerivation, coq, flocq, compcert -, fetchpatch, makeWrapper, coq2html +, ocamlPackages, fetchpatch, makeWrapper, coq2html , stdenv, tools ? stdenv.cc , version ? null }: @@ -15,9 +15,9 @@ let compcert = mkCoqDerivation rec { releaseRev = v: "v${v}"; defaultVersion = with versions; switch coq.version [ - { case = range "8.13" "8.15"; out = "3.10"; } - { case = isEq "8.12" ; out = "3.9"; } { case = range "8.8" "8.11"; out = "3.8"; } + { case = isEq "8.12" ; out = "3.9"; } + { case = range "8.12" "8.15"; out = "3.10"; } ] null; release = { @@ -26,9 +26,8 @@ let compcert = mkCoqDerivation rec { "3.10".sha256 = "sha256:19rmx8r8v46101ij5myfrz60arqjy7q3ra3fb8mxqqi3c8c4l4j6"; }; - mlPlugin = true; nativeBuildInputs = [ makeWrapper ]; - buildInputs = with coq.ocamlPackages; [ menhir menhirLib ] ++ [ coq2html ]; + buildInputs = with ocamlPackages; [ ocaml findlib menhir menhirLib ] ++ [ coq coq2html ]; propagatedBuildInputs = [ flocq ]; enableParallelBuilding = true; @@ -49,13 +48,9 @@ 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 f604db4ecdf71..6cb6bb3c813ee 100644 --- a/pkgs/development/coq-modules/coq-bits/default.nix +++ b/pkgs/development/coq-modules/coq-bits/default.nix @@ -1,18 +1,34 @@ -{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }: +{ lib, mkCoqDerivation, coq, mathcomp, version ? null }: with lib; mkCoqDerivation { pname = "coq-bits"; repo = "bits"; inherit version; - defaultVersion = with versions; switch coq.coq-version [ - { case = isGe "8.10"; out = "1.1.0"; } - { case = isGe "8.7"; out = "1.0.0"; } - ] null; + 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; - release."1.1.0".sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE="; - release."1.0.0".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl"; + 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 ]; - propagatedBuildInputs = [ mathcomp-algebra ]; + installPhase = '' + make -f Makefile CoqMakefile + make -f CoqMakefile COQLIB=$out/lib/coq/${coq.coq-version}/ install + ''; 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 03fe8c32d5c33..55423047caa70 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 563e2dc22d6df..3b8b23618d232 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, version ? null }: + lib, which, version ? null }: with lib; @@ -22,6 +22,7 @@ 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 853e77990b6eb..66a3dd222dd5b 100644 --- a/pkgs/development/coq-modules/coqhammer/default.nix +++ b/pkgs/development/coq-modules/coqhammer/default.nix @@ -28,10 +28,8 @@ 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"; - rev = "f8b4d81a213aa1f25afbe53c7c9ca1b15e3d42bc"; }; - release."1.1-coq8.8" = { sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h"; - rev = "c3cb54b4d5f33fab372d33c7189861368a08fa22"; }; + release."1.1.1-coq8.9".sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9"; + release."1.1-coq8.8".sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h"; 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 26988b81e1a6b..46ede02a57e69 100644 --- a/pkgs/development/coq-modules/coqprime/default.nix +++ b/pkgs/development/coq-modules/coqprime/default.nix @@ -20,6 +20,7 @@ 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 a4f7ca405f713..3491e6b21f2f8 100644 --- a/pkgs/development/coq-modules/coqtail-math/default.nix +++ b/pkgs/development/coq-modules/coqtail-math/default.nix @@ -14,7 +14,9 @@ mkCoqDerivation { release."8.14".sha256 = "sha256:1k8f8idjnx0mf4z479vcx55iz42rjxrbplbznv80m2famxakq03c"; release."20201124".rev = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e"; release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ="; - mlPlugin = true; + + extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml findlib ]; + 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 09dd65df41d22..1a6dba9b0c085 100644 --- a/pkgs/development/coq-modules/coquelicot/default.nix +++ b/pkgs/development/coq-modules/coquelicot/default.nix @@ -1,4 +1,4 @@ -{ lib, mkCoqDerivation, autoconf, +{ lib, mkCoqDerivation, which, 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}"; - nativeBuildInputs = [ autoconf ]; + extraNativeBuildInputs = [ which 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 fcc1303e82761..7cf6132bf6a9a 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}"; - nativeBuildInputs = [ autoreconfHook ]; + extraNativeBuildInputs = [ autoreconfHook ]; mlPlugin = true; - buildInputs = [ coq.ocamlPackages.ocamlgraph ]; + extraBuildInputs = [ 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 d94dc03b63779..47f097a34b2ef 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 = "16y57vibq3f5i5avgj80f4i3aw46wdwzx36k5d3pf3qk17qrlrdi"; + release."2016-10-24".sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64"; mlPlugin = true; - buildInputs = [ python27 ]; + extraBuildInputs = [ 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 a0f4a3ecae82b..f13aec883e769 100644 --- a/pkgs/development/coq-modules/flocq/default.nix +++ b/pkgs/development/coq-modules/flocq/default.nix @@ -1,4 +1,4 @@ -{ lib, bash, autoconf, automake, +{ lib, which, 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 = [ bash autoconf ]; + nativeBuildInputs = [ which 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 903b3518e5d6f..23cbd46743b19 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}"; - nativeBuildInputs = [ autoconf ]; + extraNativeBuildInputs = [ which 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 c3a815eb5c87e..4bf9139b49473 100644 --- a/pkgs/development/coq-modules/heq/default.nix +++ b/pkgs/development/coq-modules/heq/default.nix @@ -1,26 +1,22 @@ {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.hur"; - domain = "sf.snu.ac.kr"; + owner = "gil"; + domain = "mpi-sws.org"; inherit version fetcher; defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null; release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74"; mlPlugin = true; - preBuild = "cd src"; + propagatedBuildInputs = [ coq ]; - extraInstallFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + extraInstallFlags = [ "COQLIB=$out/lib/coq/${coq.coq-version}" ]; + preBuild = "cd src"; meta = { - homepage = "https://ropas.snu.ac.kr/~gil.hur/Heq/"; + homepage = "https://www.mpi-sws.org/~gil/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 6f15fc80388e0..c0fa2d7c8e00a 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, coq, coq-elpi, version ? null }: +{ lib, mkCoqDerivation, which, coq, coq-elpi, version ? null }: with lib; let hb = mkCoqDerivation { pname = "hierarchy-builder"; @@ -17,10 +17,13 @@ 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 4134a8fd573d1..b9257d415e57f 100644 --- a/pkgs/development/coq-modules/interval/default.nix +++ b/pkgs/development/coq-modules/interval/default.nix @@ -1,5 +1,4 @@ -{ lib, mkCoqDerivation, autoconf, coq, coquelicot, flocq, - mathcomp-ssreflect, mathcomp-fingroup, bignums ? null, gnuplot_qt, version ? null }: +{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, mathcomp-ssreflect, mathcomp-fingroup, bignums ? null, gnuplot_qt, version ? null }: mkCoqDerivation rec { pname = "interval"; @@ -21,9 +20,8 @@ mkCoqDerivation rec { release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz"; releaseRev = v: "interval-${v}"; - nativeBuildInputs = [ autoconf ]; - propagatedBuildInputs = lib.optional (lib.versions.isGe "8.6" coq.coq-version) bignums - ++ [ coquelicot flocq mathcomp-ssreflect mathcomp-fingroup ] + extraNativeBuildInputs = [ which autoconf ]; + propagatedBuildInputs = [ 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 151a0511c806a..4993a76b4f08f 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; - nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); + extraNativeBuildInputs = (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 c938a7ad02790..1d0d03fb7f7ce 100644 --- a/pkgs/development/coq-modules/ltac2/default.nix +++ b/pkgs/development/coq-modules/ltac2/default.nix @@ -17,6 +17,7 @@ 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 2504e852bafda..0a78191d8b728 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"; - propagatedBuildInputs = [ bignums ]; + extraBuildInputs = [ 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 a19d8b8dcc79d..0f562fec287c1 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, graphviz, lua, fetchzip, +{ lib, ncurses, which, graphviz, lua, fetchzip, mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false, - coqPackages, coq, version ? null }@args: + coqPackages, coq, ocamlPackages, version ? null }@args: with builtins // lib; let repo = "math-comp"; @@ -60,9 +60,8 @@ let inherit version pname defaultVersion release releaseRev repo owner; mlPlugin = versions.isLe "8.6" coq.coq-version; - nativeBuildInputs = optionals withDoc [ graphviz lua ]; - buildInputs = [ ncurses ]; - propagatedBuildInputs = mathcomp-deps; + extraNativeBuildInputs = [ which ] ++ optionals withDoc [ graphviz lua ]; + extraBuildInputs = [ ncurses ] ++ 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 09327f46b86de..583d8b7adb914 100644 --- a/pkgs/development/coq-modules/metacoq/default.nix +++ b/pkgs/development/coq-modules/metacoq/default.nix @@ -1,4 +1,4 @@ -{ lib, fetchzip, +{ lib, which, fetchzip, mkCoqDerivation, recurseIntoAttrs, single ? false, coqPackages, coq, equations, version ? null }@args: with builtins // lib; @@ -36,8 +36,10 @@ let derivation = mkCoqDerivation ({ inherit version pname defaultVersion release releaseRev repo owner; + extraNativeBuildInputs = [ which ]; mlPlugin = true; - propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps; + extraBuildInputs = [ coq.ocamlPackages.zarith ]; + propagatedBuildInputs = [ equations ] ++ 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 83333b3e1bf02..26bd38f72df11 100644 --- a/pkgs/development/coq-modules/metalib/default.nix +++ b/pkgs/development/coq-modules/metalib/default.nix @@ -13,6 +13,7 @@ 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 cbf1469e1f035..e112512ec5c72 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; - nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); - propagatedBuildInputs = (with coq.ocamlPackages; [ num ]); + extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); + extraBuildInputs = (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 a0417ca978d1e..bcc391c4f724c 100644 --- a/pkgs/development/coq-modules/simple-io/default.nix +++ b/pkgs/development/coq-modules/simple-io/default.nix @@ -11,9 +11,11 @@ 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 ebaebe6974e3e..0389b45fb5cdd 100644 --- a/pkgs/development/coq-modules/smtcoq/default.nix +++ b/pkgs/development/coq-modules/smtcoq/default.nix @@ -13,11 +13,9 @@ mkCoqDerivation { { case = isEq "8.13"; out = "itp22"; } ] null; - propagatedBuildInputs = [ trakt cvc4 ] - ++ lib.optionals (!stdenv.isDarwin) [ veriT ] - ++ (with coq.ocamlPackages; [ num zarith ]); - mlPlugin = true; - nativeBuildInputs = with coq.ocamlPackages; [ ocamlbuild ]; + propagatedBuildInputs = [ trakt cvc4 ] ++ lib.optionals (!stdenv.isDarwin) [ veriT ]; + extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml ocamlbuild ]; + extraBuildInputs = with coq.ocamlPackages; [ findlib num zarith ]; meta = { description = "Communication between Coq and SAT/SMT solvers "; diff --git a/pkgs/development/ocaml-modules/elpi/default.nix b/pkgs/development/ocaml-modules/elpi/default.nix index cc84284251772..0770f3a48d484 100644 --- a/pkgs/development/ocaml-modules/elpi/default.nix +++ b/pkgs/development/ocaml-modules/elpi/default.nix @@ -1,13 +1,12 @@ -{ stdenv, lib, fetchzip, bash -, buildDunePackage, camlp5 +{ stdenv, lib, fetchzip, buildDunePackage, camlp5 , re, perl, ncurses , ppxlib, ppx_deriving , ppxlib_0_15, ppx_deriving_0_15 -, coqPackages , version ? "1.14.1" }: with lib; -let fetched = coqPackages.metaFetch ({ +let fetched = import ../../../build-support/coq/meta-fetch/default.nix + {inherit lib stdenv fetchzip; } ({ release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis="; release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r"; release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka"; @@ -33,11 +32,6 @@ buildDunePackage rec { else [ ppxlib_0_15 ppx_deriving_0_15 ] ); - patchPhase = '' - sed -e "s/SHELL:=/SHELL?=/" -i Makefile || true - ''; - buildPhase = "SHELL=${bash} make build"; - meta = { description = "Embeddable λProlog Interpreter"; license = licenses.lgpl21Plus; diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 6cfd34aa279b4..9c3e666c5b3bc 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -1,5 +1,4 @@ -{ lib, stdenv, fetchzip -, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09 +{ lib, stdenv, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09 , ocamlPackages_4_10, ocamlPackages_4_12, fetchpatch, makeWrapper, coq2html }@args: let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in @@ -9,8 +8,6 @@ let inherit coq lib; coqPackages = self; - metaFetch = import ../build-support/coq/meta-fetch/default.nix - {inherit lib stdenv fetchzip; }; mkCoqDerivation = callPackage ../build-support/coq {}; contribs = recurseIntoAttrs |