Subject: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs.

From: Liliana Marie Prikler <[email-masked]>
Date: Sun, 21 Nov 2021 20:07:48 +0100

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?