From 1383b84d37d3dbca82c4c07bd0afe5d6e2ebaf35 Mon Sep 17 00:00:00 2001
From: Tom McLaughlin <tom@codedown.io>
Date: Mon, 2 May 2022 00:15:13 -0700
Subject: [PATCH] coq_kernel: init at 1.6.0

---
 .../editors/jupyter-kernels/coq/default.nix   | 58 +++++++++++++++++++
 .../editors/jupyter-kernels/coq/kernel.nix    | 30 ++++++++++
 pkgs/top-level/all-packages.nix               |  2 +
 3 files changed, 90 insertions(+)
 create mode 100644 pkgs/applications/editors/jupyter-kernels/coq/default.nix
 create mode 100644 pkgs/applications/editors/jupyter-kernels/coq/kernel.nix

diff --git a/pkgs/applications/editors/jupyter-kernels/coq/default.nix b/pkgs/applications/editors/jupyter-kernels/coq/default.nix
new file mode 100644
index 000000000000..545c4e8ec4e8
--- /dev/null
+++ b/pkgs/applications/editors/jupyter-kernels/coq/default.nix
@@ -0,0 +1,58 @@
+{ lib
+, stdenv
+, callPackage
+, runCommand
+, makeWrapper
+, coq
+, imagemagick
+, python3
+}:
+
+# Jupyter console:
+# nix run --impure --expr 'with import <nixpkgs> {}; jupyter-console.withSingleKernel coq-kernel.definition'
+
+# Jupyter console with packages:
+# nix run --impure --expr 'with import <nixpkgs> {}; jupyter-console.withSingleKernel (coq-kernel.definitionWithPackages [coqPackages.bignums])'
+
+# Jupyter notebook:
+# nix run --impure --expr 'with import <nixpkgs> {}; jupyter.override { definitions.coq = coq-kernel.definition; }'
+
+let
+  python = python3.withPackages (ps: [ ps.traitlets ps.jupyter_core ps.ipykernel (callPackage ./kernel.nix {}) ]);
+
+  logos = runCommand "coq-logos" { buildInputs = [ imagemagick ]; } ''
+    mkdir -p $out
+    convert ${coq.src}/ide/coqide/coq.png -resize 32x32 $out/logo-32x32.png
+    convert ${coq.src}/ide/coqide/coq.png -resize 64x64 $out/logo-64x64.png
+  '';
+
+in
+
+rec {
+  launcher = runCommand "coq-kernel-launcher" {
+    nativeBuildInputs = [ makeWrapper ];
+  } ''
+    mkdir -p $out/bin
+
+    makeWrapper ${python.interpreter} $out/bin/coq-kernel \
+      --add-flags "-m coq_jupyter" \
+      --suffix PATH : ${coq}/bin
+  '';
+
+  definition = definitionWithPackages [];
+
+  definitionWithPackages = packages: {
+    displayName = "Coq " + coq.version;
+    argv = [
+      "${launcher}/bin/coq-kernel"
+      "-f"
+      "{connection_file}"
+    ];
+    language = "coq";
+    logo32 = "${logos}/logo-32x32.png";
+    logo64 = "${logos}/logo-64x64.png";
+    env = {
+      COQPATH = lib.concatStringsSep ":" (map (x: "${x}/lib/coq/${coq.coq-version}/user-contrib/") packages);
+    };
+  };
+}
diff --git a/pkgs/applications/editors/jupyter-kernels/coq/kernel.nix b/pkgs/applications/editors/jupyter-kernels/coq/kernel.nix
new file mode 100644
index 000000000000..78bf84716fef
--- /dev/null
+++ b/pkgs/applications/editors/jupyter-kernels/coq/kernel.nix
@@ -0,0 +1,30 @@
+{ lib
+, fetchFromGitHub
+, python3
+, coq
+}:
+
+python3.pkgs.buildPythonPackage rec {
+  pname = "coq-jupyter";
+  version = "1.6.0";
+
+  src = fetchFromGitHub {
+    owner = "EugeneLoy";
+    repo = "coq_jupyter";
+    rev = "v${version}";
+    sha256 = "sha256-+Pp51cxeqjg5MW4CEccNWVjNcY9iyFNATIEage9RWJ0=";
+  };
+
+  propagatedBuildInputs = (with python3.pkgs; [ ipykernel future ]) ++ [ coq ];
+
+  nativeBuildInputs = [ coq ];
+
+  doCheck = false;
+
+  meta = with lib; {
+    homepage = "https://github.com/EugeneLoy/coq_jupyter";
+    description = "Jupyter kernel for Coq";
+    license = licenses.asl20;
+    maintainers = with maintainers; [ thomasjm ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 23fa2b4b2440..514a2afdb640 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -39521,6 +39521,8 @@ with pkgs;
 
   coq2html = callPackage ../tools/typesetting/coq2html { };
 
+  coq-kernel = callPackage ../applications/editors/jupyter-kernels/coq { };
+
   cryptoverif = callPackage ../applications/science/logic/cryptoverif { };
 
   crypto-org-wallet = callPackage ../applications/blockchains/crypto-org-wallet { };