ProofGeneral and Emacs sharing a profile

  • Done
  • quality assurance status badge
Details
3 participants
  • Brett Gilio
  • Julien Lepiller
  • zimoun
Owner
unassigned
Submitted by
Brett Gilio
Severity
normal

Debbugs page

Brett Gilio wrote 5 years ago
(address . bug-guix@gnu.org)
87zhget4mt.fsf@posteo.net
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:

Toggle snippet (3 lines)
$ 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.

Toggle snippet (5 lines)
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.

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
Julien Lepiller wrote 5 years ago
7899596C-6400-4A84-8546-5A5F2853AA07@lepiller.eu
Le 30 novembre 2019 04:38:50 GMT+01:00, Brett Gilio <brettg@posteo.net> a écrit :
Toggle quote (29 lines)
>
>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)
Brett Gilio wrote 5 years ago
(name . Julien Lepiller)(address . julien@lepiller.eu)
87mucdm2sj.fsf@posteo.net
Julien Lepiller <julien@lepiller.eu> writes:

Toggle quote (5 lines)
> 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
zimoun wrote 3 years ago
(name . Brett Gilio)(address . brettg@posteo.net)(address . 38433-done@debbugs.gnu.org)
86fsrftk3z.fsf@gmail.com
Hi,

On Fri, 29 Nov 2019 at 21:38, Brett Gilio <brettg@posteo.net> wrote:
Toggle quote (17 lines)
> 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*’:

Toggle snippet (7 lines)
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.

Therefore, closing.

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


Cheers,
simon
Closed
?
Your comment

This issue is archived.

To comment on this conversation send an email to 38433@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it
mumi current 38433
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch
You may also tag this issue. See list of standard tags. For example, to set the confirmed and easy tags
mumi command -t +confirmed -t +easy
Or, remove the moreinfo tag and set the help tag
mumi command -t -moreinfo -t +help