On Thu, Jun 10 2021, zimoun wrote:

> Hi,
>
> On Thu, 10 Jun 2021 at 15:31, Xinglu Chen <public@yoctocell.xyz> wrote:
>>
>> There hasn’t been a new release since 2016 and there has been more than 450
>> new commits since then.
>
> Cool!
>
> Does this patch fix the bug#46016?
>
> <http://issues.guix.gnu.org/issue/46016>

I didn’t know about this bug report, but I did notice that Emacs wasn’t
able to load the Elisp files (M-x coq-mode didn’t work).

Proof General generates a pg-init.el file in
/path/to/guix-profile/share/emacs/site-lisp/ProofGeneral/site-start.d,
Emacs isn’t able to find that file, so doing (require 'proof-site)
doesn’t work.

Relevant part of the Makefile

--8<---------------cut here---------------start------------->8---
ELISPP=share/${EMACS}/site-lisp/ProofGeneral
ELISP_START=${PREFIX}/share/${EMACS}/site-lisp/site-start.d

[...]

install-init:
	mkdir -p ${ELISP_START}
	echo ';;; pg-init.el --- setup for Proof General' > ${ELISP_START}/pg-init.el
	echo "(setq load-path (append load-path '(\"${DEST_ELISP}/generic\")))" >> ${ELISP_START}/pg-init.el
	echo "(require 'proof-site)" >> ${ELISP_START}/pg-init.el
--8<---------------cut here---------------end--------------->8---

With this patch, I set the ELISP_START variable to the same value os
ELISPP, now the pg-init.el file ends up in the ProofGeneral directory,
and Emacs is now able to find it.  Doing (require 'proof-site) worked,
and M-x coq-mode created a splash screen, so it seems to work (I just
starting looking into Coq).