bug#46016: broken Proof-General (emacs front-end to Coq)

[zimoun]

Hi,

Let instantiate an environment:

  guix environment -C -E TERM \
       --ad-hoc coq proof-general emacs \
       busybox \ 
       -- emacs -q

and then “C-h i m“ list ‘Proof General’ and I can read the manual.
However, there is no ELisp about coq-mode or pg stuff.  Let ’M-x shell’
and then:

--8<---------------cut here---------------start------------->8---
$ ls -aR1 $GUIX_ENVIRONMENT | grep '\.el'
guix-emacs.el
guix-emacs.elc
site-start.el
site-start.elc
--8<---------------cut here---------------end--------------->8---

(The package busybox is for debugging: necessary to be able to run Info
in container, list all files and grep them.) 


Maybe it is related to bug#45781 [1].

1: < https://issues.guix.gnu.org/45781>


All the best,
simon