bug#38433: ProofGeneral and Emacs sharing a profile

[Julien Lepiller <julien@lepiller.eu>]

Le 30 novembre 2019 04:38:50 GMT+01:00, Brett Gilio <brettg@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)