编写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本身就具有较好的代码提示功能,而且这个插件做得也不错。安装过程如下:
- 要先安装好coq后台库,这个按照上面方法1,去官方下载下来安装即可。
- 在侧边栏的“扩展”功能中搜索VSCoq(虽然也有别的关于coq的插件,但是下载量不如这个,所以就安装这个),找到后,安装即可
- 打开该插件的“扩展设置”页面,将Coqtop:Bin Path里面填入我们coq后台库的路径即可
- 因为vs code不像coqIDE提供工具栏,可以直接按钮点击上一步,下一步等运行控制功能,而是通过快捷键方式了。查看快捷键的方式就是,VSCoq插件的“扩展设置”页面也会介绍一些,但是这个不全。我们新建一个xx.v的coq文件,按F1,即可打开命令搜索栏,然后输入 coq:,即可看到所有的coq控制快捷键,其实就那么几个功能而已,现在列举如下:
- 上一步: alt+上箭头
- 下一步: alt+下箭头
- 运行到光标处: alt+右箭头
- 运行到最后一行: alt+end
- 回到第一行: alt+home
- 中断运行: 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
标签:coq,插件,快捷键,coqIDE,emacs,alt,IDE,好用 From: https://blog.51cto.com/u_13682052/5821295