Major mode for coq

Major mode for coq

[Heime]

Is there any major mode for coq formal proof management system files ?

Re: Major mode for coq

[Stefan Monnier via Users list for the GNU Emacs text editor]

> 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

Re: Major mode for coq

[Heime]

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.

Re: Major mode for coq

[Philip Kaludercic]

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

Re: Major mode for coq

[Heime]

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

Re: Major mode for coq

[Heime]

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.

Re: Major mode for coq

[Stefan Monnier]

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

My crystal ball tells me you're looking for

    (setq proof-splash-enable nil)


- Stefan

Re: Major mode for coq

[Heime]

Sent with Proton Mail secure email.

On Monday, May 6th, 2024 at 6:14 AM, Stefan Monnier <monnier@iro.umontreal.ca> wrote:

> > 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".
> 
> 
> My crystal ball tells me you're looking for
> 
> (setq proof-splash-enable nil)
> 

Would it be difficult to separate the coq-mode from the Proof General 
IDE functionality ?
 
> - Stefan

Re: Major mode for coq

[Heime]

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

> 
> 
> 
> 
> 
> Sent with Proton Mail secure email.
> 
> 
> On Monday, May 6th, 2024 at 6:14 AM, Stefan Monnier monnier@iro.umontreal.ca wrote:
> 
> > > 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".
> > 
> > My crystal ball tells me you're looking for
> > 
> > (setq proof-splash-enable nil)
> 
> 
> Would it be difficult to separate the coq-mode from the Proof General
> IDE functionality ?
> 
> > - Stefan

Currently I have an old machine with an old system that I cannot install
coq in it, but I still want to view and change the files like normal .el,
.c, and the like.

Re: Major mode for coq

[Heime]

Sent with Proton Mail secure email.

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

> On Monday, May 6th, 2024 at 6:57 AM, Heime heimeborgia@protonmail.com wrote:
> 
> > Sent with Proton Mail secure email.
> > 
> > On Monday, May 6th, 2024 at 6:14 AM, Stefan Monnier monnier@iro.umontreal.ca wrote:
> > 
> > > > 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".
> > > 
> > > My crystal ball tells me you're looking for
> > > 
> > > (setq proof-splash-enable nil)
> > 
> > Would it be difficult to separate the coq-mode from the Proof General
> > IDE functionality ?
> > 
> > > - Stefan
> 
> 
> Currently I have an old machine with an old system that I cannot install
> coq in it, but I still want to view and change the files like normal .el,
> .c, and the like.

Currently the .v files load up in verilog-mode.

Re: Major mode for coq

[Philip Kaludercic]

Heime <heimeborgia@protonmail.com> writes:

> Sent with Proton Mail secure email.
>
> On Monday, May 6th, 2024 at 6:14 AM, Stefan Monnier <monnier@iro.umontreal.ca> wrote:
>
>> > 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".
>> 
>> 
>> My crystal ball tells me you're looking for
>> 
>> (setq proof-splash-enable nil)
>> 
>
> Would it be difficult to separate the coq-mode from the Proof General 
> IDE functionality ?

As mentioned in my above message, that is what `coq-use-pg' (or rather
the opposite).  So together with Stefan's suggestion, you want to set

  (setq proof-splash-enable nil
        coq-use-pg nil)

-- 
	Philip Kaludercic on peregrine

Re: Major mode for coq

[Heime]

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

> Sent with Proton Mail secure email.
> 
> On Monday, May 6th, 2024 at 7:08 AM, Heime heimeborgia@protonmail.com wrote:
> 
> > On Monday, May 6th, 2024 at 6:57 AM, Heime heimeborgia@protonmail.com wrote:
> > 
> > > Sent with Proton Mail secure email.
> > > 
> > > On Monday, May 6th, 2024 at 6:14 AM, Stefan Monnier monnier@iro.umontreal.ca wrote:
> > > 
> > > > > 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".
> > > > 
> > > > My crystal ball tells me you're looking for
> > > > 
> > > > (setq proof-splash-enable nil)
> > > 
> > > Would it be difficult to separate the coq-mode from the Proof General
> > > IDE functionality ?
> > > 
> > > > - Stefan
> > 
> > Currently I have an old machine with an old system that I cannot install
> > coq in it, but I still want to view and change the files like normal .el,
> > .c, and the like.
> 
> 
> Currently the .v files load up in verilog-mode.

I current have the following function, but I do not get Proof General
to load when opening a .v file.

(defun provador (actm)
  "Add the directory paths and load coq features."

  (setq actm (or actm 'go))

  (unless (eq 'hold actm)
    (add-to-list 'load-path "~/contrib/company-coq")
    (require 'company-coq)

    (add-to-list 'load-path "~/contrib/proof-general")
    (require 'proof-general)) )

Re: Major mode for coq

[Stefan Monnier]

> Currently I have an old machine with an old system that I cannot install
> coq in it, but I still want to view and change the files like normal .el,
> .c, and the like. 

I have not followed Proof-General closely enough to be sure, but in the
past, opening a Coq file did not launch a `coq` process (only
subsequent PG commands would do so), so that should work fine.
If not, file a bug report against Proof-General.


        Stefan

Re: Major mode for coq

[Heime]

Sent with Proton Mail secure email.

On Monday, May 6th, 2024 at 7:59 AM, Stefan Monnier <monnier@iro.umontreal.ca> wrote:

> > Currently I have an old machine with an old system that I cannot install
> > coq in it, but I still want to view and change the files like normal .el,
> > .c, and the like.
> 
> 
> I have not followed Proof-General closely enough to be sure, but in the
> past, opening a Coq file did not launch a `coq` process (only
> subsequent PG commands would do so), so that should work fine.
> If not, file a bug report against Proof-General. - Stefan

I still think emacs should provide a coq major-mode for highlighting.

Re: Major mode for coq

[Stefan Monnier]

> I still think emacs should provide a coq major-mode for highlighting.

Patches welcome,


        Stefan

Re: Major mode for coq

[Heime]

Sent with Proton Mail secure email.

On Monday, May 6th, 2024 at 8:13 AM, Stefan Monnier <monnier@iro.umontreal.ca> wrote:

> > I still think emacs should provide a coq major-mode for highlighting.
> 
> 
> Patches welcome, - Stefan

Message Understood.  ;)