Re: Major mode for coq

[Heime <heimeborgia@protonmail.com>]

On Monday, May 6th, 2024 at 5:10 AM, Heime <heimeborgia@protonmail.com> wrote:

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

If you view the files in github, you get their contents like any programming
langauge, and without any IDE nicieties and special rendering of symbols.