GNU bug report logs - #38433
ProofGeneral and Emacs sharing a profile

Previous Next

Package: guix;

Reported by: Brett Gilio <brettg <at> posteo.net>

Date: Sat, 30 Nov 2019 03:39:02 UTC

Severity: normal

Done: zimoun <zimon.toutoune <at> gmail.com>

Bug is archived. No further changes may be made.

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

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

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to bug-guix <at> gnu.org:
bug#38433; Package guix. (Sat, 30 Nov 2019 03:39:02 GMT) Full text and rfc822 format available.

Acknowledgement sent to Brett Gilio <brettg <at> posteo.net>:
New bug report received and forwarded. Copy sent to bug-guix <at> gnu.org. (Sat, 30 Nov 2019 03:39:02 GMT) Full text and rfc822 format available.

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

From: Brett Gilio <brettg <at> posteo.net>
To: bug-guix <at> gnu.org
Subject: ProofGeneral and Emacs sharing a profile
Date: Fri, 29 Nov 2019 21:38:50 -0600
There is an issue after the EMACSLOADPATH change that creates a problem
when `proof-general` and `emacs` share a profile. This issue can be
replicated as follows:

--8<---------------cut here---------------start------------->8---
$ guix environment --ad-hoc proof-general emacs
--8<---------------cut here---------------end--------------->8---

When you launch the client of either of these after spinning up the
environment, you are prompted with this from the *Messages* buffer.

--8<---------------cut here---------------start------------->8---
Loading /gnu/store/bi3yv2q84fpyq1ym9z8rpa8hv2xhz1bf-profile/share/emacs/site-lisp/ProofGeneral/generic/proof-autoloads...done
Loading /gnu/store/bi3yv2q84fpyq1ym9z8rpa8hv2xhz1bf-profile/share/emacs/site-lisp/ProofGeneral/generic/proof-autoloads...
byte-code: Already loaded
--8<---------------cut here---------------end--------------->8---

Loading stops without an error message at this point, failing to
complete the initialization process.

I can probably figure out this issue, but I am currently drained for
time, so I am reporting it here. If nobody else gets to it before I do,
I will come back to it.

Thanks!

-- 
Brett M. Gilio
https://git.sr.ht/~brettgilio/




Information forwarded to bug-guix <at> gnu.org:
bug#38433; Package guix. (Sat, 30 Nov 2019 07:43:02 GMT) Full text and rfc822 format available.

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: bug-guix <at> gnu.org,Brett Gilio <brettg <at> posteo.net>,38433 <at> debbugs.gnu.org
Subject: Re: bug#38433: ProofGeneral and Emacs sharing a profile
Date: Sat, 30 Nov 2019 08:42:29 +0100
Le 30 novembre 2019 04:38:50 GMT+01:00, Brett Gilio <brettg <at> posteo.net> a écrit :
>
>There is an issue after the EMACSLOADPATH change that creates a problem
>when `proof-general` and `emacs` share a profile. This issue can be
>replicated as follows:
>
>--8<---------------cut here---------------start------------->8---
>$ guix environment --ad-hoc proof-general emacs
>--8<---------------cut here---------------end--------------->8---
>
>When you launch the client of either of these after spinning up the
>environment, you are prompted with this from the *Messages* buffer.
>
>--8<---------------cut here---------------start------------->8---
>Loading
>/gnu/store/bi3yv2q84fpyq1ym9z8rpa8hv2xhz1bf-profile/share/emacs/site-lisp/ProofGeneral/generic/proof-autoloads...done
>Loading
>/gnu/store/bi3yv2q84fpyq1ym9z8rpa8hv2xhz1bf-profile/share/emacs/site-lisp/ProofGeneral/generic/proof-autoloads...
>byte-code: Already loaded
>--8<---------------cut here---------------end--------------->8---
>
>Loading stops without an error message at this point, failing to
>complete the initialization process.
>
>I can probably figure out this issue, but I am currently drained for
>time, so I am reporting it here. If nobody else gets to it before I do,
>I will come back to it.
>
>Thanks!

It could pg's fault. We have a vcry old vcrsion that is probably completely broken. I tried to package a newer version, but being not an emacs user it was too hard for me. Maybe someone can give it a try (you? :p)




Information forwarded to bug-guix <at> gnu.org:
bug#38433; Package guix. (Sat, 30 Nov 2019 07:43:02 GMT) Full text and rfc822 format available.

Information forwarded to bug-guix <at> gnu.org:
bug#38433; Package guix. (Sat, 30 Nov 2019 22:13:02 GMT) Full text and rfc822 format available.

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

From: Brett Gilio <brettg <at> posteo.net>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: bug-guix <at> gnu.org, 38433 <at> debbugs.gnu.org
Subject: Re: bug#38433: ProofGeneral and Emacs sharing a profile
Date: Sat, 30 Nov 2019 16:12:44 -0600
Julien Lepiller <julien <at> lepiller.eu> writes:

> It could pg's fault. We have a vcry old vcrsion that is probably
> completely broken. I tried to package a newer version, but being not
> an emacs user it was too hard for me. Maybe someone can give it a try
> (you? :p)

I have began working updating the package. :)

A lot of things have changed between the current version in Guix, and
the latest upstream. So I want to be thorough. Will update on the status
and send a patch soon.

-- 
Brett M. Gilio
https://git.sr.ht/~brettgilio/




Information forwarded to bug-guix <at> gnu.org:
bug#38433; Package guix. (Sat, 30 Nov 2019 22:13:02 GMT) Full text and rfc822 format available.

Reply sent to zimoun <zimon.toutoune <at> gmail.com>:
You have taken responsibility. (Mon, 29 Nov 2021 08:59:01 GMT) Full text and rfc822 format available.

Notification sent to Brett Gilio <brettg <at> posteo.net>:
bug acknowledged by developer. (Mon, 29 Nov 2021 08:59:02 GMT) Full text and rfc822 format available.

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

From: zimoun <zimon.toutoune <at> gmail.com>
To: Brett Gilio <brettg <at> posteo.net>
Cc: 38433-done <at> debbugs.gnu.org
Subject: Re: bug#38433: ProofGeneral and Emacs sharing a profile
Date: Mon, 29 Nov 2021 09:57:20 +0100
Hi,

On Fri, 29 Nov 2019 at 21:38, Brett Gilio <brettg <at> posteo.net> wrote:
> There is an issue after the EMACSLOADPATH change that creates a problem
> when `proof-general` and `emacs` share a profile. This issue can be
> replicated as follows:
>
> $ guix environment --ad-hoc proof-general emacs
>
>
> When you launch the client of either of these after spinning up the
> environment, you are prompted with this from the *Messages* buffer.
>
> Loading /gnu/store/bi3yv2q84fpyq1ym9z8rpa8hv2xhz1bf-profile/share/emacs/site-lisp/ProofGeneral/generic/proof-autoloads...done
> Loading /gnu/store/bi3yv2q84fpyq1ym9z8rpa8hv2xhz1bf-profile/share/emacs/site-lisp/ProofGeneral/generic/proof-autoloads...
> byte-code: Already loaded
>
> Loading stops without an error message at this point, failing to
> complete the initialization process.

Commit cb296dfa2e2938d18ae0ee347bed0cc94bc79cf8 fixes this issue.  The
command,

    guix shell -C emacs proof-general -E TERM \
         --  emacs foo.v

leads to this ’*Messages*’:

--8<---------------cut here---------------start------------->8---
Loading /gnu/store/wbr97j47i3z6m19gycm6ryb6k0xdlg3i-proof-general-4.4-0.bc86736\
/share/emacs/site-lisp/ProofGeneral/proof-general-autoloads.el (source)...done
For information about GNU Emacs and the GNU system, type C-h C-a.
(New file)
Coq project file not detected.
--8<---------------cut here---------------end--------------->8---

Therefore, closing.

Feel free to reopen if I miss something or misunderstand your report.


Cheers,
simon




bug archived. Request was from Debbugs Internal Request <help-debbugs <at> gnu.org> to internal_control <at> debbugs.gnu.org. (Mon, 27 Dec 2021 12:24:04 GMT) Full text and rfc822 format available.

This bug report was last modified 2 years and 82 days ago.

Previous Next


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