From 944029c25a80505aaa5f19928e4911360d8505de Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg@gnu.org>
Date: Sat, 28 Dec 2019 16:38:24 -0600
Subject: [WIP 1/1] gnu: Add emacs-company-coq.
To: guix-patches@gnu.org

* gnu/packages/emacs-xyz.scm (emacs-company-coq): New variable.
---
 gnu/packages/emacs-xyz.scm | 75 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)

diff --git a/gnu/packages/emacs-xyz.scm b/gnu/packages/emacs-xyz.scm
index 06c8dc2016..b746e5a20a 100644
--- a/gnu/packages/emacs-xyz.scm
+++ b/gnu/packages/emacs-xyz.scm
@@ -92,6 +92,7 @@
   #:use-module (gnu packages bash)
   #:use-module (gnu packages cmake)
   #:use-module (gnu packages code)
+  #:use-module (gnu packages coq)
   #:use-module (gnu packages cpp)
   #:use-module (gnu packages curl)
   #:use-module (gnu packages databases)
@@ -20654,3 +20655,77 @@ buffer.  It can be used to toggle an alternative mode-line, toggle its visibilit
 or simply disable the mode-line in buffers where it is not very useful.")
     (home-page "https://github.com/hlissner/emacs-hide-mode-line")
     (license license:expat)))
+
+(define-public emacs-company-coq
+  (let ((commit "6e8bc2e367e8184079b7f4b4ab359b64ab884d7c")
+	(revision "1")
+	(version "1.0.1"))
+    (package
+      (name "emacs-company-coq")
+      (version (git-version version revision commit))
+      (source
+       (origin
+         (method git-fetch)
+         (uri (git-reference
+               (url "https://github.com/cpitclaudel/company-coq.git")
+               (commit commit)))
+         (sha256
+          (base32
+           "192vvz77yik0lx2g4yfjwx2himzzq4zhrc9mlyhdpwsmzwx7bf4r"))
+         (file-name (git-file-name name version))))
+      (build-system emacs-build-system)
+      (arguments
+       `(;; NOTE: By default this package leverages CASK. We do not need
+         ;; this. Instead, we will leverage Guix to handle installation
+         ;; for us.
+         ;; FIXME: REFMAN needs to be installed properly.
+         #:phases
+         (modify-phases %standard-phases
+           (add-after 'unpack 'move-el
+             (lambda _
+               (for-each (lambda (f)
+                           (rename-file f (basename f)))
+                         (find-files "./etc" ".*\\.el$"))
+               (for-each (lambda (f)
+                           (rename-file f (basename f)))
+                         (find-files "./experiments" ".*\\.el$"))
+               #t))
+           (add-after 'move-el 'patch-proof-general
+             (lambda* (#:key inputs #:allow-other-keys)
+               ;; Patch and load required components for proof-general.
+               (let* ((generic "/share/emacs/site-lisp/ProofGeneral/generic")
+                      (proof-site (string-append
+                                   (assoc-ref inputs "proof-general")
+                                   (string-append generic "/proof-site.el")))
+                      (proof-shell (string-append
+                                    (assoc-ref inputs "proof-general")
+                                    (string-append generic "/proof-shell.el"))))
+                 (substitute* "rebuild-screenshots.el"
+                   (("\\(require 'proof-site\\)")
+                    (string-append
+                     "(load-file \"" proof-site "\")")))
+                 (substitute* "company-coq.el"
+                   (("\\(require 'proof-site\\ nil t)")
+                    (string-append
+                     "(load-file \"" proof-site "\")")))
+                 (substitute* "company-coq-trace.el"
+                   (("\\(require 'proof-shell\\)")
+                    (string-append
+                     "(load-file \"" proof-shell "\")")))
+                 #t))))))
+      (propagated-inputs
+       `(("emacs-company-math" ,emacs-company-math)
+         ("emacs-company" ,emacs-company)
+         ("emacs-yasnippet" ,emacs-yasnippet)
+         ("emacs-dash" ,emacs-dash)
+         ("emacs-noflet" ,emacs-noflet)))
+      (native-inputs
+       `(("python" ,python)
+         ("proof-general" ,proof-general)))
+      (home-page "https://github.com/cpitclaudel/company-coq")
+      (synopsis
+       "Collection of extensions for Proof General's Coq mode")
+      (description
+       "This package includes a collection of company-mode backends for
+Proof-General's Coq mode, and many useful extensions to Proof-General.")
+      (license license:gpl3+))))
-- 
2.24.1