What are standard practices for developing Coq code in Atom Editor?

Question

I wanted to develop some Coq code in Atom. I wanted to be able to check my code line by line as usual just like with CoqIDE or emacs proof general. Is there something like that for atom or how do people develop Coq code in Atom editor?

some links:

https://discuss.atom.io/t/is-there-proof-general-for-coq-in-atom/60862

Note: I mostly found syntax hilighting.

ejgallego · Answer 1 · 2018-11-30T02:53:44.310

1

Unfortunately not that I know of; the closest you have is vscoq which even if lagging a bit behind it is on the roadmap to become fully supported again once Coq can speak LSP.

A problem I see with Atom is that its future seems uncertain now that MicroSoft bought GitHub, and indeed, for example it seems to be lacking in LSP support.

edited Nov 30 '18 at 02:53

answered Nov 30 '18 at 02:44

ejgallego

6,709
1
14
29

what is LSP support? – Charlie Parker Nov 30 '18 at 02:47
MS = Miscrosoft – Charlie Parker Nov 30 '18 at 02:47
LSP = Language Server Protocol, it is the standard that VsCode is using to communicate with tools and the one we'd like to adopt in Coq. – ejgallego Nov 30 '18 at 02:54

What are standard practices for developing Coq code in Atom Editor?

1 Answers1