Re: how to use Proof General?

[raingloom]

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!