Subject: bug#51755: closed (Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs.)

From: [email-masked] (GNU bug Tracking System)
Date: Mon, 22 Nov 2021 18:23:02 +0000

Your bug report

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

which was filed against the guix-patches package, has been closed.

The explanation is attached below, along with your original report.
If you require more details, please reply to [email-masked].

-- 
51755: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=51755
GNU Bug Tracking System
Contact [email-masked] with problems

Subject: Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads for Emacs.
From: Nicolas Goaziou <[email-masked]>
To: zimoun <[email-masked]>
Cc: [email-masked], Liliana Marie Prikler <[email-masked]>
Date: Mon, 22 Nov 2021 19:22:39 +0100
List-Id: <debbugs-submit.debbugs.gnu.org>

Hello,

zimoun <[email-masked]> 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

Subject: [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)
From: zimoun <[email-masked]>
To: [email-masked]
Cc: zimoun <[email-masked]>
Date: Wed, 10 Nov 2021 20:26:22 +0100
List-Id: <debbugs-submit.debbugs.gnu.org>

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