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
