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 <m...@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
