GNU bug report logs - #51755
[PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)

Previous Next

Package: guix-patches;

Reported by: zimoun <zimon.toutoune <at> gmail.com>

Date: Wed, 10 Nov 2021 19:35:02 UTC

Severity: normal

Tags: patch

Done: Nicolas Goaziou <mail <at> nicolasgoaziou.fr>

Bug is archived. No further changes may be made.

Full log


View this message in rfc822 format

From: zimoun <zimon.toutoune <at> gmail.com>
To: 51755 <at> debbugs.gnu.org
Cc: Julien Lepiller <julien <at> lepiller.eu>, Nicolas Goaziou <mail <at> nicolasgoaziou.fr>
Subject: [bug#51755] [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)
Date: Fri, 19 Nov 2021 13:27:13 +0100
Hi Coq or Emacs reviewers,

On Wed, 10 Nov 2021 at 20:26, zimoun <zimon.toutoune <at> gmail.com> wrote:

> This is a follow-up of bug#46016 [1] and I think close it.
>
> Now, it is possible to use ProofGeneral as any other Emacs packages.  For
> instance,
>
>    guix shell emacs proof-general coq
>    emacs foo.v
>
> For now, the dependency of 'coq' is removed as with many Emacs packages.
> Other said, the user has to provide such dependency.  IMHO, it is the spirit
> of such package where the 'prover' is let to the user (several are more or
> less supported, see doc [2]).
>
> 1: <http://issues.guix.gnu.org/issue/46016>
> 2: <https://proofgeneral.github.io/doc/master/userman/Introducing-Proof-General/#Supported-proof-assistants>

Friendly ping. :-)


Cheers,
simon




This bug report was last modified 3 years and 218 days ago.

Previous Next


GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.