me
/
guix
Archived
1
0
Fork 0
Code

gnu: proof-general: Update to 4.4-0.bc86736. 

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.

Signed-off-by: Ludovic Courtès <ludo@gnu.org>
master
Xinglu Chen 2021-06-10 15:30:06 +02:00 committed by Ludovic Courtès
parent 9eabf4983f
commit 44ed008ac1
No known key found for this signature in database
GPG Key ID: 090B11993D9AEBB5
1 changed files with 69 additions and 71 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
gnu/packages/coq.scm
View File

@ -6,6 +6,7 @@
;;; Copyright © 2020 Björn Höfling <bjoern.hoefling@bjoernhoefling.de> ;;; Copyright © 2020 Björn Höfling <bjoern.hoefling@bjoernhoefling.de>
;;; Copyright © 2020 raingloom <raingloom@riseup.net> ;;; Copyright © 2020 raingloom <raingloom@riseup.net>
;;; Copyright © 2020 Robin Green <greenrd@greenrd.org> ;;; Copyright © 2020 Robin Green <greenrd@greenrd.org>
;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
;;; ;;;
;;; This file is part of GNU Guix. ;;; This file is part of GNU Guix.
;;; ;;;
@ -142,19 +143,23 @@ It is developed using Objective Caml and Camlp5.")
(license (list license:lgpl2.1 license:opl1.0+)))) (license (list license:lgpl2.1 license:opl1.0+))))
(define-public proof-general (define-public proof-general
;; 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 (package
(name "proof-general") (name "proof-general")
(version "4.4") (version (git-version "4.4" revision commit))
(source (origin (source (origin
(method git-fetch) (method git-fetch)
(uri (git-reference (uri (git-reference
(url (string-append (url "https://github.com/ProofGeneral/PG")
"https://github.com/ProofGeneral/PG")) (commit commit)))
(commit (string-append "v" version))))
(file-name (git-file-name name version)) (file-name (git-file-name name version))
(sha256 (sha256
(base32 (base32
"0bdfk91wf71z80mdfnl8hpinripndcjgdkz854zil6521r84nqk8")))) "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa"))))
(build-system gnu-build-system) (build-system gnu-build-system)
(native-inputs (native-inputs
`(("which" ,which) `(("which" ,which)
@ -167,7 +172,9 @@ It is developed using Objective Caml and Camlp5.")
(arguments (arguments
`(#:tests? #f ; no check target `(#:tests? #f ; no check target
#:make-flags (list (string-append "PREFIX=" %output) #:make-flags (list (string-append "PREFIX=" %output)
(string-append "DEST_PREFIX=" %output)) (string-append "DEST_PREFIX=" %output)
(string-append "ELISP_START=" %output
"/share/emacs/site-lisp/ProofGeneral"))
#:modules ((guix build gnu-build-system) #:modules ((guix build gnu-build-system)
(guix build utils) (guix build utils)
(guix build emacs-utils)) (guix build emacs-utils))
@ -180,23 +187,14 @@ It is developed using Objective Caml and Camlp5.")
(lambda _ (lambda _
(substitute* "Makefile" (substitute* "Makefile"
(("\\(setq byte-compile-error-on-warn t\\)") (("\\(setq byte-compile-error-on-warn t\\)")
"(setq byte-compile-error-on-warn nil)")) "(setq byte-compile-error-on-warn nil)"))))
#t))
(add-after 'unpack 'patch-hardcoded-paths (add-after 'unpack 'patch-hardcoded-paths
(lambda* (#:key inputs outputs #:allow-other-keys) (lambda* (#:key inputs outputs #:allow-other-keys)
(let ((out (assoc-ref outputs "out")) (let ((out (assoc-ref outputs "out"))
(coq (assoc-ref inputs "coq")) (coq (assoc-ref inputs "coq"))
(emacs (assoc-ref inputs "host-emacs"))) (emacs (assoc-ref inputs "host-emacs")))
(define (coq-prog name)
(string-append coq "/bin/" name))
(substitute* "Makefile" (substitute* "Makefile"
(("/sbin/install-info") "install-info")) (("/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 (add-after 'unpack 'clean
(lambda _ (lambda _
;; Delete the pre-compiled elc files for Emacs 23. ;; Delete the pre-compiled elc files for Emacs 23.
@ -208,13 +206,13 @@ It is developed using Objective Caml and Camlp5.")
(substitute* "Makefile" (substitute* "Makefile"
((" [^ ]*\\.pdf") "")) ((" [^ ]*\\.pdf") ""))
(apply invoke "make" "install-doc" make-flags)))))) (apply invoke "make" "install-doc" make-flags))))))
(home-page "https://proofgeneral.github.io/ ") (home-page "https://proofgeneral.github.io/")
(synopsis "Generic front-end for proof assistants based on Emacs") (synopsis "Generic front-end for proof assistants based on Emacs")
(description (description
"Proof General is a major mode to turn Emacs into an interactive proof "Proof General is a major mode to turn Emacs into an interactive proof
assistant to write formal mathematical proofs using a variety of theorem assistant to write formal mathematical proofs using a variety of theorem
provers.") provers.")
(license license:gpl2+))) (license license:gpl2+))))
(define-public coq-flocq (define-public coq-flocq
(package (package