[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Nicolas Goaziou
Subject: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs.
Date: Sun, 21 Nov 2021 21:15:30 +0100
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux)


Liliana Marie Prikler <> 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 
    ;; 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 
    ;;   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" 

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

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.

Nicolas Goaziou

reply via email to

[Prev in Thread] Current Thread [Next in Thread]