* Major mode for coq @ 2024-05-05 3:12 Heime 2024-05-05 13:51 ` Stefan Monnier via Users list for the GNU Emacs text editor 0 siblings, 1 reply; 16+ messages in thread From: Heime @ 2024-05-05 3:12 UTC (permalink / raw) To: Heime via Users list for the GNU Emacs text editor Is there any major mode for coq formal proof management system files ? ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 3:12 Major mode for coq Heime @ 2024-05-05 13:51 ` Stefan Monnier via Users list for the GNU Emacs text editor 2024-05-05 16:43 ` Heime 0 siblings, 1 reply; 16+ messages in thread From: Stefan Monnier via Users list for the GNU Emacs text editor @ 2024-05-05 13:51 UTC (permalink / raw) To: help-gnu-emacs > 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 13:51 ` Stefan Monnier via Users list for the GNU Emacs text editor @ 2024-05-05 16:43 ` Heime 2024-05-05 16:59 ` Philip Kaludercic 0 siblings, 1 reply; 16+ messages in thread From: Heime @ 2024-05-05 16:43 UTC (permalink / raw) To: Stefan Monnier; +Cc: help-gnu-emacs 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 16:43 ` Heime @ 2024-05-05 16:59 ` Philip Kaludercic 2024-05-05 17:10 ` Heime 0 siblings, 1 reply; 16+ messages in thread From: Philip Kaludercic @ 2024-05-05 16:59 UTC (permalink / raw) To: Heime; +Cc: Stefan Monnier, help-gnu-emacs 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 16:59 ` Philip Kaludercic @ 2024-05-05 17:10 ` Heime 2024-05-05 17:31 ` Heime 2024-05-05 18:14 ` Stefan Monnier 0 siblings, 2 replies; 16+ messages in thread From: Heime @ 2024-05-05 17:10 UTC (permalink / raw) To: Philip Kaludercic; +Cc: Stefan Monnier, help-gnu-emacs 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". ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 17:10 ` Heime @ 2024-05-05 17:31 ` Heime 2024-05-05 18:14 ` Stefan Monnier 1 sibling, 0 replies; 16+ messages in thread From: Heime @ 2024-05-05 17:31 UTC (permalink / raw) To: Heime; +Cc: Philip Kaludercic, Stefan Monnier, help-gnu-emacs 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 17:10 ` Heime 2024-05-05 17:31 ` Heime @ 2024-05-05 18:14 ` Stefan Monnier 2024-05-05 18:57 ` Heime 1 sibling, 1 reply; 16+ messages in thread From: Stefan Monnier @ 2024-05-05 18:14 UTC (permalink / raw) To: Heime; +Cc: Philip Kaludercic, help-gnu-emacs > 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 18:14 ` Stefan Monnier @ 2024-05-05 18:57 ` Heime 2024-05-05 19:08 ` Heime 2024-05-05 19:16 ` Philip Kaludercic 0 siblings, 2 replies; 16+ messages in thread From: Heime @ 2024-05-05 18:57 UTC (permalink / raw) To: Stefan Monnier; +Cc: Philip Kaludercic, help-gnu-emacs 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 18:57 ` Heime @ 2024-05-05 19:08 ` Heime 2024-05-05 19:12 ` Heime 2024-05-05 19:59 ` Stefan Monnier 2024-05-05 19:16 ` Philip Kaludercic 1 sibling, 2 replies; 16+ messages in thread From: Heime @ 2024-05-05 19:08 UTC (permalink / raw) To: Heime; +Cc: Stefan Monnier, Philip Kaludercic, help-gnu-emacs 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 19:08 ` Heime @ 2024-05-05 19:12 ` Heime 2024-05-05 19:18 ` Heime 2024-05-05 19:59 ` Stefan Monnier 1 sibling, 1 reply; 16+ messages in thread From: Heime @ 2024-05-05 19:12 UTC (permalink / raw) To: Heime; +Cc: Stefan Monnier, Philip Kaludercic, help-gnu-emacs 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 19:12 ` Heime @ 2024-05-05 19:18 ` Heime 0 siblings, 0 replies; 16+ messages in thread From: Heime @ 2024-05-05 19:18 UTC (permalink / raw) To: Heime; +Cc: Stefan Monnier, Philip Kaludercic, help-gnu-emacs 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)) ) ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 19:08 ` Heime 2024-05-05 19:12 ` Heime @ 2024-05-05 19:59 ` Stefan Monnier 2024-05-05 20:11 ` Heime 1 sibling, 1 reply; 16+ messages in thread From: Stefan Monnier @ 2024-05-05 19:59 UTC (permalink / raw) To: Heime; +Cc: Philip Kaludercic, help-gnu-emacs > 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 19:59 ` Stefan Monnier @ 2024-05-05 20:11 ` Heime 2024-05-05 20:13 ` Stefan Monnier 0 siblings, 1 reply; 16+ messages in thread From: Heime @ 2024-05-05 20:11 UTC (permalink / raw) To: Stefan Monnier; +Cc: Philip Kaludercic, help-gnu-emacs 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 20:11 ` Heime @ 2024-05-05 20:13 ` Stefan Monnier 2024-05-05 20:52 ` Heime 0 siblings, 1 reply; 16+ messages in thread From: Stefan Monnier @ 2024-05-05 20:13 UTC (permalink / raw) To: Heime; +Cc: Philip Kaludercic, help-gnu-emacs > I still think emacs should provide a coq major-mode for highlighting. Patches welcome, Stefan ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 20:13 ` Stefan Monnier @ 2024-05-05 20:52 ` Heime 0 siblings, 0 replies; 16+ messages in thread From: Heime @ 2024-05-05 20:52 UTC (permalink / raw) To: Stefan Monnier; +Cc: Philip Kaludercic, help-gnu-emacs 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. ;) ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Major mode for coq 2024-05-05 18:57 ` Heime 2024-05-05 19:08 ` Heime @ 2024-05-05 19:16 ` Philip Kaludercic 1 sibling, 0 replies; 16+ messages in thread From: Philip Kaludercic @ 2024-05-05 19:16 UTC (permalink / raw) To: Heime; +Cc: Stefan Monnier, help-gnu-emacs 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 ^ permalink raw reply [flat|nested] 16+ messages in thread
end of thread, other threads:[~2024-05-05 20:52 UTC | newest] Thread overview: 16+ messages (download: mbox.gz follow: Atom feed -- links below jump to the message on this page -- 2024-05-05 3:12 Major mode for coq Heime 2024-05-05 13:51 ` Stefan Monnier via Users list for the GNU Emacs text editor 2024-05-05 16:43 ` Heime 2024-05-05 16:59 ` Philip Kaludercic 2024-05-05 17:10 ` Heime 2024-05-05 17:31 ` Heime 2024-05-05 18:14 ` Stefan Monnier 2024-05-05 18:57 ` Heime 2024-05-05 19:08 ` Heime 2024-05-05 19:12 ` Heime 2024-05-05 19:18 ` Heime 2024-05-05 19:59 ` Stefan Monnier 2024-05-05 20:11 ` Heime 2024-05-05 20:13 ` Stefan Monnier 2024-05-05 20:52 ` Heime 2024-05-05 19:16 ` Philip Kaludercic
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).