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

[Nicolas Goaziou]

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,
-- 
Nicolas Goaziou