diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index cee47f70a062..aedee50cefef 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -79,7 +79,7 @@ let }; releaseRev = v: "V${v}"; fetched = - import ../../../../build-support/coq/meta-fetch/default.nix + import ../../../../build-support/rocq/meta-fetch/default.nix { inherit lib diff --git a/pkgs/applications/science/logic/rocq-core/default.nix b/pkgs/applications/science/logic/rocq-core/default.nix index 6f1c384d005f..a6501daaaa3f 100644 --- a/pkgs/applications/science/logic/rocq-core/default.nix +++ b/pkgs/applications/science/logic/rocq-core/default.nix @@ -32,7 +32,7 @@ let }; releaseRev = v: "V${v}"; fetched = - import ../../../../build-support/coq/meta-fetch/default.nix + import ../../../../build-support/rocq/meta-fetch/default.nix { inherit lib diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix deleted file mode 100644 index 3c9670f4f65e..000000000000 --- a/pkgs/build-support/coq/default.nix +++ /dev/null @@ -1,246 +0,0 @@ -{ - lib, - stdenv, - coqPackages, - coq, - which, - fetchzip, - fetchurl, - dune, -}@args: - -let - lib = import ./extra-lib.nix { - inherit (args) lib; - }; - - inherit (lib) - concatStringsSep - flip - foldl - isFunction - isString - optional - optionalAttrs - optionals - optionalString - pred - remove - switch - versions - ; - - inherit (lib.attrsets) removeAttrs; - inherit (lib.strings) match; - - isGitHubDomain = d: match "^github.*" d != null; - isGitLabDomain = d: match "^gitlab.*" d != null; -in - -{ - pname, - version ? null, - fetcher ? null, - owner ? "rocq-community", - domain ? "github.com", - repo ? pname, - defaultVersion ? null, - releaseRev ? (v: v), - displayVersion ? { }, - release ? { }, - buildInputs ? [ ], - nativeBuildInputs ? [ ], - extraBuildInputs ? [ ], - extraNativeBuildInputs ? [ ], - overrideBuildInputs ? [ ], - overrideNativeBuildInputs ? [ ], - namePrefix ? [ "coq" ], - enableParallelBuilding ? true, - extraInstallFlags ? [ ], - setCOQBIN ? true, - mlPlugin ? false, - useMelquiondRemake ? null, - dropAttrs ? [ ], - keepAttrs ? [ ], - dropDerivationAttrs ? [ ], - useDuneifVersion ? (x: false), - useDune ? false, - opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])), - ... -}@args: -let - args-to-remove = foldl (flip remove) ( - [ - "version" - "fetcher" - "repo" - "owner" - "domain" - "releaseRev" - "displayVersion" - "defaultVersion" - "useMelquiondRemake" - "release" - "buildInputs" - "nativeBuildInputs" - "extraBuildInputs" - "extraNativeBuildInputs" - "overrideBuildInputs" - "overrideNativeBuildInputs" - "namePrefix" - "meta" - "useDuneifVersion" - "useDune" - "opam-name" - "extraInstallFlags" - "setCOQBIN" - "mlPlugin" - "dropAttrs" - "dropDerivationAttrs" - "keepAttrs" - "env" - ] - ++ dropAttrs - ) keepAttrs; - fetch = - import ../coq/meta-fetch/default.nix - { - inherit - lib - stdenv - fetchzip - fetchurl - ; - } - ( - { - inherit release releaseRev; - location = { inherit domain owner repo; }; - } - // optionalAttrs (args ? fetcher) { inherit fetcher; } - ); - fetched = fetch (if version != null then version else defaultVersion); - display-pkg = - n: sep: v: - let - d = displayVersion.${n} or (if sep == "" then ".." else true); - in - n - + optionalString (v != "" && v != null) ( - switch d [ - { - case = true; - out = sep + v; - } - { - case = "."; - out = sep + versions.major v; - } - { - case = ".."; - out = sep + versions.majorMinor v; - } - { - case = "..."; - out = sep + versions.majorMinorPatch v; - } - { - case = isFunction; - out = optionalString (d v != "") (sep + d v); - } - { - case = isString; - out = optionalString (d != "") (sep + d); - } - ] "" - ) - + optionalString (v == null) "-broken"; - append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-"; - prefix-name = foldl append-version "" namePrefix; - useDune = args.useDune or (useDuneifVersion fetched.version); - coqlib-flags = [ - "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib" - "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" - ]; - docdir-flags = [ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ]; - COQUSERCONTRIB = "$out/lib/coq/${coq.coq-version}/user-contrib"; -in -stdenv.mkDerivation ( - removeAttrs ( - { - - name = prefix-name + (display-pkg pname "-" fetched.version); - - inherit (fetched) version src; - - nativeBuildInputs = - args.overrideNativeBuildInputs or ( - [ which ] - ++ optional useDune dune - ++ optionals (useDune || mlPlugin) [ - coq.ocamlPackages.ocaml - coq.ocamlPackages.findlib - ] - ++ (args.nativeBuildInputs or [ ]) - ++ extraNativeBuildInputs - ); - buildInputs = - args.overrideBuildInputs or ([ coq ] ++ (args.buildInputs or [ ]) ++ extraBuildInputs); - inherit enableParallelBuilding; - - env = - optionalAttrs setCOQBIN { - COQBIN = "${coq}/bin/"; - } - // optionalAttrs (args ? useMelquiondRemake) { - inherit COQUSERCONTRIB; - } - // (args.env or { }); - - meta = - ( - { - platforms = coq.meta.platforms; - } - // (switch domain [ - { - case = pred.union isGitHubDomain isGitLabDomain; - out = { - homepage = "https://${domain}/${owner}/${repo}"; - }; - } - ] { }) - // optionalAttrs (fetched.broken or false) { - coqFilter = true; - broken = true; - } - ) - // (args.meta or { }); - - } - // (optionalAttrs (!args ? installPhase && !args ? useMelquiondRemake) { - installFlags = coqlib-flags ++ docdir-flags ++ extraInstallFlags; - }) - // (optionalAttrs useDune { - buildPhase = '' - runHook preBuild - dune build -p ${opam-name} ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} - runHook postBuild - ''; - installPhase = '' - runHook preInstall - dune install --prefix=$out --libdir $OCAMLFIND_DESTDIR ${opam-name} - mkdir $out/lib/coq/ - mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version} - runHook postInstall - ''; - }) - // (optionalAttrs (args ? useMelquiondRemake) { - preConfigurePhases = [ "autoconf" ]; - configureFlags = [ "--libdir=${COQUSERCONTRIB}/${useMelquiondRemake.logpath or ""}" ]; - buildPhase = "./remake -j$NIX_BUILD_CORES"; - installPhase = "./remake install"; - }) - // (removeAttrs args args-to-remove) - ) dropDerivationAttrs -) diff --git a/pkgs/build-support/rocq/default.nix b/pkgs/build-support/rocq/default.nix index 7a7c5fba7b25..68181efcfb44 100644 --- a/pkgs/build-support/rocq/default.nix +++ b/pkgs/build-support/rocq/default.nix @@ -3,15 +3,16 @@ stdenv, rocqPackages, rocq-core, + coq, which, fetchzip, fetchurl, dune, -}@args: +}@args0: let lib = import ./extra-lib.nix { - inherit (args) lib; + inherit (args0) lib; }; inherit (lib) @@ -66,6 +67,8 @@ in useDuneifVersion ? (x: false), useDune ? false, opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])), + useCoq ? false, + useCoqifVersion ? (x: false), ... }@args: let @@ -99,11 +102,13 @@ let "dropDerivationAttrs" "keepAttrs" "env" + "useCoq" + "useCoqifVersion" ] ++ dropAttrs ) keepAttrs; fetch = - import ../coq/meta-fetch/default.nix + import ../rocq/meta-fetch/default.nix { inherit lib @@ -158,6 +163,8 @@ let append-version = p: n: p + display-pkg n "" rocqPackages.${n}.version + "-"; prefix-name = foldl append-version "" namePrefix; useDune = args.useDune or (useDuneifVersion fetched.version); + useCoq = args.useCoq or (useCoqifVersion fetched.version); + rocq-core = if useCoq then coq // { rocq-version = coq.coq-version; } else args0.rocq-core; rocqlib-flags = [ "COQLIBINSTALL=$(out)/lib/coq/${rocq-core.rocq-version}/user-contrib" "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" @@ -190,9 +197,10 @@ stdenv.mkDerivation ( inherit enableParallelBuilding; env = - optionalAttrs setROCQBIN { + optionalAttrs (setROCQBIN && !useCoq) { ROCQBIN = "${rocq-core}/bin/"; } + // optionalAttrs (setROCQBIN && useCoq) { COQBIN = "${rocq-core}/bin/"; } // optionalAttrs (args ? useMelquiondRemake) { inherit COQUSERCONTRIB; } diff --git a/pkgs/build-support/coq/meta-fetch/default.nix b/pkgs/build-support/rocq/meta-fetch/default.nix similarity index 100% rename from pkgs/build-support/coq/meta-fetch/default.nix rename to pkgs/build-support/rocq/meta-fetch/default.nix diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index 76bf3682c5bc..bd751ed9d7fd 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -1,6 +1,6 @@ { lib, - mkCoqDerivation, + mkRocqDerivation, which, dune, coq, @@ -34,7 +34,9 @@ let propagatedBuildInputs_wo_elpi = [ coq.ocamlPackages.findlib ]; - derivation = mkCoqDerivation.override { dune = dune.override { version = "3.21.1"; }; } { + derivation = mkRocqDerivation.override { dune = dune.override { version = "3.21.1"; }; } { + useCoq = true; + namePrefix = [ "coq" ]; pname = "elpi"; repo = "coq-elpi"; owner = "LPCIC"; diff --git a/pkgs/development/coq-modules/stalmarck/default.nix b/pkgs/development/coq-modules/stalmarck/default.nix index 5bcdffbfa9c8..50eea900a422 100644 --- a/pkgs/development/coq-modules/stalmarck/default.nix +++ b/pkgs/development/coq-modules/stalmarck/default.nix @@ -1,6 +1,6 @@ { lib, - mkCoqDerivation, + mkRocqDerivation, dune, coq, stdlib, @@ -39,7 +39,9 @@ let else "A two-level approach to prove tautologies using Stålmarck's algorithm in Coq."; in - mkCoqDerivation.override { dune = dune.override { version = "3.21.1"; }; } { + mkRocqDerivation.override { dune = dune.override { version = "3.21.1"; }; } { + useCoq = true; + namePrefix = [ "coq" ]; inherit version pname diff --git a/pkgs/development/coq-modules/vscoq-language-server/default.nix b/pkgs/development/coq-modules/vscoq-language-server/default.nix index b20d6961eb7a..af1106de9f03 100644 --- a/pkgs/development/coq-modules/vscoq-language-server/default.nix +++ b/pkgs/development/coq-modules/vscoq-language-server/default.nix @@ -82,7 +82,7 @@ ocamlPackages.buildDunePackage { license = lib.licenses.mit; } // lib.optionalAttrs (fetched.broken or false) { - coqFilter = true; + rocqFilter = true; broken = true; }; } diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index a93fb26666c9..ebe42498e38a 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -27,14 +27,14 @@ let self: coq: let callPackage = self.callPackage; - coqPackages = self // { + rocqPackages = self // { recurseForDerivations = false; }; in { - inherit coqPackages lib; + inherit rocqPackages lib; - metaFetch = import ../build-support/coq/meta-fetch/default.nix { + metaFetch = import ../build-support/rocq/meta-fetch/default.nix { inherit lib stdenv @@ -42,7 +42,16 @@ let fetchurl ; }; - mkCoqDerivation = lib.makeOverridable (callPackage ../build-support/coq { }); + mkRocqDerivation = lib.makeOverridable (callPackage ../build-support/rocq { }); + mkCoqDerivation = + args: + self.mkRocqDerivation ( + { + useCoq = true; + namePrefix = [ "coq" ]; + } + // args + ); coq = coq.overrideAttrs (oldAttrs: { passthru = (oldAttrs.passthru or { }) // { @@ -286,7 +295,7 @@ let let v = set.${name} or null; in - lib.optional (!v.meta.coqFilter or false) ( + lib.optional (!v.meta.rocqFilter or false) ( lib.nameValuePair name ( if lib.isAttrs v && v.recurseForDerivations or false then filterCoqPackages v else v ) diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix index 28b980f6dbfc..7b48e4d73079 100644 --- a/pkgs/top-level/rocq-packages.nix +++ b/pkgs/top-level/rocq-packages.nix @@ -26,7 +26,7 @@ let recurseForDerivations = false; }; - metaFetch = import ../build-support/coq/meta-fetch/default.nix { + metaFetch = import ../build-support/rocq/meta-fetch/default.nix { inherit lib stdenv