[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: how to use Proof General?
From: |
raingloom |
Subject: |
Re: how to use Proof General? |
Date: |
Tue, 30 Nov 2021 03:31:23 +0100 |
On Mon, 29 Nov 2021 09:41:52 +0100
zimoun <zimon.toutoune@gmail.com> wrote:
> Hi,
>
> On Mon, 27 Sep 2021 at 11:09, Yasuaki Kudo <yasu@yasuaki.com> wrote:
> >> On Sep 27, 2021, at 10:07, raingloom <raingloom@riseup.net> wrote:
> >>
>
> >> 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.
>
> Now, it should work as expected. Could you confirm that
>
> guix shell emacs coq proof-general -- emacs scratchpad.v
>
> is correctly starting ProofGeneral? Adding other Emacs packages as
> your taste (emacs-company-coq, etc.) as well.
>
>
> Cheers,
> simon
>
I tried it a few days ago, as far as I can tell, everything is working!
Thanks!