GNU bug report logs - #51755
[PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)

Previous Next

Full log

View this message in rfc822 format

From: zimoun <zimon.toutoune <at> gmail.com>
To: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>, Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Cc: 51755 <at> debbugs.gnu.org
Subject: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs.
Date: Sun, 21 Nov 2021 22:11:58 +0100

Hi,

Thanks for the review.


On Sun, 21 Nov 2021 at 21:15, Nicolas Goaziou <mail <at> nicolasgoaziou.fr> wrote:
> Liliana Marie Prikler <liliana.prikler <at> 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. ;-)

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.