aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorzimoun <zimon.toutoune@gmail.com>2021-11-10 20:37:48 +0100
committerNicolas Goaziou <mail@nicolasgoaziou.fr>2021-11-22 19:21:17 +0100
commitcb296dfa2e2938d18ae0ee347bed0cc94bc79cf8 (patch)
tree664c342e60dadd0cb1a45e48e484c1d6505163cc
parent3d2e41adf2d907311035d60557168696aaeeb381 (diff)
downloadguix-cb296dfa2e2938d18ae0ee347bed0cc94bc79cf8.tar.gz
guix-cb296dfa2e2938d18ae0ee347bed0cc94bc79cf8.zip
gnu: proof-general: Adjust autoloads for Emacs.
Fixes <https://bugs.gnu.org/46016>. * gnu/packages/coq.scm (proof-general)[native-inputs]: Remove 'which'. [inputs]: Remove 'coq' and 'emacs'. [arguments]<#:make-flags>: Adjust to find 'emacs'. Set 'ELISP' and 'DEST_LISP'. <#:modules, #:imported-modules>: Remove. <#:phases>: Remove call to 'which' in Makefile. Add copy file allowing Emacs autoloads. Clean unnecessary code. Signed-off-by: Nicolas Goaziou <mail@nicolasgoaziou.fr>
-rw-r--r--gnu/packages/coq.scm95
1 files changed, 55 insertions, 40 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 1665afc5aa..a27ec53ecb 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -136,50 +136,65 @@ It is developed using Objective Caml and Camlp5.")
"00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa"))))
(build-system gnu-build-system)
(native-inputs
- `(("which" ,which)
- ("emacs" ,emacs-minimal)
+ `(("emacs" ,emacs-minimal)
("texinfo" ,texinfo)))
(inputs
- `(("host-emacs" ,emacs)
- ("perl" ,perl)
- ("coq" ,coq)))
+ `(("perl" ,perl)))
(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")))
+ (let ((base-directory "/share/emacs/site-lisp/ProofGeneral"))
+ `(#:tests? #f ; no check target
+ #:make-flags (list (string-append "PREFIX=" %output)
+ (string-append "EMACS=" (assoc-ref %build-inputs "emacs")
+ "/bin/emacs")
+ (string-append "DEST_PREFIX=" %output)
+ (string-append "ELISP=" %output ,base-directory)
+ (string-append "DEST_ELISP=" %output ,base-directory)
+ (string-append "ELISP_START=" %output ,base-directory))
+ #: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 _
+ (substitute* "Makefile"
+ (("/sbin/install-info") "install-info"))))
+ (add-after 'unpack 'remove-which
+ (lambda _
+ (substitute* "Makefile"
+ (("`which perl`") "perl")
+ (("`which bash`") "bash"))))
+ (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"
- (("/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))))))
+ ((" [^ ]*\\.pdf") ""))
+ (apply invoke "make" "install-doc" make-flags)))
+ (add-after 'install 'allow-subfolders-autoloads
+ ;; Autoload cookies are present in sub-directories. A friendly
+ ;; wrapper proof-general.el around generic/proof-site.el is
+ ;; provided for execution on Emacs start-up. It serves two
+ ;; purposes:
+ ;;
+ ;; * Setting up the load path when byte-compiling pg.
+ ;; * Loading a minimal PG setup on startup (not all of Proof
+ ;; General, of course; mostly mode hooks and autoloads).
+ ;;
+ ;; The renaming to proof-general-autoloads.el is Guix
+ ;; specific.
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((out (assoc-ref outputs "out")))
+ (copy-file "proof-general.el"
+ (string-append out ,base-directory
+ "/proof-general-autoloads.el")))))))))
(home-page "https://proofgeneral.github.io/")
(synopsis "Generic front-end for proof assistants based on Emacs")
(description