[Coq-Club] Writing extensions/plugins for different Coq IDEs

[Talia Ringer]

Hi all,

I'm looking to write an IDE extension or plugin for proof development in
Coq, and I'm curious if anyone knows where to look to find information on
which IDEs support extensions or plugins, and how to go about writing them.
Examples would be very useful, too. Please let me know if you can point me
toward any of this.

Best,

Talia

[Jim Fehrle]

Hi Talia,
IntelliJ has extensive support for plugins (in Java): https://www.jetbrains.org/intellij/sdk/docs/welcome.html.  The community edition of IntelliJ is free.  (I use the ReasonML plugin, which provide syntax highlighting and structure analysis for OCaml.)  I've used IntelliJ for many years--feel to ask me more about it.
Eclipse: https://www.eclipse.org/pde/

VSCode (open source, derived from Microsoft Visual Studio): https://code.visualstudio.com/docs/extensions/overview
Of course, the interesting questions are how easy each one is to work with and which one best suits your purposes.
Hope this helps.
Jim

From: Talia Ringer <***@cs.washington.edu>
To: Coq-Club <coq-***@inria.fr>
Sent: Thursday, October 18, 2018 12:13 PM
Subject: [Coq-Club] Writing extensions/plugins for different Coq IDEs

Hi all,
I'm looking to write an IDE extension or plugin for proof development in Coq, and I'm curious if anyone knows where to look to find information on which IDEs support extensions or plugins, and how to go about writing them. Examples would be very useful, too. Please let me know if you can point me toward any of this.
Best,
Talia

[Xuanrui Qi]

Hello Talia,

Maybe check out Visual Studio Code and Atom (though neither are exactly
IDEs, although the former is more like an IDE)? VSCode already has an
interactive mode for Isabelle, and Atom a mode for Idris, so it
suggests that a similar mode is possible for Coq. Also, maybe IntelliJ
would work as well?

There are a lot of material on writing VSCode and Atom extensions
online. Here, for example, is the official guide on writing VSCode
extensions: https://code.visualstudio.com/docs/extensions/overview.

Again, this isn't something I'm an expert in, so leaving the rest of
the discussion to other members of the list.

-Ray
--
Xuanrui "Ray" Qi
Department of Computer Science
Tufts University
161 College Ave, Halligan Hall
Medford, MA 02144, USA

Post by Talia Ringer
Hi all,
I'm looking to write an IDE extension or plugin for proof development
in Coq, and I'm curious if anyone knows where to look to find
information on which IDEs support extensions or plugins, and how to
go about writing them. Examples would be very useful, too. Please let
me know if you can point me toward any of this.
Best,
Talia

[Talia Ringer]

Thanks all! To clarify, I'm looking to extend IDEs that already have Coq
support with some useful development tools.

Post by Xuanrui Qi
Hello Talia,
Maybe check out Visual Studio Code and Atom (though neither are exactly
IDEs, although the former is more like an IDE)? VSCode already has an
interactive mode for Isabelle, and Atom a mode for Idris, so it
suggests that a similar mode is possible for Coq. Also, maybe IntelliJ
would work as well?
There are a lot of material on writing VSCode and Atom extensions
online. Here, for example, is the official guide on writing VSCode
extensions: https://code.visualstudio.com/docs/extensions/overview.
Again, this isn't something I'm an expert in, so leaving the rest of
the discussion to other members of the list.
-Ray
--
Xuanrui "Ray" Qi
Department of Computer Science
Tufts University
161 College Ave, Halligan Hall
Medford, MA 02144, USA

Post by Talia Ringer
Hi all,
I'm looking to write an IDE extension or plugin for proof development
in Coq, and I'm curious if anyone knows where to look to find
information on which IDEs support extensions or plugins, and how to
go about writing them. Examples would be very useful, too. Please let
me know if you can point me toward any of this.
Best,
Talia

[Xuanrui Qi]

There seems to be a page on GUI/IDEs for Coq on the Coq wiki:
https://github.com/coq/coq/wiki/Tools. Besides Proof General and
CoqIDE, there are Coq plugins for Eclipse and VS Code.

There should be plenty of resources on how to write/extend Eclipse
and/or VS Code, depending on whether you'd write Java/Scala or
JavaScript/TypeScript...

-Ray
--
Xuanrui "Ray" Qi
Department of Computer Science
Tufts University
161 College Ave, Halligan Hall
Medford, MA 02144, USA

Post by Talia Ringer
Thanks all! To clarify, I'm looking to extend IDEs that already have
Coq support with some useful development tools.

Post by Xuanrui Qi
Hello Talia,
Maybe check out Visual Studio Code and Atom (though neither are exactly
IDEs, although the former is more like an IDE)? VSCode already has an
interactive mode for Isabelle, and Atom a mode for Idris, so it
suggests that a similar mode is possible for Coq. Also, maybe IntelliJ
would work as well?
There are a lot of material on writing VSCode and Atom extensions
online. Here, for example, is the official guide on writing VSCode
extensions: https://code.visualstudio.com/docs/extensions/overview.
Again, this isn't something I'm an expert in, so leaving the rest of
the discussion to other members of the list.
-Ray