Split out CoqIDE by default when Coq >= 8.14.

pkgs/applications/science/logic/coq/default.nix

@@ -8,10 +8,10 @@
 { lib, stdenv, fetchzip, writeText, pkg-config, gnumake42
 , customOCamlPackages ? null
 , ocamlPackages_4_05, ocamlPackages_4_09, ocamlPackages_4_10, ocamlPackages_4_12, ncurses
-, buildIde ? true
+, buildIde ? null # default is true for Coq < 8.14 and false for Coq >= 8.14
 , glib, gnome, wrapGAppsHook, makeDesktopItem, copyDesktopItems
 , csdp ? null
-, version, coq-version ? null,
+, version, coq-version ? null
 }@args:
 let lib' = lib; in
 let lib = import ../../../../build-support/coq/extra-lib.nix {lib = lib';}; in
@@ -59,6 +59,7 @@ let
   version = fetched.version;
   coq-version = args.coq-version or (if version != "dev" then versions.majorMinor version else "dev");
   coqAtLeast = v: coq-version == "dev" || versionAtLeast coq-version v;
+  buildIde = args.buildIde or (!coqAtLeast "8.14");
   ideFlags = optionalString (buildIde && !coqAtLeast "8.10")
     "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt";
   csdpPatch = if csdp != null then ''

pkgs/development/coq-modules/coqide/default.nix

@@ -0,0 +1,61 @@
+{ lib
+, makeDesktopItem
+, copyDesktopItems
+, wrapGAppsHook
+, glib
+, gnome
+, mkCoqDerivation
+, coq
+, version ? null }:
+
+with lib; mkCoqDerivation rec {
+  pname = "coqide";
+  inherit version;
+
+  inherit (coq) src;
+  release."${coq.version}" = {};
+
+  defaultVersion = if versions.isGe "8.14" coq.version then coq.version else null;
+
+  preConfigure = ''
+    patchShebangs dev/tools/
+  '';
+  prefixKey = "-prefix ";
+
+  useDune2 = true;
+
+  buildInputs = [
+    copyDesktopItems
+    wrapGAppsHook
+    coq.ocamlPackages.lablgtk3-sourceview3
+    glib
+    gnome.adwaita-icon-theme
+  ];
+
+  buildPhase = ''
+    runHook preBuild
+    dune build -p ${pname} -j $NIX_BUILD_CORES
+    runHook postBuild
+  '';
+  installPhase = ''
+    runHook preInstall
+    dune install --prefix $out ${pname}
+    runHook postInstall
+  '';
+
+  desktopItems = makeDesktopItem {
+    name = "coqide";
+    exec = "coqide";
+    icon = "coq";
+    desktopName = "CoqIDE";
+    comment = "Graphical interface for the Coq proof assistant";
+    categories = [ "Development" "Science" "Math" "IDE" "GTK" ];
+  };
+
+  meta = with lib; {
+    homepage = "https://coq.inria.fr";
+    description = "The CoqIDE user interface for the Coq proof assistant";
+    license = licenses.lgpl21Plus;
+    maintainers = [ maintainers.Zimmi48 ];
+  };
+}

pkgs/top-level/coq-packages.nix

@@ -36,6 +36,7 @@ let
       coq-record-update = callPackage ../development/coq-modules/coq-record-update { };
       coqeal = callPackage ../development/coq-modules/coqeal {};
       coqhammer = callPackage ../development/coq-modules/coqhammer {};
+      coqide = callPackage ../development/coq-modules/coqide {};
       coqprime = callPackage ../development/coq-modules/coqprime {};
       coqtail-math = callPackage ../development/coq-modules/coqtail-math {};
       coquelicot = callPackage ../development/coq-modules/coquelicot {};