GNU bug report logs - #46016
broken Proof-General (emacs front-end to Coq)

Previous Next

Package: guix;

Reported by: zimoun <zimon.toutoune <at> gmail.com>

Date: Thu, 21 Jan 2021 11:14:01 UTC

Severity: normal

Done: zimoun <zimon.toutoune <at> gmail.com>

Bug is archived. No further changes may be made.

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

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

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to bug-guix <at> gnu.org:
bug#46016; Package guix. (Thu, 21 Jan 2021 11:14:01 GMT) Full text and rfc822 format available.

Acknowledgement sent to zimoun <zimon.toutoune <at> gmail.com>:
New bug report received and forwarded. Copy sent to bug-guix <at> gnu.org. (Thu, 21 Jan 2021 11:14:01 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: bug-guix <at> gnu.org
Subject: broken Proof-General (emacs front-end to Coq)
Date: Thu, 21 Jan 2021 12:10:55 +0100
Hi,

Let instantiate an environment:

  guix environment -C -E TERM \
       --ad-hoc coq proof-general emacs \
       busybox \ 
       -- emacs -q

and then “C-h i m“ list ‘Proof General’ and I can read the manual.
However, there is no ELisp about coq-mode or pg stuff.  Let ’M-x shell’
and then:

--8<---------------cut here---------------start------------->8---
$ ls -aR1 $GUIX_ENVIRONMENT | grep '\.el'
guix-emacs.el
guix-emacs.elc
site-start.el
site-start.elc
--8<---------------cut here---------------end--------------->8---

(The package busybox is for debugging: necessary to be able to run Info
in container, list all files and grep them.) 


Maybe it is related to bug#45781 [1].

1: < https://issues.guix.gnu.org/45781>


All the best,
simon




Information forwarded to bug-guix <at> gnu.org:
bug#46016; Package guix. (Thu, 21 Jan 2021 12:09:02 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: 46016 <at> debbugs.gnu.org
Subject: Re: bug#46016: broken Proof-General (emacs front-end to Coq)
Date: Thu, 21 Jan 2021 13:04:27 +0100
Hi,

On Thu, 21 Jan 2021 at 12:10, zimoun <zimon.toutoune <at> gmail.com> wrote:

> Let instantiate an environment:
>
>   guix environment -C -E TERM \
>        --ad-hoc coq proof-general emacs \
>        busybox \ 
>        -- emacs -q
>

[...]

> $ ls -aR1 $GUIX_ENVIRONMENT | grep '\.el'
> guix-emacs.el
> guix-emacs.elc
> site-start.el
> site-start.elc

This command is wrong and shows nothing! :-)

However, note that once Emacs is launched,

 M-: (load “$GUIX_ENVIRONMENT/share/emacs/site-lisp/site-start.d/pg-init.el”)

allows to see the ’ProofGeneral’ front-end; for instance opening a Coq
file and small experiments seem to work.


> Maybe it is related to bug#45781 [1].
>
> 1: < https://issues.guix.gnu.org/45781>

Well, I do not know if it is related.  But what is loaded does not seem
to work as expected.  I mean, I am expecting that all under
’site-lisp/site-start.d/’ are run at start time.


All the best,
simon




Information forwarded to bug-guix <at> gnu.org:
bug#46016; Package guix. (Thu, 21 Jan 2021 21:29:02 GMT) Full text and rfc822 format available.

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

From: Mark H Weaver <mhw <at> netris.org>
To: zimoun <zimon.toutoune <at> gmail.com>, 46016 <at> debbugs.gnu.org
Subject: Re: bug#46016: broken Proof-General (emacs front-end to Coq)
Date: Thu, 21 Jan 2021 16:26:43 -0500
[Message part 1 (text/plain, inline)]
I've been carrying the attached commit on my private branch for a while
now.  It may be an improvement, but I've forgotten the details.  I used
proof-general for a while when I was learning Coq, but have since
removed it because I found it annoying that GNOME Shell misidentified my
normal Emacs as being an instance of Proof General.

      Mark

[0001-LOCAL-gnu-proof-general-Improve-packaging.patch (text/x-patch, inline)]
From a33bc91ac1327e3bcad335bb2eb84abaf7b785cb Mon Sep 17 00:00:00 2001
From: Mark H Weaver <mhw <at> netris.org>
Date: Tue, 7 Apr 2020 05:39:41 -0400
Subject: [PATCH] LOCAL: gnu: proof-general: Improve packaging.

* gnu/packages/coq.scm (proof-general)[arguments]: Remove the
'disable-byte-compile-error-on-warn' and 'clean' custom phases.  Add
'make-installed-binaries-executable' phase.  Adapt 'patch-hardcoded-paths'
phase to new version.  Reindent.
---
 gnu/packages/coq.scm | 52 ++++++++++++++++++++++----------------------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fb6a899b48..656a07f31b 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -148,8 +148,7 @@ It is developed using Objective Caml and Camlp5.")
     (source (origin
               (method git-fetch)
               (uri (git-reference
-                    (url (string-append
-                          "https://github.com/ProofGeneral/PG"))
+                    (url "https://github.com/ProofGeneral/PG.git")
                     (commit (string-append "v" version))))
               (file-name (git-file-name name version))
               (sha256
@@ -176,31 +175,32 @@ It is developed using Objective Caml and Camlp5.")
        #:phases
        (modify-phases %standard-phases
          (delete 'configure)
-         (add-after 'unpack 'disable-byte-compile-error-on-warn
-                    (lambda _
-                      (substitute* "Makefile"
-                        (("\\(setq byte-compile-error-on-warn t\\)")
-                         "(setq byte-compile-error-on-warn nil)"))
-                      #t))
          (add-after 'unpack 'patch-hardcoded-paths
-                    (lambda* (#:key inputs outputs #:allow-other-keys)
-                      (let ((out   (assoc-ref outputs "out"))
-                            (coq   (assoc-ref inputs "coq"))
-                            (emacs (assoc-ref inputs "host-emacs")))
-                        (define (coq-prog name)
-                          (string-append coq "/bin/" name))
-                        (substitute* "Makefile"
-                          (("/sbin/install-info") "install-info"))
-                        (substitute* "bin/proofgeneral"
-                          (("^PGHOMEDEFAULT=.*" all)
-                           (string-append all
-                                          "PGHOME=$PGHOMEDEFAULT\n"
-                                          "EMACS=" emacs "/bin/emacs")))
-                        #t)))
-         (add-after 'unpack 'clean
-           (lambda _
-             ;; Delete the pre-compiled elc files for Emacs 23.
-             (invoke "make" "clean")))
+           (lambda* (#:key inputs outputs #:allow-other-keys)
+             (let ((out   (assoc-ref outputs "out"))
+                   (coq   (assoc-ref inputs "coq"))
+                   (emacs (assoc-ref inputs "host-emacs")))
+               (define (coq-prog name)
+                 (string-append coq "/bin/" name))
+               (make-file-writable "coq/coq-system.el")
+               (emacs-substitute-variables "coq/coq-system.el"
+                 ("coq-prog-name"           (coq-prog "coqtop"))
+                 ("coq-compiler"            (coq-prog "coqc"))
+                 ("coq-dependency-analyzer" (coq-prog "coqdep")))
+               (substitute* "Makefile"
+                 (("/sbin/install-info") "install-info"))
+               (substitute* "bin/proofgeneral"
+                 (("^PGHOMEDEFAULT=.*" all)
+                  (string-append
+                   "PGHOMEDEFAULT=" out "/share/emacs/site-lisp/ProofGeneral\n"
+                   "EMACS=" emacs "/bin/emacs")))
+               #t)))
+         (add-after 'install 'make-installed-binaries-executable
+           (lambda* (#:key outputs #:allow-other-keys)
+             (let ((out (assoc-ref outputs "out")))
+               (for-each (lambda (file) (chmod file #o555))
+                         (find-files (string-append out "/bin")))
+               #t)))
          (add-after 'install 'install-doc
            (lambda* (#:key make-flags #:allow-other-keys)
              ;; XXX FIXME avoid building/installing pdf files,
-- 
2.30.0


Information forwarded to bug-guix <at> gnu.org:
bug#46016; Package guix. (Fri, 22 Jan 2021 10:20:02 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: Mark H Weaver <mhw <at> netris.org>, 46016 <at> debbugs.gnu.org
Subject: Re: bug#46016: broken Proof-General (emacs front-end to Coq)
Date: Fri, 22 Jan 2021 11:15:32 +0100
Hi Mark,

On Thu, 21 Jan 2021 at 16:26, Mark H Weaver <mhw <at> netris.org> wrote:
> I've been carrying the attached commit on my private branch for a while
> now.  It may be an improvement, but I've forgotten the details.  I
> used

Thanks!  It helps.

Based on your patch, I have tweaked a bit and now “bin/proofgeneral“
seems to work.  However, I have not yet tweaked enough to have the Emacs
load-path works.

> +               (substitute* "bin/proofgeneral"
> +                 (("^PGHOMEDEFAULT=.*" all)

What does this line do?


All the best,
simon




Information forwarded to bug-guix <at> gnu.org:
bug#46016; Package guix. (Sun, 24 Jan 2021 18:38:01 GMT) Full text and rfc822 format available.

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

From: John Soo <jsoo1 <at> asu.edu>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 46016 <at> debbugs.gnu.org, Mark H Weaver <mhw <at> netris.org>
Subject: Re: bug#46016: broken Proof-General (emacs front-end to Coq)
Date: Sun, 24 Jan 2021 10:37:46 -0800
Hi zimoun,

I use Proof General pretty regularly. I think this is the same as
https://issues.guix.gnu.org/45781.

Kindly,

John




Information forwarded to bug-guix <at> gnu.org:
bug#46016; Package guix. (Mon, 25 Jan 2021 11:05:01 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: John Soo <jsoo1 <at> asu.edu>
Cc: 46016 <at> debbugs.gnu.org, Mark H Weaver <mhw <at> netris.org>
Subject: Re: bug#46016: broken Proof-General (emacs front-end to Coq)
Date: Mon, 25 Jan 2021 11:54:43 +0100
Hi John,

On Sun, 24 Jan 2021 at 10:37, John Soo <jsoo1 <at> asu.edu> wrote:

> I use Proof General pretty regularly. I think this is the same as
> https://issues.guix.gnu.org/45781.

No, I do not think it is the same issue.

 As the Mark’s patch and my previous message [1] in this thread both
shown, I think the package is misconfigured.  Therefore, how do you use
it?  Maybe, I misunderstand something.


1: https://yhetil.org/guix/86eeielcms.fsf <at> gmail.com


Thanks,
simon




Information forwarded to bug-guix <at> gnu.org:
bug#46016; Package guix. (Mon, 25 Jan 2021 15:15:01 GMT) Full text and rfc822 format available.

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

From: John Soo <jsoo1 <at> asu.edu>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 46016 <at> debbugs.gnu.org, Mark H Weaver <mhw <at> netris.org>
Subject: Re: bug#46016: broken Proof-General (emacs front-end to Coq)
Date: Mon, 25 Jan 2021 07:14:23 -0800
Hi zimoun!

I'm sorry I forgot I had this line in init.el:

(load-file "~/.guix-profile/share/emacs/site-lisp/site-start.d/pg-init.el")

It does seem like proof general is misconfigured. Apologies.

- John




Information forwarded to bug-guix <at> gnu.org:
bug#46016; Package guix. (Wed, 10 Nov 2021 19:39:02 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: 46016 <at> debbugs.gnu.org
Cc: mhw <at> netris.org, public <at> yoctocell.xyz, jsoo1 <at> asu.edu
Subject: Re: bug#46016: broken Proof-General (emacs front-end to Coq)
Date: Wed, 10 Nov 2021 20:38:20 +0100
Hi,

I think this bug is fixed by patch#51755 [1].

1: <http://issues.guix.gnu.org/issue/51755>

Cheers,
simon




Reply sent to zimoun <zimon.toutoune <at> gmail.com>:
You have taken responsibility. (Mon, 22 Nov 2021 18:37:02 GMT) Full text and rfc822 format available.

Notification sent to zimoun <zimon.toutoune <at> gmail.com>:
bug acknowledged by developer. (Mon, 22 Nov 2021 18:37:02 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: 46016-done <at> debbugs.gnu.org
Cc: mhw <at> netris.org, public <at> yoctocell.xyz, jsoo1 <at> asu.edu
Subject: Re: bug#46016: broken Proof-General (emacs front-end to Coq)
Date: Mon, 22 Nov 2021 19:36:04 +0100
Hi,

On Wed, 10 Nov 2021 at 20:38, zimoun <zimon.toutoune <at> gmail.com> wrote:

> 1: <http://issues.guix.gnu.org/issue/51755>

Done with cb296dfa2e2938d18ae0ee347bed0cc94bc79cf8.

Cheers,
simon




bug archived. Request was from Debbugs Internal Request <help-debbugs <at> gnu.org> to internal_control <at> debbugs.gnu.org. (Tue, 21 Dec 2021 12:24:05 GMT) Full text and rfc822 format available.

This bug report was last modified 2 years and 88 days ago.

Previous Next


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