From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1 ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms11 with LMTPS id eJTKLXLzCWBmIwAA0tVLHw (envelope-from ) for ; Thu, 21 Jan 2021 21:34:42 +0000 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1 with LMTPS id MHOrKXLzCWCCGgAAbx9fmQ (envelope-from ) for ; Thu, 21 Jan 2021 21:34:42 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 230E19402C2 for ; Thu, 21 Jan 2021 21:34:42 +0000 (UTC) Received: from localhost ([::1]:39826 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1l2hbF-0002mN-3U for larch@yhetil.org; Thu, 21 Jan 2021 16:34:41 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:60702) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1l2hVm-0007J0-F2 for bug-guix@gnu.org; Thu, 21 Jan 2021 16:29:02 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:48020) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1l2hVm-0001zd-7o for bug-guix@gnu.org; Thu, 21 Jan 2021 16:29:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1l2hVm-0002UJ-2x for bug-guix@gnu.org; Thu, 21 Jan 2021 16:29:02 -0500 X-Loop: help-debbugs@gnu.org Subject: bug#46016: broken Proof-General (emacs front-end to Coq) Resent-From: Mark H Weaver Original-Sender: "Debbugs-submit" Resent-CC: bug-guix@gnu.org Resent-Date: Thu, 21 Jan 2021 21:29:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 46016 X-GNU-PR-Package: guix X-GNU-PR-Keywords: To: zimoun , 46016@debbugs.gnu.org Received: via spool by 46016-submit@debbugs.gnu.org id=B46016.16112644859496 (code B ref 46016); Thu, 21 Jan 2021 21:29:02 +0000 Received: (at 46016) by debbugs.gnu.org; 21 Jan 2021 21:28:05 +0000 Received: from localhost ([127.0.0.1]:59566 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1l2hUr-0002T6-Bu for submit@debbugs.gnu.org; Thu, 21 Jan 2021 16:28:05 -0500 Received: from world.peace.net ([64.112.178.59]:37342) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1l2hUo-0002SP-UG for 46016@debbugs.gnu.org; Thu, 21 Jan 2021 16:28:03 -0500 Received: from mhw by world.peace.net with esmtpsa (TLS1.3:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1l2hUi-00037v-7P; Thu, 21 Jan 2021 16:27:56 -0500 From: Mark H Weaver In-Reply-To: <86h7nalf40.fsf@gmail.com> References: <86h7nalf40.fsf@gmail.com> Date: Thu, 21 Jan 2021 16:26:43 -0500 Message-ID: <87v9bqf0b5.fsf@netris.org> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: bug-guix@gnu.org List-Id: Bug reports for GNU Guix List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: bug-guix-bounces+larch=yhetil.org@gnu.org Sender: "bug-Guix" X-Migadu-Flow: FLOW_IN X-Migadu-Spam-Score: -2.35 Authentication-Results: aspmx1.migadu.com; dkim=none; dmarc=none; spf=pass (aspmx1.migadu.com: domain of bug-guix-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=bug-guix-bounces@gnu.org X-Migadu-Queue-Id: 230E19402C2 X-Spam-Score: -2.35 X-Migadu-Scanner: scn0.migadu.com X-TUID: vxCJ7YJbO7/A --=-=-= Content-Type: text/plain 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 --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0001-LOCAL-gnu-proof-general-Improve-packaging.patch Content-Description: Patch to possibly improve Proof General packaging in Guix >From a33bc91ac1327e3bcad335bb2eb84abaf7b785cb Mon Sep 17 00:00:00 2001 From: Mark H Weaver 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 --=-=-=--