mbox series

[bug#51755,0/1] Fix ProofGeneral (emacs front-end for Coq)

Message ID 20211110192622.368232-1-zimon.toutoune@gmail.com
Headers show
Series Fix ProofGeneral (emacs front-end for Coq) | expand

Message

Simon Tournier Nov. 10, 2021, 7:26 p.m. UTC 
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

Comments

Simon Tournier Nov. 19, 2021, 12:27 p.m. UTC | #1 
Hi Coq or Emacs reviewers,

On Wed, 10 Nov 2021 at 20:26, zimoun <zimon.toutoune@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