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

**From**: |
Yasuaki Kudo |

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

**Date**: |
Mon, 27 Sep 2021 11:09:32 +0900 |

Hi!
I did this just last night so let me tell you what I did.
I installed using guix install command emacs, coq and proof-general but in the
end I probably could not observe that proof-general was working from the Guix
installation so I followed the standard installation instruction on Proof
General homepage , which is an instruction of how to do so with MELPA. ðŸ˜„
I didn't spend much time examining whether proof-genetal from Guix was working
or not...
-Yasu
>* On Sep 27, 2021, at 10:07, raingloom <raingloom@riseup.net> wrote:*
>* *
>* ï»¿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?*
>* *