[Top][All Lists]

[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


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...


> On Sep 27, 2021, at 10:07, raingloom <> 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?

reply via email to

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