[PATCH] gnu: Add emacs-company-coq.

DoneSubmitted by John Soo.
Details
2 participants
  • John Soo
  • Nicolas Goaziou
Owner
unassigned
Severity
normal
J
J
John Soo wrote on 29 Mar 03:04 +0200
(address . guix-patches@gnu.org)
87mu802cqb.fsf@asu.edu
Hi Guix,
Company-coq is indispensable when working in coq for me.
Thanks for your patience with all these patches as I try to only useguix for emacs package management.
- John
Toggle quote (1 lines)>From 94fd93cdb32460b27f7bb3611d474ddbe0b330b0 Mon Sep 17 00:00:00 2001
From: John Soo <jsoo1@asu.edu>Date: Tue, 24 Mar 2020 07:03:21 -0700Subject: [PATCH] gnu: Add emacs-company-coq.
* gnu/packages/emacs-xyz.scm (emacs-company-coq): New variable.--- gnu/packages/emacs-xyz.scm | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+)
Toggle diff (55 lines)diff --git a/gnu/packages/emacs-xyz.scm b/gnu/packages/emacs-xyz.scmindex 9d40b8019e..97c34a00a3 100644--- a/gnu/packages/emacs-xyz.scm+++ b/gnu/packages/emacs-xyz.scm@@ -65,6 +65,7 @@ ;;; Copyright © 2020 Michael Rohleder <mike@rohleder.de> ;;; Copyright © 2020 Brice Waegeneire <brice@waegenei.re> ;;; Copyright © 2020 6033fe7de85d <6033fe7de85d@airmail.cc>+;;; Copyright © 2020 John Soo <jsoo1@asu.edu> ;;; ;;; This file is part of GNU Guix. ;;;@@ -21776,3 +21777,40 @@ enables modal editing and composition of commands, too. It combines ideas of other Editors like Vim or Kakoune and tries to align them with regular Emacs conventions.") (license license:gpl3+)))++(define-public emacs-company-coq+ (package+ (name "emacs-company-coq")+ (version "1.0.1")+ (source+ (origin+ (method git-fetch)+ (uri+ (git-reference+ (url "https://github.com/cpitclaudel/company-coq")+ (commit version)))+ (file-name (git-file-name name version))+ (sha256+ (base32+ "0dxi4h8xqq5647k7h89s4pi8nwyj3brlhsckrv3p3b1g4dr6mk3b"))))+ (inputs+ `(("emacs-company" ,emacs-company)+ ("emacs-company-math" ,emacs-company-math)+ ("emacs-dash" ,emacs-dash)+ ("emacs-yasnippet" ,emacs-yasnippet)))+ (build-system emacs-build-system)+ (home-page "https://github.com/cpitclaudel/company-coq")+ (synopsis "IDE extensions for Proof General's Coq mode")+ (description "A collection of extensions for Proof General's Coq+mode. Including:++@itemize+@item Prettification of operators, types, and subscripts+@item Auto-completion+@item Insertion of cases+@item Fully explicit intros+@item Outlines, code folding, and jumping to definition+@item Help with errors+@item and more+@end itemize")+ (license license:gpl3+)))-- 2.26.0
N
N
Nicolas Goaziou wrote on 30 Mar 14:38 +0200
(name . John Soo)(address . jsoo1@asu.edu)(address . 40299-done@debbugs.gnu.org)
87sghq81bf.fsf@nicolasgoaziou.fr
Hello,
John Soo <jsoo1@asu.edu> writes:
Toggle quote (2 lines)> Company-coq is indispensable when working in coq for me.
I slightly expounded the description and applied your patch asf931d46ce3e342f53dee926d3cff70b081f58e5f.
Thank you!
Regards,
-- Nicolas Goaziou
Closed
?