Hi, On Tue, 06 Dec 2022 at 10:38, pinoaffe <pinoa...@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