GNU bug report logs -
#38433
ProofGeneral and Emacs sharing a profile
Previous Next
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.
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):
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):
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):
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):
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.