broken Proof-General (emacs front-end to Coq)

  • Done
  • quality assurance status badge
Details
3 participants
  • John Soo
  • Mark H Weaver
  • zimoun
Owner
unassigned
Submitted by
zimoun
Severity
normal
Z
Z
zimoun wrote on 21 Jan 2021 12:10
(address . bug-guix@gnu.org)
86h7nalf40.fsf@gmail.com
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:

Toggle snippet (7 lines)
$ ls -aR1 $GUIX_ENVIRONMENT | grep '\.el'
guix-emacs.el
guix-emacs.elc
site-start.el
site-start.elc

(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].



All the best,
simon
Z
Z
zimoun wrote on 21 Jan 2021 13:04
(address . 46016@debbugs.gnu.org)
86eeielcms.fsf@gmail.com
Hi,

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

Toggle quote (8 lines)
> Let instantiate an environment:
>
> guix environment -C -E TERM \
> --ad-hoc coq proof-general emacs \
> busybox \
> -- emacs -q
>

[...]

Toggle quote (6 lines)
> $ 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.


Toggle quote (4 lines)
> 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
M
M
Mark H Weaver wrote on 21 Jan 2021 22:26
87v9bqf0b5.fsf@netris.org
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
From a33bc91ac1327e3bcad335bb2eb84abaf7b785cb Mon Sep 17 00:00:00 2001
From: Mark H Weaver <mhw@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(-)

Toggle diff (73 lines)
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
Z
Z
zimoun wrote on 22 Jan 2021 11:15
86bldhl1kr.fsf@gmail.com
Hi Mark,

On Thu, 21 Jan 2021 at 16:26, Mark H Weaver <mhw@netris.org> wrote:
Toggle quote (4 lines)
> 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.

Toggle quote (3 lines)
> + (substitute* "bin/proofgeneral"
> + (("^PGHOMEDEFAULT=.*" all)

What does this line do?


All the best,
simon
J
Z
Z
zimoun wrote on 25 Jan 2021 11:54
(name . John Soo)(address . jsoo1@asu.edu)
867do1l218.fsf@gmail.com
Hi John,

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

Toggle quote (3 lines)
> 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.




Thanks,
simon
J
J
John Soo wrote on 25 Jan 2021 16:14
(name . zimoun)(address . zimon.toutoune@gmail.com)
874kj5vyk0.fsf@asu.edu
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
Z
Z
Z
zimoun wrote on 22 Nov 2021 19:36
(address . 46016-done@debbugs.gnu.org)
87zgpwqbqj.fsf@gmail.com
Hi,

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

Toggle quote (2 lines)
Done with cb296dfa2e2938d18ae0ee347bed0cc94bc79cf8.

Cheers,
simon
Closed
?
Your comment

This issue is archived.

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

To respond to this issue using the mumi CLI, first switch to it
mumi current 46016
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch