bug#46016: broken Proof-General (emacs front-end to Coq)

[Mark H Weaver]

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(-)

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