diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 03ca07274c51..fc3a72e49ad5 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -19,6 +19,7 @@ ocamlPackages_4_10, ocamlPackages_4_12, ocamlPackages_4_14, + rocqPackages, # for versions >= 9.0 that are transition shims on top of Rocq ncurses, buildIde ? null, # default is true for Coq < 8.14 and false for Coq >= 8.14 glib, @@ -27,7 +28,6 @@ makeDesktopItem, copyDesktopItems, csdp ? null, - rocq-core, # for versions >= 9.0 that are transition shims on top of Rocq version, coq-version ? null, }@args: @@ -148,7 +148,6 @@ let self = stdenv.mkDerivation { pname = "coq"; inherit (fetched) version src; - exact-version = args.version; passthru = { inherit coq-version; @@ -161,6 +160,7 @@ let findlib num ; + rocqPackages = lib.optionalAttrs (coqAtLeast "8.21") rocqPackages; emacsBufferSetup = pkgs: '' ; Propagate coq paths to children (inherit-local-permanent coq-prog-name "${self}/bin/coqtop") @@ -334,7 +334,7 @@ if coqAtLeast "8.21" then self.overrideAttrs (o: { # coq-core is now a shim for rocq propagatedBuildInputs = o.propagatedBuildInputs ++ [ - (rocq-core.override { version = o.exact-version; }) + rocqPackages.rocq-core ]; buildPhase = '' runHook preBuild diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix index 3a6ce9bd4a31..533319ff9ec2 100644 --- a/pkgs/development/coq-modules/bignums/default.nix +++ b/pkgs/development/coq-modules/bignums/default.nix @@ -2,85 +2,62 @@ lib, mkCoqDerivation, coq, - rocqPackages_9_0, - rocqPackages_9_1, - rocqPackages, stdlib, version ? null, }: -(mkCoqDerivation { - pname = "bignums"; - owner = "rocq-community"; - inherit version; - defaultVersion = - let - case = case: out: { inherit case out; }; - in - with lib.versions; - lib.switch coq.coq-version [ - (case (range "9.0" "9.1") "9.0.0+rocq${coq.coq-version}") - (case (range "8.13" "8.20") "9.0.0+coq${coq.coq-version}") - (case (range "8.6" "8.17") "${coq.coq-version}.0") - ] null; +let + derivation = mkCoqDerivation { + pname = "bignums"; + owner = "rocq-community"; + inherit version; + defaultVersion = + let + case = case: out: { inherit case out; }; + in + with lib.versions; + lib.switch coq.coq-version [ + (case (range "8.13" "8.20") "9.0.0+coq${coq.coq-version}") + (case (range "8.6" "8.17") "${coq.coq-version}.0") + ] null; - release."9.0.0+rocq9.1".sha256 = "sha256-MSjlfJs3JOakuShOj+isNlus0bKlZ+rkvzRoKZQK5RQ="; - release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78="; - release."9.0.0+coq8.20".sha256 = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY="; - release."9.0.0+coq8.19".sha256 = "sha256-02uL+qWbUveHe67zKfc8w3U0iN3X2DKBsvP3pKpW8KQ="; - release."9.0.0+coq8.18".sha256 = "sha256-vLeJ0GNKl4M84Uj2tAwlrxJOSR6VZoJQvdlDhxJRge8="; - release."9.0.0+coq8.17".sha256 = "sha256-Mn85LqxJKPDIfpxRef9Uh5POwOKlTQ7jsMVz1wnQwuY="; - release."9.0.0+coq8.16".sha256 = "sha256-pwFTl4Unr2ZIirAB3HTtfhL2YN7G/Pg88RX9AhKWXbE="; - release."9.0.0+coq8.15".sha256 = "sha256-2oGOANn3XULHNIlyqjZ5ppQTQa2QF1zzf3YjHAd/pjo="; - release."9.0.0+coq8.14".sha256 = "sha256-qTU152Dz34W6nFZ0pPbja9ouUm/714ZrLQ/Z4N/HIC4="; - release."9.0.0+coq8.13".sha256 = "sha256-zvAqV3VAB7cN+nlMhjSXzxuDkdd387ju2VSb2EUthI0="; - release."8.17.0".sha256 = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw="; - release."8.16.0".sha256 = "sha256-DH3iWwatPlhhCVYVlgL2WLkvneSVzSXUiKo2e0+1zR4="; - release."8.15.0".sha256 = "093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns"; - release."8.14.0".sha256 = "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06"; - release."8.13.0".sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"; - release."8.12.0".sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8"; - release."8.11.0".sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"; - release."8.10.0".sha256 = "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5"; - release."8.9.0".sha256 = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01"; - release."8.8.0".sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg"; - release."8.7.0".sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl"; - release."8.6.0".rev = "v8.6.0"; - release."8.6.0".sha256 = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj"; - releaseRev = v: "${if lib.versions.isGe "9.0" v then "v" else "V"}${v}"; + release."9.0.0+coq8.20".sha256 = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY="; + release."9.0.0+coq8.19".sha256 = "sha256-02uL+qWbUveHe67zKfc8w3U0iN3X2DKBsvP3pKpW8KQ="; + release."9.0.0+coq8.18".sha256 = "sha256-vLeJ0GNKl4M84Uj2tAwlrxJOSR6VZoJQvdlDhxJRge8="; + release."9.0.0+coq8.17".sha256 = "sha256-Mn85LqxJKPDIfpxRef9Uh5POwOKlTQ7jsMVz1wnQwuY="; + release."9.0.0+coq8.16".sha256 = "sha256-pwFTl4Unr2ZIirAB3HTtfhL2YN7G/Pg88RX9AhKWXbE="; + release."9.0.0+coq8.15".sha256 = "sha256-2oGOANn3XULHNIlyqjZ5ppQTQa2QF1zzf3YjHAd/pjo="; + release."9.0.0+coq8.14".sha256 = "sha256-qTU152Dz34W6nFZ0pPbja9ouUm/714ZrLQ/Z4N/HIC4="; + release."9.0.0+coq8.13".sha256 = "sha256-zvAqV3VAB7cN+nlMhjSXzxuDkdd387ju2VSb2EUthI0="; + release."8.17.0".sha256 = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw="; + release."8.16.0".sha256 = "sha256-DH3iWwatPlhhCVYVlgL2WLkvneSVzSXUiKo2e0+1zR4="; + release."8.15.0".sha256 = "093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns"; + release."8.14.0".sha256 = "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06"; + release."8.13.0".sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"; + release."8.12.0".sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8"; + release."8.11.0".sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"; + release."8.10.0".sha256 = "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5"; + release."8.9.0".sha256 = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01"; + release."8.8.0".sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg"; + release."8.7.0".sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl"; + release."8.6.0".rev = "v8.6.0"; + release."8.6.0".sha256 = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj"; + releaseRev = v: "${if lib.versions.isGe "9.0" v then "v" else "V"}${v}"; - mlPlugin = true; + mlPlugin = true; - propagatedBuildInputs = [ stdlib ]; + propagatedBuildInputs = [ stdlib ]; - meta = { - license = lib.licenses.lgpl2; + meta = { + license = lib.licenses.lgpl2; + }; }; -}).overrideAttrs - ( - o: - # this is just a wrapper for rocPackages.bignums for Rocq >= 9.0 - lib.optionalAttrs - (coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version)) - ( - let - case = case: out: { inherit case out; }; - rp = lib.switch coq.coq-version [ - (case (lib.versions.isEq "9.0") rocqPackages_9_0) - (case (lib.versions.isEq "9.1") rocqPackages_9_1) - ] rocqPackages; - in - { - configurePhase = '' - echo no configuration - ''; - buildPhase = '' - echo building nothing - ''; - installPhase = '' - echo installing nothing - ''; - propagatedBuildInputs = o.propagatedBuildInputs ++ [ rp.bignums ]; - } - ) - ) +in +# this is just a wrapper for rocqPackages.bignums for Rocq >= 9.0 +if coq.rocqPackages ? bignums then + coq.rocqPackages.bignums.override { + inherit version stdlib; + inherit (coq.rocqPackages) rocq-core; + } +else + derivation diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index 0dc2c1726ab5..a3fea8bacdcf 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -3,9 +3,6 @@ mkCoqDerivation, which, coq, - rocqPackages_9_0, - rocqPackages_9_1, - rocqPackages, stdlib, version ? null, elpi-version ? null, @@ -23,7 +20,7 @@ let in with lib.versions; lib.switch coq.coq-version [ - (case (range "8.20" "9.1") "2.0.7") + (case (range "8.20" "8.20") "2.0.7") (case (range "8.18" "8.19") "1.18.1") (case (range "8.16" "8.17") "1.17.0") (case "8.15" "1.15.0") @@ -47,8 +44,8 @@ let in with lib.versions; lib.switch coq.coq-version [ - (case (range "8.20" "9.1") "2.6.0") - (case (range "8.20" "9.0") "2.5.2") + (case (range "8.20" "8.20") "2.6.0") + (case (range "8.20" "8.20") "2.5.2") (case "8.19" "2.0.1") (case "8.18" "2.0.0") (case "8.17" "1.18.0") @@ -141,42 +138,27 @@ let ); patched-derivation4 = patched-derivation3.overrideAttrs ( o: - # this is just a wrapper for rocPackages.rocq-elpi for Rocq >= 9.0 - if coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version) then - let - case = case: out: { inherit case out; }; - rp = lib.switch coq.coq-version [ - (case "9.0" rocqPackages_9_0) - (case "9.1" rocqPackages_9_1) - ] rocqPackages; - in + lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.5.0" o.version)) { configurePhase = '' - echo no configuration + make dune-files || true ''; buildPhase = '' - echo building nothing + dune build -p rocq-elpi @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} ''; installPhase = '' - echo installing nothing + dune install --root . rocq-elpi --prefix=$out --libdir $OCAMLFIND_DESTDIR + mkdir $out/lib/coq/ + mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version} ''; - propagatedBuildInputs = o.propagatedBuildInputs ++ [ rp.rocq-elpi ]; } - else - lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.5.0" o.version)) - { - configurePhase = '' - make dune-files || true - ''; - buildPhase = '' - dune build -p rocq-elpi @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} - ''; - installPhase = '' - dune install --root . rocq-elpi --prefix=$out --libdir $OCAMLFIND_DESTDIR - mkdir $out/lib/coq/ - mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version} - ''; - } ); in -patched-derivation4 +# this is just a wrapper for rocqPackages.stdlib for Rocq >= 9.0 +if coq.rocqPackages ? rocq-elpi then + coq.rocqPackages.rocq-elpi.override { + inherit version elpi-version; + inherit (coq.rocqPackages) rocq-core; + } +else + patched-derivation4 diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix index cde093329011..9d04f5878ec4 100644 --- a/pkgs/development/coq-modules/hierarchy-builder/default.nix +++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix @@ -2,9 +2,6 @@ lib, mkCoqDerivation, coq, - rocqPackages_9_0, - rocqPackages_9_1, - rocqPackages, stdlib, coq-elpi, version ? null, @@ -21,7 +18,7 @@ let in with lib.versions; lib.switch coq.coq-version [ - (case (range "8.20" "9.1") "1.9.1") + (case (range "8.20" "8.20") "1.9.1") (case (range "8.19" "8.20") "1.8.0") (case (range "8.18" "8.20") "1.7.1") (case (range "8.16" "8.18") "1.6.0") @@ -60,44 +57,28 @@ let license = licenses.mit; }; }; + hb2 = hb.overrideAttrs ( + o: + lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") { + buildPhase = "make build"; + } + // ( + if lib.versions.isGe "1.1.0" o.version || o.version == "dev" then + { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; } + else + { installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; } + ) + // lib.optionalAttrs (o.version != null && o.version == "1.8.1") { + propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ]; + } + ); in -hb.overrideAttrs ( - o: - lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") { - buildPhase = "make build"; +# this is just a wrapper for rocqPackages.hierarchy-builder for Rocq >= 9.0 +if coq.rocqPackages ? hierarchy-builder then + coq.rocqPackages.hierarchy-builder.override { + inherit version; + inherit (coq.rocqPackages) rocq-core; + rocq-elpi = coq-elpi; } - // ( - if lib.versions.isGe "1.1.0" o.version || o.version == "dev" then - { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; } - else - { installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; } - ) - // lib.optionalAttrs (o.version != null && o.version == "1.8.1") { - propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ]; - } - # this is just a wrapper for rocqPackages.hierarchy-builder for Rocq >= 9.0 - // - lib.optionalAttrs - (coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version)) - ( - let - case = case: out: { inherit case out; }; - rp = lib.switch coq.coq-version [ - (case "9.0" rocqPackages_9_0) - (case "9.1" rocqPackages_9_1) - ] rocqPackages; - in - { - configurePhase = '' - echo no configuration - ''; - buildPhase = '' - echo building nothing - ''; - installPhase = '' - echo installing nothing - ''; - propagatedBuildInputs = o.propagatedBuildInputs ++ [ rp.hierarchy-builder ]; - } - ) -) +else + hb2 diff --git a/pkgs/development/coq-modules/parseque/default.nix b/pkgs/development/coq-modules/parseque/default.nix index 7d2fd5b2832e..f890c4e17139 100644 --- a/pkgs/development/coq-modules/parseque/default.nix +++ b/pkgs/development/coq-modules/parseque/default.nix @@ -1,67 +1,43 @@ { lib, mkCoqDerivation, - rocqPackages_9_0, - rocqPackages_9_1, - rocqPackages, - which, coq, version ? null, }: with lib; -(mkCoqDerivation { - pname = "parseque"; - repo = "parseque"; - owner = "rocq-community"; +let + derivation = mkCoqDerivation { + pname = "parseque"; + repo = "parseque"; + owner = "rocq-community"; - inherit version; - defaultVersion = - with versions; - switch - [ coq.coq-version ] - [ - { - cases = [ (range "8.16" "9.0") ]; - out = "0.2.2"; - } - ] - null; + inherit version; + defaultVersion = + let + case = case: out: { inherit case out; }; + in + with versions; + switch coq.coq-version [ + (case (range "8.16" "8.20") "0.2.2") + ] null; - release."0.2.2".sha256 = "sha256-O50Rs7Yf1H4wgwb7ltRxW+7IF0b04zpfs+mR83rxT+E="; + release."0.2.2".sha256 = "sha256-O50Rs7Yf1H4wgwb7ltRxW+7IF0b04zpfs+mR83rxT+E="; - releaseRev = v: "v${v}"; + releaseRev = v: "v${v}"; - meta = { - description = "Total parser combinators in Coq/Rocq"; - maintainers = with maintainers; [ womeier ]; - license = licenses.mit; + meta = { + description = "Total parser combinators in Coq/Rocq"; + maintainers = with maintainers; [ womeier ]; + license = licenses.mit; + }; }; -}).overrideAttrs - ( - o: - # this is just a wrapper for rocPackages.parseque for Rocq >= 9.0 - lib.optionalAttrs - (coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version)) - ( - let - case = case: out: { inherit case out; }; - rp = lib.switch coq.coq-version [ - (case "9.0" rocqPackages_9_0) - (case "9.1" rocqPackages_9_1) - ] rocqPackages; - in - { - configurePhase = '' - echo no configuration - ''; - buildPhase = '' - echo building nothing - ''; - installPhase = '' - echo installing nothing - ''; - propagatedBuildInputs = [ rp.parseque ]; - } - ) - ) +in +# this is just a wrapper for rocqPackages.parseque for Rocq >= 9.0 +if coq.rocqPackages ? parseque then + coq.rocqPackages.parseque.override { + inherit version; + inherit (coq.rocqPackages) rocq-core; + } +else + derivation diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix index 5ce07d4757bf..ebbe95b7fa64 100644 --- a/pkgs/development/coq-modules/stdlib/default.nix +++ b/pkgs/development/coq-modules/stdlib/default.nix @@ -1,67 +1,54 @@ { coq, - rocqPackages_9_0, - rocqPackages_9_1, - rocqPackages, mkCoqDerivation, lib, version ? null, -}@args: -(mkCoqDerivation { +}: - pname = "stdlib"; - repo = "stdlib"; - owner = "coq"; - opam-name = "coq-stdlib"; +let + derivation = mkCoqDerivation { - inherit version; - defaultVersion = - let - case = case: out: { inherit case out; }; - in - with lib.versions; - lib.switch coq.coq-version [ - (case (isLe "9.1") "9.0.0") - # the < 9.0 above is artificial as stdlib was included in Coq before - ] null; - releaseRev = v: "V${v}"; + pname = "stdlib"; + repo = "stdlib"; + owner = "coq"; + opam-name = "coq-stdlib"; - release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ="; - - configurePhase = '' - echo no configuration - ''; - buildPhase = '' - echo building nothing - ''; - installPhase = '' - echo installing nothing - ''; - - meta = { - description = "Compatibility metapackage for Coq Stdlib library after the Rocq renaming"; - license = lib.licenses.lgpl21Only; - }; - -}).overrideAttrs - ( - o: - # stdlib is already included in Coq <= 8.20 - if coq.version != null && coq.version != "dev" && lib.versions.isLt "8.21" coq.version then - { - installPhase = '' - touch $out - ''; - } - else + inherit version; + defaultVersion = let case = case: out: { inherit case out; }; - rp = lib.switch coq.coq-version [ - (case "9.0" rocqPackages_9_0) - (case "9.1" rocqPackages_9_1) - ] rocqPackages; in - { - propagatedBuildInputs = [ rp.stdlib ]; - } - ) + with lib.versions; + lib.switch coq.coq-version [ + (case (isLe "9.1") "9.0.0") + # the < 9.0 above is artificial as stdlib was included in Coq before + ] null; + releaseRev = v: "V${v}"; + + release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ="; + + configurePhase = '' + echo no configuration + ''; + buildPhase = '' + echo building nothing + ''; + installPhase = '' + echo installing nothing + touch $out + ''; + + meta = { + description = "Compatibility metapackage for Coq Stdlib library after the Rocq renaming"; + license = lib.licenses.lgpl21Only; + }; + }; +in +# this is just a wrapper for rocqPackages.stdlib for Rocq >= 9.0 +if coq.rocqPackages ? stdlib then + coq.rocqPackages.stdlib.override { + inherit version; + inherit (coq.rocqPackages) rocq-core; + } +else + derivation diff --git a/pkgs/development/rocq-modules/parseque/default.nix b/pkgs/development/rocq-modules/parseque/default.nix index 415ba2bc4d06..a61c00cb485b 100644 --- a/pkgs/development/rocq-modules/parseque/default.nix +++ b/pkgs/development/rocq-modules/parseque/default.nix @@ -1,7 +1,6 @@ { lib, mkRocqDerivation, - which, stdlib, rocq-core, version ? null, diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 17d3cb80f782..a523101ce1ec 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -15462,6 +15462,21 @@ with pkgs; ocamlPackages = ocaml-ng.ocamlPackages_4_12; }; + inherit + (callPackage ./rocq-packages.nix { + inherit (ocaml-ng) + ocamlPackages_4_14 + ; + }) + mkRocqPackages + rocqPackages_9_0 + rocq-core_9_0 + rocqPackages_9_1 + rocq-core_9_1 + rocqPackages + rocq-core + ; + inherit (callPackage ./coq-packages.nix { inherit (ocaml-ng) @@ -15471,6 +15486,11 @@ with pkgs; ocamlPackages_4_12 ocamlPackages_4_14 ; + inherit + rocqPackages_9_0 + rocqPackages_9_1 + rocqPackages + ; }) mkCoqPackages coqPackages_8_5 @@ -15513,21 +15533,6 @@ with pkgs; coq ; - inherit - (callPackage ./rocq-packages.nix { - inherit (ocaml-ng) - ocamlPackages_4_14 - ; - }) - mkRocqPackages - rocqPackages_9_0 - rocq-core_9_0 - rocqPackages_9_1 - rocq-core_9_1 - rocqPackages - rocq-core - ; - coq-kernel = callPackage ../applications/editors/jupyter-kernels/coq { }; cubicle = callPackage ../applications/science/logic/cubicle { diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 4e0c6d690077..1b75cdff5477 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -11,6 +11,9 @@ ocamlPackages_4_10, ocamlPackages_4_12, ocamlPackages_4_14, + rocqPackages_9_0, + rocqPackages_9_1, + rocqPackages, fetchpatch, makeWrapper, coq2html, @@ -265,7 +268,7 @@ let ) (lib.attrNames set) ); mkCoq = - version: + version: rp: callPackage ../applications/science/logic/coq { inherit version @@ -275,6 +278,7 @@ let ocamlPackages_4_12 ocamlPackages_4_14 ; + rocqPackages = rp; }; in rec { @@ -295,24 +299,24 @@ rec { in self.filterPackages (!coq.dontFilter or false); - coq_8_5 = mkCoq "8.5"; - coq_8_6 = mkCoq "8.6"; - coq_8_7 = mkCoq "8.7"; - coq_8_8 = mkCoq "8.8"; - coq_8_9 = mkCoq "8.9"; - coq_8_10 = mkCoq "8.10"; - coq_8_11 = mkCoq "8.11"; - coq_8_12 = mkCoq "8.12"; - coq_8_13 = mkCoq "8.13"; - coq_8_14 = mkCoq "8.14"; - coq_8_15 = mkCoq "8.15"; - coq_8_16 = mkCoq "8.16"; - coq_8_17 = mkCoq "8.17"; - coq_8_18 = mkCoq "8.18"; - coq_8_19 = mkCoq "8.19"; - coq_8_20 = mkCoq "8.20"; - coq_9_0 = mkCoq "9.0"; - coq_9_1 = mkCoq "9.1"; + coq_8_5 = mkCoq "8.5" { }; + coq_8_6 = mkCoq "8.6" { }; + coq_8_7 = mkCoq "8.7" { }; + coq_8_8 = mkCoq "8.8" { }; + coq_8_9 = mkCoq "8.9" { }; + coq_8_10 = mkCoq "8.10" { }; + coq_8_11 = mkCoq "8.11" { }; + coq_8_12 = mkCoq "8.12" { }; + coq_8_13 = mkCoq "8.13" { }; + coq_8_14 = mkCoq "8.14" { }; + coq_8_15 = mkCoq "8.15" { }; + coq_8_16 = mkCoq "8.16" { }; + coq_8_17 = mkCoq "8.17" { }; + coq_8_18 = mkCoq "8.18" { }; + coq_8_19 = mkCoq "8.19" { }; + coq_8_20 = mkCoq "8.20" { }; + coq_9_0 = mkCoq "9.0" rocqPackages_9_0; + coq_9_1 = mkCoq "9.1" rocqPackages_9_1; coqPackages_8_5 = mkCoqPackages coq_8_5; coqPackages_8_6 = mkCoqPackages coq_8_6;