[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
## how to use Proof General?

**From**: |
raingloom |

**Subject**: |
how to use Proof General? |

**Date**: |
Sun, 26 Sep 2021 23:02:58 +0000 |

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?

**how to use Proof General?**,
*raingloom* **<=**