GNU bug report logs -
#46016
broken Proof-General (emacs front-end to Coq)
Previous Next
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.
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):
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):
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):
[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):
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):
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):
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):
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):
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):
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.