GNU bug report logs - #40311
[PATCH] Update proof-general

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 40311 in the body.
You can then email your comments to 40311 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

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

From: John Soo <jsoo1 <at> asu.edu>
To: guix-patches <at> gnu.org
Subject: [PATCH] Update proof-general
Date: Sun, 29 Mar 2020 03:06:34 -0700

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

Hi Guix,

In my effort to use strictly guix for my emacs package management, I
found that proof-general was not working out of the box with guix.el.

In the end I could not figure out how to make it work, but I did update
proof-general to 4.4 and updated the home-page.

proof-general puts its initialization file in
%outputs/share/emacs/site-lisp/site-start.d/pg-init.el. I also see
Tuareg puts the file there. Niether that path, nor any subdirectory of
site-lisp is included by $EMACSLOADPATH or is autoloaded by guix.el.

For the record, I added
(load-file "~/.guix-profile/share/emacs/site-lisp/site-start.d/pg-init.el")
to init.el as a workaround.

Anyways, this should fix proof-general to work with the current version
of coq at least and add some more newer niceties in recent versions.

Thanks, as always!

John

[0001-gnu-proof-general-Update-to-4.4.patch (text/x-patch, attachment)]

[0002-gnu-proof-general-Update-home-page.patch (text/x-patch, attachment)]

Message #10 received at 40311-done <at> debbugs.gnu.org (full text, mbox):

From: Marius Bakke <mbakke <at> fastmail.com>
To: John Soo <jsoo1 <at> asu.edu>, 40311-done <at> debbugs.gnu.org
Subject: Re: [bug#40311] [PATCH] Update proof-general
Date: Thu, 02 Apr 2020 18:59:52 +0200

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

John Soo <jsoo1 <at> asu.edu> writes:

> Hi Guix,
>
> In my effort to use strictly guix for my emacs package management, I
> found that proof-general was not working out of the box with guix.el.
>
> In the end I could not figure out how to make it work, but I did update
> proof-general to 4.4 and updated the home-page.
>
> proof-general puts its initialization file in
> %outputs/share/emacs/site-lisp/site-start.d/pg-init.el. I also see
> Tuareg puts the file there. Niether that path, nor any subdirectory of
> site-lisp is included by $EMACSLOADPATH or is autoloaded by guix.el.
>
> For the record, I added
> (load-file "~/.guix-profile/share/emacs/site-lisp/site-start.d/pg-init.el")
> to init.el as a workaround.
>
> Anyways, this should fix proof-general to work with the current version
> of coq at least and add some more newer niceties in recent versions.

Thanks!  I applied both patches, and also added a proper commit message
for the first one (mention the changes to the various fields).

I also added a git-file-name for the first patch as suggested by 'guix
lint'.

[signature.asc (application/pgp-signature, inline)]

Previous Next

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