how to use Proof General?

how to use Proof General?

[raingloom]

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?

Re: how to use Proof General?

[Yasuaki Kudo]

Hi!

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

-Yasu



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

Re: how to use Proof General?

[zimoun]

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?

[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!

Re: how to use Proof General?

[zimoun]

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