Re: Major mode for coq

[Heime <heimeborgia@protonmail.com>]

On Monday, May 6th, 2024 at 4:59 AM, Philip Kaludercic <philipk@posteo.net> wrote:

> Heime heimeborgia@protonmail.com writes:
> 
> > Sent with Proton Mail secure email.
> > 
> > On Monday, May 6th, 2024 at 1:51 AM, Stefan Monnier via Users list for
> > the GNU Emacs text editor help-gnu-emacs@gnu.org wrote:
> > 
> > > > Is there any major mode for coq formal proof management system files ?
> > > 
> > > I don't know what you mean by "system files", but there's a coq-mode as
> > > part of Proof-General (available in NonGNU ELPA). - Stefan
> > 
> > Right. But I was hoping to see something that we are all familiar with.
> > Open the file with a coq-mode without the interface of "Proof General".
> > Just see some highlighting and some tools for the file type, as one gets
> > with elisp, c, and fortran. Currently the language highlighting only
> > gets activated as a proof general feature. It goes much beyond just showing
> > the contents of the file.
> 
> 
> Proof-general includes a coq-mode, and there is a user option
> `coq-use-pg' that can disable integration with Proof General (but
> usually you don't want that, since having the interaction with the Coq
> system is what makes working with Coq in Emacs interesting).
> 
> --
> Philip Kaludercic on icterid

It would still be good to open a file with the highlighting before people
have installed "Proof General".  "Proof General"  could then use that mode
and do the other stuff as well.  I could be more productive if I can change
the files without the details of "Proof General".