bug#51755: closed ([PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq))

[GNU bug Tracking System]

Your message dated Mon, 22 Nov 2021 19:22:39 +0100
with message-id <87r1b8t5hs.fsf@nicolasgoaziou.fr>
and subject line Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust 
autoloads for Emacs.
has caused the debbugs.gnu.org bug report #51755,
regarding [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)
to be marked as done.

(If you believe you have received this mail in error, please contact
help-debbugs@gnu.org.)


-- 
51755: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=51755
GNU Bug Tracking System
Contact help-debbugs@gnu.org with problems
> --- Begin Message ---
>
>
>
> Subject: 
>
> [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)
>
>
>
>
> Date: 
>
> Wed, 10 Nov 2021 20:26:22 +0100
>
>
>
>
> Hi,
>
> This is a follow-up of bug#46016 [1] and I think close it.
>
> Now, it is possible to use ProofGeneral as any other Emacs packages.  For
> instance,
>
>    guix shell emacs proof-general coq
>    emacs foo.v
>
> For now, the dependency of 'coq' is removed as with many Emacs packages.
> Other said, the user has to provide such dependency.  IMHO, it is the spirit
> of such package where the 'prover' is let to the user (several are more or
> less supported, see doc [2]).
>
> Cheers,
> simon
>
>
>
> 1: <http://issues.guix.gnu.org/issue/46016>
> 2: 
> <https://proofgeneral.github.io/doc/master/userman/Introducing-Proof-General/#Supported-proof-assistants>
>
>
> zimoun (1):
>   gnu: proof-general: Adjust autoloads for Emacs.
>
>  gnu/packages/coq.scm | 85 +++++++++++++++++++++++---------------------
>  1 file changed, 45 insertions(+), 40 deletions(-)
>
>
> base-commit: 140b486437670ce95cb24a935b58cba52a9dac31
> -- 
> 2.33.1
>
>
>
>
> --- End Message ---
> --- Begin Message ---
>
>
>
> Subject: 
>
> Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs.
>
>
>
>
> Date: 
>
> Mon, 22 Nov 2021 19:22:39 +0100
>
>
>
>
> User-agent: 
>
> Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux)
>
>
>
>
> Hello,
>
> zimoun <zimon.toutoune@gmail.com> writes:
>
> > Instead, I propose to extend to:
> >
> > --8<---------------cut here---------------start------------->8---
> >              (add-after 'install 'allow-subfolders-autoloads
> >                ;; Autoload cookies are present in sub-directories. A friendly
> >                ;; wrapper proof-general.el around generic/proof-site.el is
> >                ;; provided 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).
> >                ;; The rename to proof-general-autoloads.el is Guix specific.
> >                (lambda* (#:key outputs #:allow-other-keys)
> >                  (let ((out (assoc-ref outputs "out")))
> >                    (copy-file "proof-general.el"
> >                               (string-append out ,base-directory
> >                                              
> > "/proof-general-autoloads.el")))))))))
> > --8<---------------cut here---------------end--------------->8---
> >
> >
> > Is it fine?  If yes, I can send* a v2.  Or please push directly. :-)
>
> I pushed it directly. Thank you!
>
> Regards,
> -- 
> Nicolas Goaziou
>
>
> --- End Message ---