[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: how to use Proof General?
From: |
zimoun |
Subject: |
Re: how to use Proof General? |
Date: |
Mon, 29 Nov 2021 09:41:52 +0100 |
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
- Re: how to use Proof General?,
zimoun <=