coqPackages: etc

- use propagatedBuildInputs to make sure ocaml plugin stuff is in path
- updated coqPackage.heq (broken url)
- fixed use of `DESTDIR` and `COQMF_COQLIB` in mkCoqDerivation
- adding `COQCORELIB` environement variable to put ocaml plugin files in the right place
- make metaFetch available from `coqPackages`
This commit is contained in:
Cyril Cohen 2021-02-19 19:34:30 +01:00 committed by Vincent Laporte
parent a34b9c1f1c
commit 7e589a45ef
34 changed files with 128 additions and 113 deletions

View file

@ -29,14 +29,19 @@ 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, * `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, * `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`, * `namePrefix` (optional, defaults to `[ "coq" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
* `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, * `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).
* `extraBuildInputs` (optional), this allows to add more build inputs, * `extraNativeBuildInputs` (optional, deprecated), an additional list of derivation to add to `nativeBuildInputs`,
* `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. * `overrideNativeBuildInputs` (optional) replaces the default list of derivation to which `nativeBuildInputs` and `extraNativeBuildInputs` adds extra elements,
* `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"`, * `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"`,
* `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. * `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. * `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. * `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 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. * `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.
* `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`, * `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). * `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`. * `dropAttrs`, `keepAttrs`, `dropDerivationAttrs` are all optional and allow to tune which attribute is added or removed from the final call to `mkDerivation`.

View file

@ -70,9 +70,9 @@ let
{ case = range "8.7" "8.10"; out = ocamlPackages_4_09; } { case = range "8.7" "8.10"; out = ocamlPackages_4_09; }
{ case = range "8.5" "8.6"; out = ocamlPackages_4_05; } { case = range "8.5" "8.6"; out = ocamlPackages_4_05; }
] ocamlPackages_4_12; ] ocamlPackages_4_12;
ocamlNativeBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ] ocamlNativeBuildInputs = [ ocamlPackages.ocaml ]
++ optional (coqAtLeast "8.14") ocamlPackages.dune_2; ++ optional (coqAtLeast "8.14") ocamlPackages.dune_2;
ocamlBuildInputs = [] ocamlBuildInputs = [ ocamlPackages.findlib ]
++ optional (!coqAtLeast "8.10") ocamlPackages.camlp5 ++ optional (!coqAtLeast "8.10") ocamlPackages.camlp5
++ optional (!coqAtLeast "8.13") ocamlPackages.num ++ optional (!coqAtLeast "8.13") ocamlPackages.num
++ optional (coqAtLeast "8.13") ocamlPackages.zarith; ++ optional (coqAtLeast "8.13") ocamlPackages.zarith;
@ -136,13 +136,15 @@ self = stdenv.mkDerivation {
++ optional buildIde copyDesktopItems ++ optional buildIde copyDesktopItems
++ optional (buildIde && coqAtLeast "8.10") wrapGAppsHook ++ optional (buildIde && coqAtLeast "8.10") wrapGAppsHook
++ optional (!coqAtLeast "8.6") gnumake42; ++ optional (!coqAtLeast "8.6") gnumake42;
buildInputs = [ ncurses ] ++ ocamlBuildInputs buildInputs = [ ncurses ]
++ optionals buildIde ++ optionals buildIde
(if coqAtLeast "8.10" (if coqAtLeast "8.10"
then [ ocamlPackages.lablgtk3-sourceview3 glib gnome.adwaita-icon-theme ] then [ ocamlPackages.lablgtk3-sourceview3 glib gnome.adwaita-icon-theme ]
else [ ocamlPackages.lablgtk ]) else [ ocamlPackages.lablgtk ])
; ;
propagatedBuildInputs = ocamlBuildInputs;
postPatch = '' postPatch = ''
UNAME=$(type -tp uname) UNAME=$(type -tp uname)
RM=$(type -tp rm) RM=$(type -tp rm)

View file

@ -1,4 +1,4 @@
{ lib, stdenv, coqPackages, coq, fetchzip }@args: { lib, stdenv, coqPackages, coq, which, fetchzip }@args:
let lib = import ./extra-lib.nix {inherit (args) lib;}; in let lib = import ./extra-lib.nix {inherit (args) lib;}; in
with builtins; with lib; with builtins; with lib;
let let
@ -15,8 +15,12 @@ in
releaseRev ? (v: v), releaseRev ? (v: v),
displayVersion ? {}, displayVersion ? {},
release ? {}, release ? {},
buildInputs ? [],
nativeBuildInputs ? [],
extraBuildInputs ? [], extraBuildInputs ? [],
extraNativeBuildInputs ? [], extraNativeBuildInputs ? [],
overrideBuildInputs ? [],
overrideNativeBuildInputs ? [],
namePrefix ? [ "coq" ], namePrefix ? [ "coq" ],
enableParallelBuilding ? true, enableParallelBuilding ? true,
extraInstallFlags ? [], extraInstallFlags ? [],
@ -35,7 +39,11 @@ let
args-to-remove = foldl (flip remove) ([ args-to-remove = foldl (flip remove) ([
"version" "fetcher" "repo" "owner" "domain" "releaseRev" "version" "fetcher" "repo" "owner" "domain" "releaseRev"
"displayVersion" "defaultVersion" "useMelquiondRemake" "displayVersion" "defaultVersion" "useMelquiondRemake"
"release" "extraBuildInputs" "extraNativeBuildInputs" "extraPropagatedBuildInputs" "namePrefix" "release"
"buildInputs" "nativeBuildInputs"
"extraBuildInputs" "extraNativeBuildInputs"
"overrideBuildInputs" "overrideNativeBuildInputs"
"namePrefix"
"meta" "useDune2ifVersion" "useDune2" "opam-name" "meta" "useDune2ifVersion" "useDune2" "opam-name"
"extraInstallFlags" "setCOQBIN" "mlPlugin" "extraInstallFlags" "setCOQBIN" "mlPlugin"
"dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs; "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
@ -57,9 +65,16 @@ let
] "") + optionalString (v == null) "-broken"; ] "") + optionalString (v == null) "-broken";
append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-"; append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-";
prefix-name = foldl append-version "" namePrefix; 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); 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 in
stdenv.mkDerivation (removeAttrs ({ stdenv.mkDerivation (removeAttrs ({
@ -68,12 +83,12 @@ stdenv.mkDerivation (removeAttrs ({
inherit (fetched) version src; inherit (fetched) version src;
nativeBuildInputs = [ coq ] nativeBuildInputs = args.overrideNativeBuildInputs
++ optionals useDune2 [coq.ocaml coq.ocamlPackages.dune_2] or ([ which ] ++ optional useDune2 coq.ocamlPackages.dune_2
++ optionals mlPlugin coq.ocamlNativeBuildInputs ++ optional (useDune2 || mlPlugin) coq.ocaml
++ extraNativeBuildInputs; ++ (args.nativeBuildInputs or []) ++ extraNativeBuildInputs);
buildInputs = optionals mlPlugin coq.ocamlBuildInputs buildInputs = args.overrideBuildInputs
++ extraBuildInputs; or ([ coq ] ++ (args.buildInputs or []) ++ extraBuildInputs);
inherit enableParallelBuilding; inherit enableParallelBuilding;
meta = ({ platforms = coq.meta.platforms; } // meta = ({ platforms = coq.meta.platforms; } //
@ -88,9 +103,7 @@ stdenv.mkDerivation (removeAttrs ({
// (optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; }) // (optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; })
// (optionalAttrs (!args?installPhase && !args?useMelquiondRemake) { // (optionalAttrs (!args?installPhase && !args?useMelquiondRemake) {
installFlags = installFlags =
[ "${var-coqlib-install}=$(out)/lib/coq/${coq.coq-version}/" ] ++ [ "DESTDIR=$(out)" ] ++ coqlib-flags ++ docdir-flags ++
optional (match ".*doc$" (args.installTargets or "") != null)
"DOCDIR=$(out)/share/coq/${coq.coq-version}/" ++
extraInstallFlags; extraInstallFlags;
}) })
// (optionalAttrs useDune2 { // (optionalAttrs useDune2 {

View file

@ -20,7 +20,7 @@ with lib; mkCoqDerivation {
release."1.4.0".rev = "168c6b86c7d3f87ee51791f795a8828b1521589a"; release."1.4.0".rev = "168c6b86c7d3f87ee51791f795a8828b1521589a";
release."1.4.0".sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm"; release."1.4.0".sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm";
extraBuildInputs = [ bignums ]; propagatedBuildInputs = [ bignums ];
enableParallelBuilding = false; enableParallelBuilding = false;
meta = { meta = {

View file

@ -8,7 +8,7 @@ with lib; mkCoqDerivation {
release."20170921".rev = "e3557740a699167e6adb1a65855509d55a392fa1"; release."20170921".rev = "e3557740a699167e6adb1a65855509d55a392fa1";
release."20170921".sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v"; release."20170921".sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v";
extraBuildInputs = [ autoconf automake ]; nativeBuildInputs = [ autoconf automake ];
preConfigure = '' preConfigure = ''
patchShebangs ./autogen.sh patchShebangs ./autogen.sh

View file

@ -36,8 +36,7 @@ let recent = lib.versions.isGe "8.7" coq.coq-version; in
"substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native"; "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native";
mlPlugin = true; mlPlugin = true;
extraNativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild; nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild;
extraBuildInputs = lib.optional recent coq.ocamlPackages.num;
propagatedBuildInputs = [ ssreflect ] propagatedBuildInputs = [ ssreflect ]
++ lib.optionals recent [ coq-ext-lib simple-io ]; ++ lib.optionals recent [ coq-ext-lib simple-io ];
extraInstallFlags = [ "-f Makefile.coq" ]; extraInstallFlags = [ "-f Makefile.coq" ];

View file

@ -31,7 +31,7 @@ mkCoqDerivation {
release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf"; release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf";
release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0="; release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0=";
releaseRev = v: "v${v}"; releaseRev = v: "v${v}";
extraBuildInputs = [ ITree ]; buildInputs = [ ITree ];
propagatedBuildInputs = [ compcert ]; propagatedBuildInputs = [ compcert ];
preConfigure = '' preConfigure = ''

View file

@ -5,7 +5,7 @@ with lib; mkCoqDerivation {
owner = "coq"; owner = "coq";
displayVersion = { bignums = ""; }; displayVersion = { bignums = ""; };
inherit version; 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; then "${coq.coq-version}.0" else null;
release."8.15.0".sha256 = "093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns"; release."8.15.0".sha256 = "093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns";

View file

@ -1,5 +1,5 @@
{ lib, fetchzip, mkCoqDerivation, coq, flocq, compcert { lib, fetchzip, mkCoqDerivation, coq, flocq, compcert
, ocamlPackages, fetchpatch, makeWrapper, coq2html , fetchpatch, makeWrapper, coq2html
, stdenv, tools ? stdenv.cc , stdenv, tools ? stdenv.cc
, version ? null , version ? null
}: }:
@ -15,9 +15,9 @@ let compcert = mkCoqDerivation rec {
releaseRev = v: "v${v}"; releaseRev = v: "v${v}";
defaultVersion = with versions; switch coq.version [ 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 = 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; ] null;
release = { release = {
@ -26,8 +26,9 @@ let compcert = mkCoqDerivation rec {
"3.10".sha256 = "sha256:19rmx8r8v46101ij5myfrz60arqjy7q3ra3fb8mxqqi3c8c4l4j6"; "3.10".sha256 = "sha256:19rmx8r8v46101ij5myfrz60arqjy7q3ra3fb8mxqqi3c8c4l4j6";
}; };
mlPlugin = true;
nativeBuildInputs = [ makeWrapper ]; nativeBuildInputs = [ makeWrapper ];
buildInputs = with ocamlPackages; [ ocaml findlib menhir menhirLib ] ++ [ coq coq2html ]; buildInputs = with coq.ocamlPackages; [ menhir menhirLib ] ++ [ coq2html ];
propagatedBuildInputs = [ flocq ]; propagatedBuildInputs = [ flocq ];
enableParallelBuilding = true; enableParallelBuilding = true;
@ -48,9 +49,13 @@ let compcert = mkCoqDerivation rec {
''; '';
installTargets = "documentation install"; installTargets = "documentation install";
installFlags = []; # trust ./configure
preInstall = ''
mkdir -p $out/share/man
mkdir -p $man/share
'';
postInstall = '' postInstall = ''
# move man into place # move man into place
mkdir -p $man/share
mv $out/share/man/ $man/share/ mv $out/share/man/ $man/share/
# move docs into place # move docs into place

View file

@ -1,34 +1,18 @@
{ lib, mkCoqDerivation, coq, mathcomp, version ? null }: { lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
with lib; mkCoqDerivation { with lib; mkCoqDerivation {
pname = "coq-bits"; pname = "coq-bits";
repo = "bits"; repo = "bits";
inherit version; inherit version;
defaultVersion = defaultVersion = with versions; switch coq.coq-version [
if versions.isGe "8.10" coq.version { case = isGe "8.10"; out = "1.1.0"; }
then "1.1.0" { case = isGe "8.7"; out = "1.0.0"; }
else if versions.isGe "8.7" coq.version ] null;
then "1.0.0"
else null;
release = { release."1.1.0".sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE=";
"1.0.0" = { release."1.0.0".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";
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 = { meta = {
description = "A formalization of bitset operations in Coq"; description = "A formalization of bitset operations in Coq";

View file

@ -7,7 +7,7 @@ with builtins; with lib; let
{ case = "8.13"; out = { version = "1.13.7"; };} { case = "8.13"; out = { version = "1.13.7"; };}
{ case = "8.14"; out = { version = "1.13.7"; };} { case = "8.14"; out = { version = "1.13.7"; };}
{ case = "8.15"; out = { version = "1.14.1"; };} { case = "8.15"; out = { version = "1.14.1"; };}
] {}); ] { version = "1.14.1"; } );
in mkCoqDerivation { in mkCoqDerivation {
pname = "elpi"; pname = "elpi";
repo = "coq-elpi"; repo = "coq-elpi";
@ -48,8 +48,8 @@ in mkCoqDerivation {
release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b"; release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
releaseRev = v: "v${v}"; releaseRev = v: "v${v}";
extraNativeBuildInputs = [ which elpi ];
mlPlugin = true; mlPlugin = true;
propagatedBuildInputs = [ elpi ];
meta = { meta = {
description = "Coq plugin embedding ELPI."; description = "Coq plugin embedding ELPI.";

View file

@ -1,6 +1,6 @@
{ coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials, { coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials,
mathcomp-real-closed, mathcomp-real-closed,
lib, which, version ? null }: lib, version ? null }:
with lib; with lib;
@ -22,7 +22,6 @@ with lib;
release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk"; release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk";
release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24"; release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
extraBuildInputs = [ which ];
propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ]; propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ];
meta = { meta = {

View file

@ -28,8 +28,10 @@ with lib; mkCoqDerivation {
release."1.3-coq8.12".sha256 = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8"; release."1.3-coq8.12".sha256 = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8";
release."1.3-coq8.11".sha256 = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b"; release."1.3-coq8.11".sha256 = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b";
release."1.3-coq8.10".sha256 = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd"; release."1.3-coq8.10".sha256 = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd";
release."1.1.1-coq8.9".sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9"; release."1.1.1-coq8.9" = { sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9";
release."1.1-coq8.8".sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h"; 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.13".version = "1.3.1";
release."1.3.1-coq8.12".version = "1.3.1"; release."1.3.1-coq8.12".version = "1.3.1";

View file

@ -20,7 +20,6 @@ with lib; mkCoqDerivation {
release."8.7.2".sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k"; release."8.7.2".sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k";
releaseRev = v: "v${v}"; releaseRev = v: "v${v}";
extraBuildInputs = [ which ];
propagatedBuildInputs = [ bignums ]; propagatedBuildInputs = [ bignums ];
meta = with lib; { meta = with lib; {

View file

@ -14,9 +14,7 @@ mkCoqDerivation {
release."8.14".sha256 = "sha256:1k8f8idjnx0mf4z479vcx55iz42rjxrbplbznv80m2famxakq03c"; release."8.14".sha256 = "sha256:1k8f8idjnx0mf4z479vcx55iz42rjxrbplbznv80m2famxakq03c";
release."20201124".rev = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e"; release."20201124".rev = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e";
release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ="; release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ=";
mlPlugin = true;
extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml findlib ];
meta = { meta = {
license = licenses.lgpl3Only; license = licenses.lgpl3Only;
maintainers = [ maintainers.siraben ]; maintainers = [ maintainers.siraben ];

View file

@ -1,4 +1,4 @@
{ lib, mkCoqDerivation, which, autoconf, { lib, mkCoqDerivation, autoconf,
coq, ssreflect, version ? null }: coq, ssreflect, version ? null }:
with lib; mkCoqDerivation { with lib; mkCoqDerivation {
@ -16,7 +16,7 @@ with lib; mkCoqDerivation {
release."3.0.2".sha256 = "1rqfbbskgz7b1bcpva8wh3v3456sq2364y804f94sc8y5sij23nl"; release."3.0.2".sha256 = "1rqfbbskgz7b1bcpva8wh3v3456sq2364y804f94sc8y5sij23nl";
releaseRev = v: "coquelicot-${v}"; releaseRev = v: "coquelicot-${v}";
extraNativeBuildInputs = [ which autoconf ]; nativeBuildInputs = [ autoconf ];
propagatedBuildInputs = [ ssreflect ]; propagatedBuildInputs = [ ssreflect ];
useMelquiondRemake.logpath = "Coquelicot"; useMelquiondRemake.logpath = "Coquelicot";

View file

@ -39,9 +39,9 @@ mkCoqDerivation {
release."0.6".sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n"; release."0.6".sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n";
releaseRev = v: "v${v}"; releaseRev = v: "v${v}";
extraNativeBuildInputs = [ autoreconfHook ]; nativeBuildInputs = [ autoreconfHook ];
mlPlugin = true; mlPlugin = true;
extraBuildInputs = [ coq.ocamlPackages.ocamlgraph ]; buildInputs = [ coq.ocamlPackages.ocamlgraph ];
# dpd_compute.ml uses deprecated Pervasives.compare # dpd_compute.ml uses deprecated Pervasives.compare
# Versions prior to 0.6.5 do not have the WARN_ERR build flag # Versions prior to 0.6.5 do not have the WARN_ERR build flag

View file

@ -8,10 +8,10 @@ with lib; mkCoqDerivation rec {
inherit version; inherit version;
defaultVersion = if coq.coq-version == "8.5" then "2016-10-24" else null; defaultVersion = if coq.coq-version == "8.5" then "2016-10-24" else null;
release."2016-10-24".rev = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a"; release."2016-10-24".rev = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a";
release."2016-10-24".sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64"; release."2016-10-24".sha256 = "16y57vibq3f5i5avgj80f4i3aw46wdwzx36k5d3pf3qk17qrlrdi";
mlPlugin = true; mlPlugin = true;
extraBuildInputs = [ python27 ]; buildInputs = [ python27 ];
prePatch = "patchShebangs etc/coq-scripts"; prePatch = "patchShebangs etc/coq-scripts";

View file

@ -1,4 +1,4 @@
{ lib, which, autoconf, automake, { lib, bash, autoconf, automake,
mkCoqDerivation, coq, version ? null }: mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation { with lib; mkCoqDerivation {
@ -16,7 +16,7 @@ with lib; mkCoqDerivation {
release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj"; release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj";
releaseRev = v: "flocq-${v}"; releaseRev = v: "flocq-${v}";
nativeBuildInputs = [ which autoconf ]; nativeBuildInputs = [ bash autoconf ];
mlPlugin = true; mlPlugin = true;
useMelquiondRemake.logpath = "Flocq"; useMelquiondRemake.logpath = "Flocq";

View file

@ -13,7 +13,7 @@ with lib; mkCoqDerivation {
release."1.4.4".sha256 = "114q2hgw64j6kqa9mg3qcp1nlf0ia46z2xadq81fnkxqm856ml7l"; release."1.4.4".sha256 = "114q2hgw64j6kqa9mg3qcp1nlf0ia46z2xadq81fnkxqm856ml7l";
releaseRev = v: "gappalib-coq-${v}"; releaseRev = v: "gappalib-coq-${v}";
extraNativeBuildInputs = [ which autoconf ]; nativeBuildInputs = [ autoconf ];
mlPlugin = true; mlPlugin = true;
propagatedBuildInputs = [ flocq ]; propagatedBuildInputs = [ flocq ];
useMelquiondRemake.logpath = "Gappa"; useMelquiondRemake.logpath = "Gappa";

View file

@ -1,22 +1,26 @@
{lib, fetchzip, mkCoqDerivation, coq, version ? null }: {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 { with lib; mkCoqDerivation {
pname = "heq"; pname = "heq";
repo = "Heq"; repo = "Heq";
owner = "gil"; owner = "gil.hur";
domain = "mpi-sws.org"; domain = "sf.snu.ac.kr";
inherit version fetcher; inherit version fetcher;
defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null; defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null;
release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74"; release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74";
mlPlugin = true; mlPlugin = true;
propagatedBuildInputs = [ coq ];
extraInstallFlags = [ "COQLIB=$out/lib/coq/${coq.coq-version}" ];
preBuild = "cd src"; preBuild = "cd src";
extraInstallFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
meta = { 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"; description = "Heq : a Coq library for Heterogeneous Equality";
maintainers = with maintainers; [ jwiegley ]; maintainers = with maintainers; [ jwiegley ];
}; };

View file

@ -1,4 +1,4 @@
{ lib, mkCoqDerivation, which, coq, coq-elpi, version ? null }: { lib, mkCoqDerivation, coq, coq-elpi, version ? null }:
with lib; let hb = mkCoqDerivation { with lib; let hb = mkCoqDerivation {
pname = "hierarchy-builder"; pname = "hierarchy-builder";
@ -17,13 +17,10 @@ with lib; let hb = mkCoqDerivation {
release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h"; release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
releaseRev = v: "v${v}"; releaseRev = v: "v${v}";
extraNativeBuildInputs = [ which ];
propagatedBuildInputs = [ coq-elpi ]; propagatedBuildInputs = [ coq-elpi ];
mlPlugin = true; mlPlugin = true;
installFlags = [ "DESTDIR=$(out)" "COQMF_COQLIB=lib/coq/${coq.coq-version}" ];
extraInstallFlags = [ "VFILES=structures.v" ]; extraInstallFlags = [ "VFILES=structures.v" ];
meta = { meta = {

View file

@ -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 { mkCoqDerivation rec {
pname = "interval"; pname = "interval";
@ -20,8 +21,9 @@ mkCoqDerivation rec {
release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz"; release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz";
releaseRev = v: "interval-${v}"; releaseRev = v: "interval-${v}";
extraNativeBuildInputs = [ which autoconf ]; nativeBuildInputs = [ autoconf ];
propagatedBuildInputs = [ bignums coquelicot flocq mathcomp-ssreflect mathcomp-fingroup ] 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 ]; ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
useMelquiondRemake.logpath = "Interval"; useMelquiondRemake.logpath = "Interval";
mlPlugin = true; mlPlugin = true;

View file

@ -17,7 +17,7 @@ mkCoqDerivation rec {
] null; ] null;
mlPlugin = true; mlPlugin = true;
extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
enableParallelBuilding = false; enableParallelBuilding = false;
meta = { meta = {

View file

@ -17,7 +17,6 @@ with lib; mkCoqDerivation {
release."0.1-8.7".rev = "v0.1-8.7"; release."0.1-8.7".rev = "v0.1-8.7";
release."0.1-8.7".sha256 = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0"; release."0.1-8.7".sha256 = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0";
nativeBuildInputs = [ which ];
mlPlugin = true; mlPlugin = true;
meta = { meta = {

View file

@ -9,7 +9,7 @@ with lib; mkCoqDerivation {
release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby"; release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby";
release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw"; release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw";
extraBuildInputs = [ bignums ]; propagatedBuildInputs = [ bignums ];
meta = { meta = {
homepage = "https://math-classes.github.io"; homepage = "https://math-classes.github.io";

View file

@ -10,9 +10,9 @@
# See the documentation at doc/languages-frameworks/coq.section.md. # # 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, mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false,
coqPackages, coq, ocamlPackages, version ? null }@args: coqPackages, coq, version ? null }@args:
with builtins // lib; with builtins // lib;
let let
repo = "math-comp"; repo = "math-comp";
@ -60,8 +60,9 @@ let
inherit version pname defaultVersion release releaseRev repo owner; inherit version pname defaultVersion release releaseRev repo owner;
mlPlugin = versions.isLe "8.6" coq.coq-version; mlPlugin = versions.isLe "8.6" coq.coq-version;
extraNativeBuildInputs = [ which ] ++ optionals withDoc [ graphviz lua ]; nativeBuildInputs = optionals withDoc [ graphviz lua ];
extraBuildInputs = [ ncurses ] ++ mathcomp-deps; buildInputs = [ ncurses ];
propagatedBuildInputs = mathcomp-deps;
buildFlags = optional withDoc "doc"; buildFlags = optional withDoc "doc";

View file

@ -1,4 +1,4 @@
{ lib, which, fetchzip, { lib, fetchzip,
mkCoqDerivation, recurseIntoAttrs, single ? false, mkCoqDerivation, recurseIntoAttrs, single ? false,
coqPackages, coq, equations, version ? null }@args: coqPackages, coq, equations, version ? null }@args:
with builtins // lib; with builtins // lib;
@ -36,10 +36,8 @@ let
derivation = mkCoqDerivation ({ derivation = mkCoqDerivation ({
inherit version pname defaultVersion release releaseRev repo owner; inherit version pname defaultVersion release releaseRev repo owner;
extraNativeBuildInputs = [ which ];
mlPlugin = true; mlPlugin = true;
extraBuildInputs = [ coq.ocamlPackages.zarith ]; propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
propagatedBuildInputs = [ equations ] ++ metacoq-deps;
patchPhase = '' patchPhase = ''
patchShebangs ./configure.sh patchShebangs ./configure.sh

View file

@ -13,7 +13,6 @@ with lib; mkCoqDerivation {
release."8.10".sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs"; release."8.10".sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs";
sourceRoot = "source/Metalib"; sourceRoot = "source/Metalib";
installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}";
meta = { meta = {
license = licenses.mit; license = licenses.mit;

View file

@ -24,8 +24,8 @@ mkCoqDerivation rec {
] null; ] null;
mlPlugin = true; mlPlugin = true;
extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
extraBuildInputs = (with coq.ocamlPackages; [ num ]); propagatedBuildInputs = (with coq.ocamlPackages; [ num ]);
postPatch = '' postPatch = ''
for p in Make Makefile.coq.local for p in Make Makefile.coq.local

View file

@ -11,11 +11,9 @@ with lib; mkCoqDerivation {
] null; ] null;
release."1.7.0".sha256 = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci"; release."1.7.0".sha256 = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci";
release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax"; release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax";
extraNativeBuildInputs = (with coq.ocamlPackages; [ cppo zarith ]);
propagatedBuildInputs = [ coq-ext-lib ]
++ (with coq.ocamlPackages; [ ocaml ocamlbuild ]);
mlPlugin = true; mlPlugin = true;
nativeBuildInputs = coq.ocamlPackages.cppo;
propagatedBuildInputs = [ coq-ext-lib coq.ocamlPackages.ocamlbuild ];
doCheck = true; doCheck = true;
checkTarget = "test"; checkTarget = "test";

View file

@ -13,9 +13,11 @@ mkCoqDerivation {
{ case = isEq "8.13"; out = "itp22"; } { case = isEq "8.13"; out = "itp22"; }
] null; ] null;
propagatedBuildInputs = [ trakt cvc4 ] ++ lib.optionals (!stdenv.isDarwin) [ veriT ]; propagatedBuildInputs = [ trakt cvc4 ]
extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml ocamlbuild ]; ++ lib.optionals (!stdenv.isDarwin) [ veriT ]
extraBuildInputs = with coq.ocamlPackages; [ findlib num zarith ]; ++ (with coq.ocamlPackages; [ num zarith ]);
mlPlugin = true;
nativeBuildInputs = with coq.ocamlPackages; [ ocamlbuild ];
meta = { meta = {
description = "Communication between Coq and SAT/SMT solvers "; description = "Communication between Coq and SAT/SMT solvers ";

View file

@ -1,12 +1,13 @@
{ stdenv, lib, fetchzip, buildDunePackage, camlp5 { stdenv, lib, fetchzip, bash
, buildDunePackage, camlp5
, re, perl, ncurses , re, perl, ncurses
, ppxlib, ppx_deriving , ppxlib, ppx_deriving
, ppxlib_0_15, ppx_deriving_0_15 , ppxlib_0_15, ppx_deriving_0_15
, coqPackages
, version ? "1.14.1" , version ? "1.14.1"
}: }:
with lib; with lib;
let fetched = import ../../../build-support/coq/meta-fetch/default.nix let fetched = coqPackages.metaFetch ({
{inherit lib stdenv fetchzip; } ({
release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis="; release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis=";
release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r"; release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r";
release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka"; release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka";
@ -32,6 +33,11 @@ buildDunePackage rec {
else [ ppxlib_0_15 ppx_deriving_0_15 ] else [ ppxlib_0_15 ppx_deriving_0_15 ]
); );
patchPhase = ''
sed -e "s/SHELL:=/SHELL?=/" -i Makefile || true
'';
buildPhase = "SHELL=${bash} make build";
meta = { meta = {
description = "Embeddable λProlog Interpreter"; description = "Embeddable λProlog Interpreter";
license = licenses.lgpl21Plus; license = licenses.lgpl21Plus;

View file

@ -1,4 +1,5 @@
{ lib, stdenv, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09 { lib, stdenv, fetchzip
, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
, ocamlPackages_4_10, ocamlPackages_4_12, fetchpatch, makeWrapper, coq2html , ocamlPackages_4_10, ocamlPackages_4_12, fetchpatch, makeWrapper, coq2html
}@args: }@args:
let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in
@ -8,6 +9,8 @@ let
inherit coq lib; inherit coq lib;
coqPackages = self; coqPackages = self;
metaFetch = import ../build-support/coq/meta-fetch/default.nix
{inherit lib stdenv fetchzip; };
mkCoqDerivation = callPackage ../build-support/coq {}; mkCoqDerivation = callPackage ../build-support/coq {};
contribs = recurseIntoAttrs contribs = recurseIntoAttrs