[Top][All Lists]

[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


On Mon, 27 Sep 2021 at 11:09, Yasuaki Kudo <> wrote:
>> On Sep 27, 2021, at 10:07, raingloom <> 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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]