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

Previous Next

Full log

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: guix-patches <at> gnu.org
Cc: zimoun <zimon.toutoune <at> gmail.com>
Subject: [PATCH 0/1] Fix ProofGeneral (emacs front-end for Coq)
Date: Wed, 10 Nov 2021 20:26:22 +0100

Hi,

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

Cheers,
simon



1: <http://issues.guix.gnu.org/issue/46016>
2: <https://proofgeneral.github.io/doc/master/userman/Introducing-Proof-General/#Supported-proof-assistants>


zimoun (1):
  gnu: proof-general: Adjust autoloads for Emacs.

 gnu/packages/coq.scm | 85 +++++++++++++++++++++++---------------------
 1 file changed, 45 insertions(+), 40 deletions(-)


base-commit: 140b486437670ce95cb24a935b58cba52a9dac31
-- 
2.33.1

Previous Next

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