diff --git a/doc/languages-frameworks/rocq.section.md b/doc/languages-frameworks/rocq.section.md index f2ba50312807..056394056797 100644 --- a/doc/languages-frameworks/rocq.section.md +++ b/doc/languages-frameworks/rocq.section.md @@ -74,6 +74,8 @@ The recommended way of defining a derivation for a Rocq library, is to use the ` * `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 `COQLIBINSTALL` and `COQPLUGININSTALL` so as to install in the proper subdirectory. Indeed Rocq libraries should be installed in `$(out)/lib/coq/${rocq-core.rocq-version}/user-contrib/`. Such directories are automatically added to the `$ROCQPATH` environment variable by the hook defined in the Rocq derivation. * `setROCQBIN` (optional, defaults to `true`), by default, the environment variable `$ROCQBIN` is set to the current Rocq's binary, but one can disable this behavior by setting it to `false`, +* `useCoq` (optional, defaults to `false`), adds the Coq compatibility binaries to the build environment, which is necessary for some packages that still depend on them and sets `COQBIN` to the path of the `coqc` binary (if `setROCQBIN` is also set to `true`). A wrapper `mkCoqDerivation` is provided that sets this option to `true`. +* `useCoqifVersion` (optional, defaults to `(x: false)`), adds the Coq compatibility binaries to the build environment if the provided predicate evaluates to true on the version. This can be useful for supporting old package versions that need the Coq compatibility binaries, while newer versions do not. * `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 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