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

Previous Next

Full log

Message #14 received at 51755 <at> debbugs.gnu.org (full text, mbox):

From: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 51755 <at> debbugs.gnu.org
Subject: Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads
 for Emacs.
Date: Sun, 21 Nov 2021 19:40:56 +0100

Hello,

zimoun <zimon.toutoune <at> 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

Previous Next

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