From 944029c25a80505aaa5f19928e4911360d8505de Mon Sep 17 00:00:00 2001
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(+)
Toggle diff (92 lines)
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
