The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

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

On Thu, Oct 18, 2018, 12:54 PM Xuanrui Qi <xqi01 AT cs.tufts.edu> wrote:

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

Email: xqi01 AT cs.tufts.edu

On Thu, 2018-10-18 at 12:12 -0700, Talia Ringer wrote:
> 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