GNU bug report logs - #48947
[PATCH] gnu: proof-general: Update to 4.4-0.bc86736.

Previous Next

Full log

Message #11 received at 48947 <at> debbugs.gnu.org (full text, mbox):

From: Xinglu Chen <public <at> yoctocell.xyz>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 48947 <at> debbugs.gnu.org
Subject: Re: [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736.
Date: Fri, 11 Jun 2021 11:05:02 +0200

[Message part 1 (text/plain, inline)]

On Thu, Jun 10 2021, zimoun wrote:

> Hi,
>
> On Thu, 10 Jun 2021 at 15:31, Xinglu Chen <public <at> 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).

[signature.asc (application/pgp-signature, inline)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.