Subject: bug#38433: ProofGeneral and Emacs sharing a profile

From: Brett Gilio <[email-masked]>
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/