编写coq程序需要一个后台coq库（负责证明过程推导等所有功能，提供coq的所有服务），一个界面编辑器组成。

可以编写coq的开发环境大概有3个：

1、coqIDE

这个是coq官方的，下载地址 Install Coq | The Coq Proof Assistant

里面包含了coq 后台库，还包含了coqIDE（即界面编辑器）。这个coqIDE比较好上手，缺点就是代码提示功能，比较弱，写代码感觉有点费劲，效率低。

我用的是8.5版本，带的coqIDE功能比较正常。但是现在最新的8.15版本，带的coqIDE界面更加美观一些，代码提示等功能还是一样的弱，甚至有些方面还不如8.5版本的coqIDE了，此外，功能还不正常，启动时候竟然提示少库，此外，进入了设置页面，多点几下，软件就卡死了。反正就是不如之前的版本好用。

2、vs code装VSCoq插件

这个比较好用，推荐用这个，因为vscode本身就具有较好的代码提示功能，而且这个插件做得也不错。安装过程如下：

1. 要先安装好coq后台库，这个按照上面方法1，去官方下载下来安装即可。
2. 在侧边栏的“扩展”功能中搜索VSCoq（虽然也有别的关于coq的插件，但是下载量不如这个，所以就安装这个），找到后，安装即可
3. 打开该插件的“扩展设置”页面，将Coqtop:Bin Path里面填入我们coq后台库的路径即可
   
4. 因为vs code不像coqIDE提供工具栏，可以直接按钮点击上一步，下一步等运行控制功能，而是通过快捷键方式了。查看快捷键的方式就是，VSCoq插件的“扩展设置”页面也会介绍一些，但是这个不全。我们新建一个xx.v的coq文件，按F1，即可打开命令搜索栏，然后输入 coq:，即可看到所有的coq控制快捷键，其实就那么几个功能而已，现在列举如下：
   1. 上一步：                  alt+上箭头
   2. 下一步：                  alt+下箭头
   3. 运行到光标处：       alt+右箭头
   4. 运行到最后一行：    alt+end
   5. 回到第一行：           alt+home
   6. 中断运行：               ctrl+alt+`

         还有几个其它命令，自己看看吧，其实右键菜单，也显示了这几个的。

3、emacs装ProofGeneral插件

这个本身是在Linux环境下用的，但是windows上也可以。这个是对于高手用的，因为不熟练的人，用emacs本身都非常费劲（甚至都不能用鼠标，就是文本行+快捷键），这个很多很多都需要自己配置，快捷键什么的，得记好久好久。当然，自己用了几十年，非常熟练了，配置得很适合自己，那么emacs编码效率就会非常高了。

ProofGeneral插件网址：

GitHub - ProofGeneral/PG: This repo is the new home of Proof General

这个比较难配，然后有人搞出来个 company-coq 插件，这个是对ProofGeneral的再次打包，看介绍，好像代码提示功能很强，但是仍然是基于emacs的，所以一般人还是驾驭不了。

官网：GitHub - cpitclaudel/company-coq: A Coq IDE build on top of Proof General's Coq mode

其它的介绍博客

https://www.5axxw.com/wiki/content/heselk

由于emacs比较难用，然后有人说可以搞个 Spacemacs 什么的，这个我没有仔细研究过了 https://www.jianshu.com/p/71a2820cf9a1