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

[zimoun <zimon.toutoune@gmail.com>]

Hi,

On Thu, 21 Jan 2021 at 12:10, zimoun <zimon.toutoune@gmail.com> wrote:

> Let instantiate an environment:
>
>   guix environment -C -E TERM \
>        --ad-hoc coq proof-general emacs \
>        busybox \ 
>        -- emacs -q
>

[...]

> $ ls -aR1 $GUIX_ENVIRONMENT | grep '\.el'
> guix-emacs.el
> guix-emacs.elc
> site-start.el
> site-start.elc

This command is wrong and shows nothing! :-)

However, note that once Emacs is launched,

 M-: (load “$GUIX_ENVIRONMENT/share/emacs/site-lisp/site-start.d/pg-init.el”)

allows to see the ’ProofGeneral’ front-end; for instance opening a Coq
file and small experiments seem to work.


> Maybe it is related to bug#45781 [1].
>
> 1: < https://issues.guix.gnu.org/45781>

Well, I do not know if it is related.  But what is loaded does not seem
to work as expected.  I mean, I am expecting that all under
’site-lisp/site-start.d/’ are run at start time.


All the best,
simon