coq: nix-buffer: Inherit variables to PG shell

1 files changed, 31 insertions, 0 deletions

diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 9faa9d8feb8..fd3655ce9e9 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -46,6 +46,37 @@ self = stdenv.mkDerivation {
       (mapc (lambda (arg)
         (when (file-directory-p (concat arg "/lib/coq/${coq-version}/user-contrib"))
           (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${stdenv.lib.concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)}))
+      ; TODO Abstract this pattern from here and nixBufferBuilders.withPackages!
+      (defvar nixpkgs--coq-buffer-count 0)
+      (when (eq nixpkgs--coq-buffer-count 0)
+        (make-variable-buffer-local 'nixpkgs--is-nixpkgs-coq-buffer)
+        (defun nixpkgs--coq-inherit (buf)
+          (inherit-local-inherit-child buf)
+          (with-current-buffer buf
+            (setq nixpkgs--coq-buffer-count (1+ nixpkgs--coq-buffer-count))
+            (add-hook 'kill-buffer-hook 'nixpkgs--decrement-coq-buffer-count nil t))
+          buf)
+        ; When generating a scomint buffer, do inherit-local inheritance and make it a nixpkgs-coq buffer
+        (defun nixpkgs--around-scomint-make (orig &rest r)
+          (if nixpkgs--is-nixpkgs-coq-buffer
+              (progn
+                (advice-add 'get-buffer-create :filter-return #'nixpkgs--coq-inherit)
+                (apply orig r)
+                (advice-remove 'get-buffer-create #'nixpkgs--coq-inherit))
+            (apply orig r)))
+        (advice-add 'scomint-make :around #'nixpkgs--around-scomint-make)
+        ; When we have no more coq buffers, tear down the buffer handling
+        (defun nixpkgs--decrement-coq-buffer-count ()
+          (setq nixpkgs--coq-buffer-count (1- nixpkgs--coq-buffer-count))
+          (when (eq nixpkgs--coq-buffer-count 0)
+            (advice-remove 'scomint-make #'nixpkgs--around-scomint-make)
+            (fmakunbound 'nixpkgs--around-scomint-make)
+            (fmakunbound 'nixpkgs--coq-inherit)
+            (fmakunbound 'nixpkgs--decrement-coq-buffer-count))))
+      (setq nixpkgs--coq-buffer-count (1+ nixpkgs--coq-buffer-count))
+      (add-hook 'kill-buffer-hook 'nixpkgs--decrement-coq-buffer-count nil t)
+      (setq nixpkgs--is-nixpkgs-coq-buffer t)
+      (inherit-local 'nixpkgs--is-nixpkgs-coq-buffer)
     '';
   };