Emacs proof-general

[pinoaffe <pinoaffe@gmail.com>]

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