[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 2020 03:04
(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 use
guix 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 -0700
Subject: [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.scm
index 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 2020 14:38
(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 as
f931d46ce3e342f53dee926d3cff70b081f58e5f.

Thank you!

Regards,

--
Nicolas Goaziou
Closed
?
Your comment

This issue is archived.

To comment on this conversation send email to 40299@debbugs.gnu.org