| Message ID | 20211110193748.368696-1-zimon.toutoune@gmail.com |
|---|---|
| State | Accepted |
| Headers | show |
| Series | Fix ProofGeneral (emacs front-end for Coq) | expand |
| Context | Check | Description |
|---|---|---|
| cbaines/comparison | success | View comparision |
| cbaines/git branch | success | View Git branch |
| cbaines/applying patch | success | View Laminar job |
| cbaines/issue | success | View issue |
Hello, zimoun <zimon.toutoune@gmail.com> writes: > * 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. Thanks. > + (add-after 'install 'allow-subfolders-autoloads > + (lambda* (#:key outputs #:allow-other-keys) > + (let ((out (assoc-ref outputs "out"))) > + ;; Make it visible by Emacs > + (copy-file "proof-general.el" > + (string-append out ,base-directory > + "/proof-general-autoloads.el"))))))))) So, IIUC, the above is basically a hack: you disguise the main file into an autoloads file because no autoloads file is generated from the code base? If so, this might deserve a longer comment, IMO. Otherwise, LGTM. Regards,
Hi, Am Sonntag, den 21.11.2021, 19:40 +0100 schrieb Nicolas Goaziou: > > + (add-after 'install 'allow-subfolders-autoloads > > + (lambda* (#:key outputs #:allow-other-keys) > > + (let ((out (assoc-ref outputs "out"))) > > + ;; Make it visible by Emacs > > + (copy-file "proof-general.el" > > + (string-append out ,base-directory > > + "/proof-general- > > autoloads.el"))))))))) > > So, IIUC, the above is basically a hack: you disguise the main file > into an autoloads file because no autoloads file is generated from > the code base? If so, this might deserve a longer comment, IMO. On a related note, what would be so bad about having to (require 'proof-general) interactively? Alternatively, we could in an after- unpack phase add autoload cookies to the source file or write our own autoloads altogether. WDYT?
Hello, Liliana Marie Prikler <liliana.prikler@gmail.com> writes: > Am Sonntag, den 21.11.2021, 19:40 +0100 schrieb Nicolas Goaziou: >> So, IIUC, the above is basically a hack: you disguise the main file >> into an autoloads file because no autoloads file is generated from >> the code base? If so, this might deserve a longer comment, IMO. Actually, my assumption was wrong. "proof-general.el" is a meta-autoloads file: ;; This file is a thin, package.el-friendly wrapper around generic/proof-site, ;; suitable 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). > On a related note, what would be so bad about having to (require > 'proof-general) interactively? When not byte compiled, the file only does (require 'proof-site (expand-file-name "generic/proof-site" pg-init--pg-root))) I guess we could also provide a single autoloads file doing just that or, according to the manual, (load "PROOF-GENERAL-HOME/generic/proof-site.el") > Alternatively, we could in an after- > unpack phase add autoload cookies to the source file or write our own > autoloads altogether. WDYT? Autoload cookies are already present in the code base, but in sub-directories. OTOH, I assume the solution proposed by Zimoun, as hackish as it is, works well enough. And it requires less work. IMO, it is acceptable with a good comment. Regards,
Hi, Thanks for the review. On Sun, 21 Nov 2021 at 21:15, Nicolas Goaziou <mail@nicolasgoaziou.fr> wrote: > Liliana Marie Prikler <liliana.prikler@gmail.com> writes: >> Am Sonntag, den 21.11.2021, 19:40 +0100 schrieb Nicolas Goaziou: >>> So, IIUC, the above is basically a hack: you disguise the main file >>> into an autoloads file because no autoloads file is generated from >>> the code base? If so, this might deserve a longer comment, IMO. > > Actually, my assumption was wrong. "proof-general.el" is > a meta-autoloads file: > > ;; This file is a thin, package.el-friendly wrapper around generic/proof-site, > ;; suitable 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). Yes. Note that ’proof-general’ was at one moment in its long history a standalone package, i.e., running ’bin/proofgeneneral’ started Emacs and launched everything. This had been removed long time ago [1] but the current code inherits this long history. 1: <https://github.com/ProofGeneral/PG/commit/1a18e33658645a81225c56b5d4f4a4b89434d301> >> Alternatively, we could in an after- >> unpack phase add autoload cookies to the source file or write our own >> autoloads altogether. WDYT? > > Autoload cookies are already present in the code base, but in > sub-directories. Yes. The limitation comes from this subdirectory structure. This breaks the usual way of packaging Emacs tools for Guix, IIUC. > OTOH, I assume the solution proposed by Zimoun, as hackish as it is, > works well enough. And it requires less work. IMO, it is acceptable with > a good comment. From my point of view, my proposed patch appears to me the easiest fix. If something is better, please let me know. :-) About the comment, I thought « allow-subfolders-autoloads » and « Make it visible by Emacs » would have been enough. ;-) --8<---------------cut here---------------start------------->8--- (add-after 'install 'allow-subfolders-autoloads (lambda* (#:key outputs #:allow-other-keys) (let ((out (assoc-ref outputs "out"))) ;; Make it visible by Emacs --8<---------------cut here---------------end--------------->8--- Instead, I propose to extend to: --8<---------------cut here---------------start------------->8--- (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 rename 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"))))))))) --8<---------------cut here---------------end--------------->8--- Is it fine? If yes, I can send* a v2. Or please push directly. :-) Cheers, simon *send v2: for the record, I do not have commit right. ;-)
Hi Nicolas,
On Mon, 22 Nov 2021 at 19:22, Nicolas Goaziou <mail@nicolasgoaziou.fr> wrote:
> I pushed it directly. Thank you!
Thank you.
Cheers,
simon
Hello, zimoun <zimon.toutoune@gmail.com> writes: > Instead, I propose to extend to: > > --8<---------------cut here---------------start------------->8--- > (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 rename 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"))))))))) > --8<---------------cut here---------------end--------------->8--- > > > Is it fine? If yes, I can send* a v2. Or please push directly. :-) I pushed it directly. Thank you! Regards,
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index dccb9bea4c..2cf9d1a602 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -135,50 +135,55 @@ (define-public proof-general "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 + (lambda* (#:key outputs #:allow-other-keys) + (let ((out (assoc-ref outputs "out"))) + ;; Make it visible by Emacs + (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