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

Previous Next

Full log

View this message in rfc822 format

From: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: zimoun <zimon.toutoune <at> gmail.com>
Subject: bug#51755: closed (Re: [bug#51755] [PATCH 1/1] gnu:
 proof-general: Adjust autoloads for Emacs.)
Date: Mon, 22 Nov 2021 18:23:02 +0000

[Message part 1 (text/plain, inline)]

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 51755 <at> debbugs.gnu.org.

-- 
51755: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=51755
GNU Bug Tracking System
Contact help-debbugs <at> gnu.org with problems

[Message part 2 (message/rfc822, inline)]

From: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 51755-done <at> debbugs.gnu.org,
 Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Subject: Re: [bug#51755] [PATCH 1/1] gnu: proof-general: Adjust autoloads
 for Emacs.
Date: Mon, 22 Nov 2021 19:22:39 +0100

Hello,

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

[Message part 3 (message/rfc822, inline)]

From: zimoun <zimon.toutoune <at> gmail.com>
To: guix-patches <at> gnu.org
Cc: zimoun <zimon.toutoune <at> gmail.com>
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

Previous Next

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