Emacs proof-general

Emacs proof-general

[pinoaffe]

Hi folks,

the proof-general package seems to be broken - I cannot load it from
emacs, even when it is properly installed and in the path. I've tried
requiring proof-general, proof-general-autoloads, and loading it using
use-package.  I think the issue is that proof-general.el is renamed to
proof-general-autoloads.el in the guix package definition, while the
file still ends in `(provide 'proof-general)`.

I don't know why this file is renamed, but I see two possible
resolutions:
- either don't rename proof-general.el, or
- rename it, edit `(provide 'proof-general)`, and optionally add a new file
    proof-general.el so that it can be loaded in the conventional manner.

I've shied away from posting a patch making either of these changes
since I don't understand the reason for the renaming.

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

Kind regards,
pinoaffe

Re: Emacs proof-general

[zimoun]

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