From patchwork Sat Dec 28 22:43:15 2019 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Brett Gilio X-Patchwork-Id: 19465 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 23B0217989; Sat, 28 Dec 2019 22:44:10 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id AFDB91795E for ; Sat, 28 Dec 2019 22:44:09 +0000 (GMT) Received: from localhost ([::1]:46852 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ilKob-00081q-7i for patchwork@mira.cbaines.net; Sat, 28 Dec 2019 17:44:09 -0500 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 X-Loop: help-debbugs@gnu.org Subject: [bug#38784] [WIP 1/1] gnu: Add emacs-company-coq. References: <87mubchy3m.fsf@gnu.org> In-Reply-To: <87mubchy3m.fsf@gnu.org> Resent-From: Brett Gilio Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 28 Dec 2019 22:44:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 38784 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: To: 38784@debbugs.gnu.org Received: via spool by 38784-submit@debbugs.gnu.org id=B38784.157757299618495 (code B ref 38784); Sat, 28 Dec 2019 22:44:01 +0000 Received: (at 38784) by debbugs.gnu.org; 28 Dec 2019 22:43:16 +0000 Received: from localhost ([127.0.0.1]:59062 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ilKnj-0004oF-Rf for submit@debbugs.gnu.org; Sat, 28 Dec 2019 17:43:16 -0500 Received: from eggs.gnu.org ([209.51.188.92]:37455) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ilKni-0004o2-2A for 38784@debbugs.gnu.org; Sat, 28 Dec 2019 17:43:14 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:39253) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ilKnc-0001zk-Pa for 38784@debbugs.gnu.org; Sat, 28 Dec 2019 17:43:08 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48410 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ilKna-0004Qm-V0 for 38784@debbugs.gnu.org; Sat, 28 Dec 2019 17:43:08 -0500 From: Brett Gilio Date: Sat, 28 Dec 2019 16:43:15 -0600 Message-ID: <87imm0hy0s.fsf@gnu.org> MIME-Version: 1.0 Content-Disposition: inline; filename=0001-gnu-Add-emacs-company-coq.patch Content-Description: [WIP 1/1] gnu: Add emacs-company-coq. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches 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