about summary refs log tree commit diff
path: root/nixpkgs/pkgs/applications/science/logic/coq/default.nix
diff options
context:
space:
mode:
Diffstat (limited to 'nixpkgs/pkgs/applications/science/logic/coq/default.nix')
-rw-r--r--nixpkgs/pkgs/applications/science/logic/coq/default.nix20
1 files changed, 17 insertions, 3 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/coq/default.nix b/nixpkgs/pkgs/applications/science/logic/coq/default.nix
index cd19b9a94424..e595bf47c67c 100644
--- a/nixpkgs/pkgs/applications/science/logic/coq/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/coq/default.nix
@@ -9,7 +9,7 @@
 , customOCamlPackages ? null
 , ocamlPackages_4_05, ocamlPackages_4_09, ocamlPackages_4_10, ncurses
 , buildIde ? true
-, glib, gnome, wrapGAppsHook
+, glib, gnome, wrapGAppsHook, makeDesktopItem, copyDesktopItems
 , csdp ? null
 , version, coq-version ? null,
 }@args:
@@ -124,7 +124,9 @@ self = stdenv.mkDerivation {
     '';
   };
 
-  nativeBuildInputs = [ pkg-config ] ++ optional (!versionAtLeast "8.6") gnumake42;
+  nativeBuildInputs = [ pkg-config ]
+    ++ optional buildIde copyDesktopItems
+    ++ optional (!versionAtLeast "8.6") gnumake42;
   buildInputs = [ ncurses ] ++ ocamlBuildInputs
     ++ optionals buildIde
       (if versionAtLeast "8.10"
@@ -166,12 +168,24 @@ self = stdenv.mkDerivation {
 
   createFindlibDestdir = true;
 
+  desktopItems = optional buildIde (makeDesktopItem {
+    name = "coqide";
+    exec = "coqide";
+    icon = "coq";
+    desktopName = "CoqIDE";
+    comment = "Graphical interface for the Coq proof assistant";
+    categories = "Development;Science;Math;IDE;GTK";
+  });
+
   postInstall = ''
     cp bin/votour $out/bin/
     ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq
+  '' + optionalString buildIde ''
+    mkdir -p "$out/share/pixmaps"
+    ln -s "$out/share/coq/coq.png" "$out/share/pixmaps/"
   '';
 
-  meta = with lib; {
+  meta = {
     description = "Coq proof assistant";
     longDescription = ''
       Coq is a formal proof management system.  It provides a formal language