GNU bug report logs - #48947
[PATCH] gnu: proof-general: Update to 4.4-0.bc86736.

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 48947 in the body.
You can then email your comments to 48947 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Xinglu Chen <public <at> yoctocell.xyz>
To: guix-patches <at> gnu.org
Subject: [PATCH] gnu: proof-general: Update to 4.4-0.bc86736.
Date: Thu, 10 Jun 2021 15:30:06 +0200

There hasn’t been a new release since 2016 and there has been more than 450
new commits since then.

* gnu/packages/coq.scm (proof-general): Update to 4.4-0.bc86736.
[arguments]<#:make-flags>: Set ELISP_START.
<#:phases>: Remove ‘coq-prog’ procedure which was unused; don’t run
‘substitute*’ on bin/proofgeneral since it no longer exists.  Don’t end phases
with #t, this will be unnecessary once the ‘core-updates’ branch is merged.
[home-page]: Remove trailing whitesapce.
---
 gnu/packages/coq.scm | 140 +++++++++++++++++++++----------------------
 1 file changed, 69 insertions(+), 71 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fb6a899b48..fa1f4078b8 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -6,6 +6,7 @@
 ;;; Copyright © 2020 Björn Höfling <bjoern.hoefling <at> bjoernhoefling.de>
 ;;; Copyright © 2020 raingloom <raingloom <at> riseup.net>
 ;;; Copyright © 2020 Robin Green <greenrd <at> greenrd.org>
+;;; Copyright © 2021 Xinglu Chen <public <at> yoctocell.xyz>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -142,79 +143,76 @@ It is developed using Objective Caml and Camlp5.")
     (license (list license:lgpl2.1 license:opl1.0+))))
 
 (define-public proof-general
-  (package
-    (name "proof-general")
-    (version "4.4")
-    (source (origin
-              (method git-fetch)
-              (uri (git-reference
-                    (url (string-append
-                          "https://github.com/ProofGeneral/PG"))
-                    (commit (string-append "v" version))))
-              (file-name (git-file-name name version))
-              (sha256
-               (base32
-                "0bdfk91wf71z80mdfnl8hpinripndcjgdkz854zil6521r84nqk8"))))
-    (build-system gnu-build-system)
-    (native-inputs
-     `(("which" ,which)
-       ("emacs" ,emacs-minimal)
-       ("texinfo" ,texinfo)))
-    (inputs
-     `(("host-emacs" ,emacs)
-       ("perl" ,perl)
-       ("coq" ,coq)))
-    (arguments
-     `(#:tests? #f  ; no check target
-       #:make-flags (list (string-append "PREFIX=" %output)
-                          (string-append "DEST_PREFIX=" %output))
-       #:modules ((guix build gnu-build-system)
-                  (guix build utils)
-                  (guix build emacs-utils))
-       #:imported-modules (,@%gnu-build-system-modules
-                           (guix build emacs-utils))
-       #: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")))
-         (add-after 'install 'install-doc
-           (lambda* (#:key make-flags #:allow-other-keys)
-             ;; XXX FIXME avoid building/installing pdf files,
-             ;; due to unresolved errors building them.
-             (substitute* "Makefile"
-               ((" [^ ]*\\.pdf") ""))
-             (apply invoke "make" "install-doc" make-flags))))))
-    (home-page "https://proofgeneral.github.io/ ")
-    (synopsis "Generic front-end for proof assistants based on Emacs")
-    (description
-     "Proof General is a major mode to turn Emacs into an interactive proof
+  ;; The latest release is from 2016 and there has been more than 450 commits
+  ;; since then.
+  ;; Commit from 2021-06-07.
+  (let ((commit "bc86736abb728ec0d28abc90ef0adae21d29a66a")
+        (revision "0"))
+    (package
+      (name "proof-general")
+      (version (git-version "4.4" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/ProofGeneral/PG")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa"))))
+      (build-system gnu-build-system)
+      (native-inputs
+       `(("which" ,which)
+         ("emacs" ,emacs-minimal)
+         ("texinfo" ,texinfo)))
+      (inputs
+       `(("host-emacs" ,emacs)
+         ("perl" ,perl)
+         ("coq" ,coq)))
+      (arguments
+       `(#:tests? #f                   ; no check target
+         #:make-flags (list (string-append "PREFIX=" %output)
+                            (string-append "DEST_PREFIX=" %output)
+                            (string-append "ELISP_START=" %output
+                                           "/share/emacs/site-lisp/ProofGeneral"))
+         #:modules ((guix build gnu-build-system)
+                    (guix build utils)
+                    (guix build emacs-utils))
+         #:imported-modules (,@%gnu-build-system-modules
+                             (guix build emacs-utils))
+         #: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)"))))
+           (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")))
+                 (substitute* "Makefile"
+                   (("/sbin/install-info") "install-info")))))
+           (add-after 'unpack 'clean
+             (lambda _
+               ;; Delete the pre-compiled elc files for Emacs 23.
+               (invoke "make" "clean")))
+           (add-after 'install 'install-doc
+             (lambda* (#:key make-flags #:allow-other-keys)
+               ;; XXX FIXME avoid building/installing pdf files,
+               ;; due to unresolved errors building them.
+               (substitute* "Makefile"
+                 ((" [^ ]*\\.pdf") ""))
+               (apply invoke "make" "install-doc" make-flags))))))
+      (home-page "https://proofgeneral.github.io/")
+      (synopsis "Generic front-end for proof assistants based on Emacs")
+      (description
+       "Proof General is a major mode to turn Emacs into an interactive proof
 assistant to write formal mathematical proofs using a variety of theorem
 provers.")
-    (license license:gpl2+)))
+      (license license:gpl2+))))
 
 (define-public coq-flocq
   (package

base-commit: ac886034020b11b647f893116824f7d7b998ce82
-- 
2.32.0

Message #8 received at 48947 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Xinglu Chen <public <at> yoctocell.xyz>
Cc: 48947 <at> debbugs.gnu.org
Subject: Re: [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736.
Date: Thu, 10 Jun 2021 18:07:03 +0200

Hi,

On Thu, 10 Jun 2021 at 15:31, Xinglu Chen <public <at> yoctocell.xyz> wrote:
>
> There hasn’t been a new release since 2016 and there has been more than 450
> new commits since then.

Cool!

Does this patch fix the bug#46016?

<http://issues.guix.gnu.org/issue/46016>

All the best,
simon

Message #11 received at 48947 <at> debbugs.gnu.org (full text, mbox):

From: Xinglu Chen <public <at> yoctocell.xyz>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 48947 <at> debbugs.gnu.org
Subject: Re: [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736.
Date: Fri, 11 Jun 2021 11:05:02 +0200

[Message part 1 (text/plain, inline)]

On Thu, Jun 10 2021, zimoun wrote:

> Hi,
>
> On Thu, 10 Jun 2021 at 15:31, Xinglu Chen <public <at> yoctocell.xyz> wrote:
>>
>> There hasn’t been a new release since 2016 and there has been more than 450
>> new commits since then.
>
> Cool!
>
> Does this patch fix the bug#46016?
>
> <http://issues.guix.gnu.org/issue/46016>

I didn’t know about this bug report, but I did notice that Emacs wasn’t
able to load the Elisp files (M-x coq-mode didn’t work).

Proof General generates a pg-init.el file in
/path/to/guix-profile/share/emacs/site-lisp/ProofGeneral/site-start.d,
Emacs isn’t able to find that file, so doing (require 'proof-site)
doesn’t work.

Relevant part of the Makefile

--8<---------------cut here---------------start------------->8---
ELISPP=share/${EMACS}/site-lisp/ProofGeneral
ELISP_START=${PREFIX}/share/${EMACS}/site-lisp/site-start.d

[...]

install-init:
	mkdir -p ${ELISP_START}
	echo ';;; pg-init.el --- setup for Proof General' > ${ELISP_START}/pg-init.el
	echo "(setq load-path (append load-path '(\"${DEST_ELISP}/generic\")))" >> ${ELISP_START}/pg-init.el
	echo "(require 'proof-site)" >> ${ELISP_START}/pg-init.el
--8<---------------cut here---------------end--------------->8---

With this patch, I set the ELISP_START variable to the same value os
ELISPP, now the pg-init.el file ends up in the ProofGeneral directory,
and Emacs is now able to find it.  Doing (require 'proof-site) worked,
and M-x coq-mode created a splash screen, so it seems to work (I just
starting looking into Coq).

[signature.asc (application/pgp-signature, inline)]

Message #16 received at 48947-done <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: Xinglu Chen <public <at> yoctocell.xyz>
Cc: 48947-done <at> debbugs.gnu.org, zimoun <zimon.toutoune <at> gmail.com>
Subject: Re: bug#48947: [PATCH] gnu: proof-general: Update to 4.4-0.bc86736.
Date: Sun, 13 Jun 2021 22:41:06 +0200

Hi,

Xinglu Chen <public <at> yoctocell.xyz> skribis:

> There hasn’t been a new release since 2016 and there has been more than 450
> new commits since then.
>
> * gnu/packages/coq.scm (proof-general): Update to 4.4-0.bc86736.
> [arguments]<#:make-flags>: Set ELISP_START.
> <#:phases>: Remove ‘coq-prog’ procedure which was unused; don’t run
> ‘substitute*’ on bin/proofgeneral since it no longer exists.  Don’t end phases
> with #t, this will be unnecessary once the ‘core-updates’ branch is merged.
> [home-page]: Remove trailing whitesapce.

Applied, thanks!

I let you check whether the issue zimoun refers to can be closed.

Ludo’.

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.