[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, 27 Sep 2021 13:56:36 +0200 |
Hi,
On Mon, 27 Sept 2021 at 03:08, raingloom <raingloom@riseup.net> 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?
You might be interested by:
<http://issues.guix.gnu.org/issue/46016>
explaining that there is a bug in the default config of the Emacs
front-end of ProofGeneral.
All the best,
simon