Hi! I'm trying to use Proof General with Emacs, but so far I couldn't figure out a way to launch it. Running guix environment `--ad-hoc proof-general emacs coq emacs-company-coq -- emacs scratchpad.v` results in Verilog mode being started and when I try to manually launch coq-mode with M-x, it's not even there.
I'm running packages from a few days ago. Given how many Coq packages we have, I assume someone is in fact using them. Or that at least they worked at some point. Am I missing something obvious? I'm not exactly an Emacs or Coq expert, but so far I haven't had trouble with Emacs modules in ad-hoc environments and I managed to run Coq IDE before. Or is there a bug in how proof-general is packaged?
