[PATCH] gnu: proof-general: Update to 4.4-0.bc86736.

DoneSubmitted by Xinglu Chen.
Details
3 participants
  • Ludovic Courtès
  • Xinglu Chen
  • zimoun
Owner
unassigned
Severity
normal
X
X
Xinglu Chen wrote 4 days ago
(address . guix-patches@gnu.org)
287f5f7500552106833f349c1f9493ab89470b39.1623331764.git.public@yoctocell.xyz
There hasn’t been a new release since 2016 and there has been more than 450new 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 phaseswith #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(-)
Toggle diff (164 lines)diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scmindex 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@bjoernhoefling.de> ;;; Copyright © 2020 raingloom <raingloom@riseup.net> ;;; Copyright © 2020 Robin Green <greenrd@greenrd.org>+;;; Copyright © 2021 Xinglu Chen <public@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
Z
Z
zimoun wrote 4 days ago
(name . Xinglu Chen)(address . public@yoctocell.xyz)(address . 48947@debbugs.gnu.org)
CAJ3okZ2yQG61uR5PYSHsDKFHX03cNBfyFUnKfD=sqGwy9WPemA@mail.gmail.com
Hi,
On Thu, 10 Jun 2021 at 15:31, Xinglu Chen <public@yoctocell.xyz> wrote:
Toggle quote (4 lines)>> 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
X
X
Xinglu Chen wrote 3 days ago
(name . zimoun)(address . zimon.toutoune@gmail.com)(address . 48947@debbugs.gnu.org)
87pmwsbwld.fsf@yoctocell.xyz
On Thu, Jun 10 2021, zimoun wrote:
Toggle quote (13 lines)> Hi,>> On Thu, 10 Jun 2021 at 15:31, Xinglu Chen <public@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’table 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
Toggle snippet (12 lines)ELISPP=share/${EMACS}/site-lisp/ProofGeneralELISP_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
With this patch, I set the ELISP_START variable to the same value osELISPP, 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 juststarting looking into Coq).
-----BEGIN PGP SIGNATURE-----
iQJJBAEBCAAzFiEEAVhh4yyK5+SEykIzrPUJmaL7XHkFAmDDJz4VHHB1YmxpY0B5b2N0b2NlbGwueHl6AAoJEKz1CZmi+1x5ThsP/inqkyFcjhjKnOpf+l2XQ7hKmUfM42jvKCIcnlHsxpK0zpsc+aTIX/1o9XFDoBkPfvISG65GqAujiiJgI++pVHH5ebfDpX42arbu785xD024XWdKIcR5mNG45Ct/wotRDiQuMUkgzmnWyA8KD+jLB7wqRha4KLt+IUKzHmc6k1qG1JNiPM+knQ6LYs08kRIWwXDK+sIa19A3oUNGBPGF3KVW1Dyrj1y8RGJaFzV6kRFj8yzkmCbRD24MXSJGX9qdbbi4lNAgXIOpcctGU2keUCGtsl9GZAUdU0eqca8gNHfactPX25tEFrSHrsEp02dMmG4ZYX1v3psO0r28iOCrRTTNCHVvqUWQlPYVHre6XGLvwlSAi0e5KV/0SAIewsdNcVr/k4ZTfJ4BipJZmSQqETibMlhCAgygFXzsgFUtaPtGw0HbzGbu9PWgLgRyuuFPEhx7i2KfPYU4jyXKIvWTX+fJ2wtQi8c9Us65a6MKPPkFNrQhdEGPJUU6/PTjCfHGVNL1iFoWgJ5OE/W6GTgcuFeT0reiWFcxFGqiPBuktEwphpYPajh5jnBQnnnJ/iROXggarHMoC7yRbzE70HP90fXplAXZM0qcuvG2MIJZl1QmdYG1YNVY65w3WebXU/SOusSt99DyItx+3eQjlL+SRX2+fDZGDQtILkOvyAHi2qiG=Gf/G-----END PGP SIGNATURE-----
L
L
Ludovic Courtès wrote 9 hours ago
Re: bug#48947: [PATCH] gnu: proof-general: Update to 4.4-0.bc86736.
(name . Xinglu Chen)(address . public@yoctocell.xyz)
87k0mxzee5.fsf@gnu.org
Hi,
Xinglu Chen <public@yoctocell.xyz> skribis:
Toggle quote (10 lines)> 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’.
Closed
?