From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:48808) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ilKoV-00081g-2u for guix-patches@gnu.org; Sat, 28 Dec 2019 17:44:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1ilKoT-0006EK-Pq for guix-patches@gnu.org; Sat, 28 Dec 2019 17:44:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:53089) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1ilKoT-0006DP-LG for guix-patches@gnu.org; Sat, 28 Dec 2019 17:44:01 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1ilKoT-0004pW-Jw for guix-patches@gnu.org; Sat, 28 Dec 2019 17:44:01 -0500 Subject: [bug#38784] [WIP 1/1] gnu: Add emacs-company-coq. References: <87mubchy3m.fsf@gnu.org> In-Reply-To: <87mubchy3m.fsf@gnu.org> Resent-Message-ID: From: Brett Gilio Date: Sat, 28 Dec 2019 16:43:15 -0600 Message-ID: <87imm0hy0s.fsf@gnu.org> MIME-Version: 1.0 Content-Type: text/x-patch Content-Disposition: inline; filename=0001-gnu-Add-emacs-company-coq.patch Content-Description: [WIP 1/1] gnu: Add emacs-company-coq. List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: 38784@debbugs.gnu.org >From 944029c25a80505aaa5f19928e4911360d8505de Mon Sep 17 00:00:00 2001 From: Brett Gilio 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