all messages for Guix-related lists mirrored at yhetil.org
 help / color / mirror / code / Atom feed
* [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736.
@ 2021-06-10 13:30 Xinglu Chen
  2021-06-10 16:07 ` zimoun
  2021-06-13 20:41 ` bug#48947: " Ludovic Courtès
  0 siblings, 2 replies; 4+ messages in thread
From: Xinglu Chen @ 2021-06-10 13:30 UTC (permalink / raw)
  To: 48947

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






^ permalink raw reply related	[flat|nested] 4+ messages in thread

* [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736.
  2021-06-10 13:30 [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736 Xinglu Chen
@ 2021-06-10 16:07 ` zimoun
  2021-06-11  9:05   ` Xinglu Chen
  2021-06-13 20:41 ` bug#48947: " Ludovic Courtès
  1 sibling, 1 reply; 4+ messages in thread
From: zimoun @ 2021-06-10 16:07 UTC (permalink / raw)
  To: Xinglu Chen; +Cc: 48947

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>

All the best,
simon




^ permalink raw reply	[flat|nested] 4+ messages in thread

* [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736.
  2021-06-10 16:07 ` zimoun
@ 2021-06-11  9:05   ` Xinglu Chen
  0 siblings, 0 replies; 4+ messages in thread
From: Xinglu Chen @ 2021-06-11  9:05 UTC (permalink / raw)
  To: zimoun; +Cc: 48947

[-- Attachment #1: Type: text/plain, Size: 1574 bytes --]

On Thu, Jun 10 2021, zimoun wrote:

> 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’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).



[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 861 bytes --]

^ permalink raw reply	[flat|nested] 4+ messages in thread

* bug#48947: [PATCH] gnu: proof-general: Update to 4.4-0.bc86736.
  2021-06-10 13:30 [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736 Xinglu Chen
  2021-06-10 16:07 ` zimoun
@ 2021-06-13 20:41 ` Ludovic Courtès
  1 sibling, 0 replies; 4+ messages in thread
From: Ludovic Courtès @ 2021-06-13 20:41 UTC (permalink / raw)
  To: Xinglu Chen; +Cc: 48947-done, zimoun

Hi,

Xinglu Chen <public@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’.




^ permalink raw reply	[flat|nested] 4+ messages in thread

end of thread, other threads:[~2021-06-13 20:42 UTC | newest]

Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-06-10 13:30 [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736 Xinglu Chen
2021-06-10 16:07 ` zimoun
2021-06-11  9:05   ` Xinglu Chen
2021-06-13 20:41 ` bug#48947: " Ludovic Courtès

Code repositories for project(s) associated with this external index

	https://git.savannah.gnu.org/cgit/guix.git

This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.