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

[Nicolas Goaziou]

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