GNU bug report logs - #38784
[WIP 0/1] Add emacs-company-coq.

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 38784 in the body.
You can then email your comments to 38784 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: guix-patches <at> gnu.org
Subject: [WIP 0/1] Add emacs-company-coq.
Date: Sat, 28 Dec 2019 16:41:33 -0600

[0000-cover-letter.patch (text/x-patch, inline)]

From 944029c25a80505aaa5f19928e4911360d8505de Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Sat, 28 Dec 2019 16:39:14 -0600
Subject: [WIP 0/1] Add emacs-company-coq.
To: guix-patches <at> gnu.org

This is a WIP patch for adding emacs-company-coq. There is still more that
needs to be done before this package is ready to be pushed to master. Such
as getting the Coq-based test suite to run, ensuring that all of the cases
usually covered by CASK are being covered by Guix, and getting the REFMAN
to install properly.

Brett Gilio (1):
  gnu: Add emacs-company-coq.

 gnu/packages/emacs-xyz.scm | 75 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)

-- 
2.24.1

Message #8 received at 38784 <at> debbugs.gnu.org (full text, mbox):

From: Brett Gilio <brettg <at> gnu.org>
To: 38784 <at> debbugs.gnu.org
Subject: [WIP 1/1] gnu: Add emacs-company-coq.
Date: Sat, 28 Dec 2019 16:43:15 -0600

[0001-gnu-Add-emacs-company-coq.patch (text/x-patch, inline)]

From 944029c25a80505aaa5f19928e4911360d8505de Mon Sep 17 00:00:00 2001
From: Brett Gilio <brettg <at> gnu.org>
Date: Sat, 28 Dec 2019 16:38:24 -0600
Subject: [WIP 1/1] gnu: Add emacs-company-coq.
To: guix-patches <at> 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

Message #13 received at 38784-done <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Brett Gilio <brettg <at> gnu.org>
Cc: 38784-done <at> debbugs.gnu.org
Subject: Re: bug#38784: [WIP 0/1] Add emacs-company-coq.
Date: Tue, 12 Apr 2022 12:45:34 +0200

Hi,

Thanks for your submission.

On Sat, 28 Dec 2019 at 16:43, Brett Gilio <brettg <at> gnu.org> wrote:

> * gnu/packages/emacs-xyz.scm (emacs-company-coq): New variable.
> ---
>  gnu/packages/emacs-xyz.scm | 75 ++++++++++++++++++++++++++++++++++++++
>  1 file changed, 75 insertions(+)

[...]

> +(define-public emacs-company-coq
> +  (let ((commit "6e8bc2e367e8184079b7f4b4ab359b64ab884d7c")
> +	(revision "1")
> +	(version "1.0.1"))
> +    (package
> +      (name "emacs-company-coq")

[...]

> +      (license license:gpl3+))))

--8<---------------cut here---------------start------------->8---
f931d46ce3e342f53dee926d3cff70b081f58e5f
Author:     John Soo <jsoo1 <at> asu.edu>
AuthorDate: Mon Mar 30 14:36:38 2020 +0200
Commit:     Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
CommitDate: Mon Mar 30 14:37:41 2020 +0200

gnu: Add emacs-company-coq.

* gnu/packages/emacs-xyz.scm (emacs-company-coq): New variable.

1 file changed, 37 insertions(+)
gnu/packages/emacs-xyz.scm | 37 +++++++++++++++++++++++++++++++++++++
--8<---------------cut here---------------end--------------->8---

Therefore, closing!


Cheers,
simon

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.