Re: Emacs proof-general

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

Hi,

On Tue, 06 Dec 2022 at 10:38, pinoaffe <pinoaffe@gmail.com> wrote:

> I don't know why this file is renamed,

The explanations are here: :-)

    https://issues.guix.gnu.org/51755#5

or here: :-)

    https://git.savannah.gnu.org/cgit/guix.git/tree/gnu/packages/coq.scm#n217


> Does anyone know what's going on, and how this can be resolved?  (or is
> this just a case of user-error?)

Well, it works for me. ;-)  This,

   guix shell -C emacs proof-general coq -- emacs -q foo.v

correctly starts Proof-General.  Then, depending on what is inside the
file foo.v, say:

    Definition x := 42.
    Print x.

so I start Coq pressing ’C-c C-n’.

Otherwise, I have my Emacs packages under the profile
~/.config/guix/profiles/emacs (containing the packages emacs and
proof-general) and another profile ~/.confi/guix/profiles/compiler
(containing the package coq).  And I do not have any specific Coq or
Proof-General configuration in ~/.config/emacs.


Could you be more specific about what is not working for you?


Cheers,
simon