首页 > 编程语言 >coq程序编写好用的IDE推荐

coq程序编写好用的IDE推荐

时间:2022-11-03 23:08:19浏览次数:74  
标签:coq 插件 快捷键 coqIDE emacs alt IDE 好用


编写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​

 

标签:coq,插件,快捷键,coqIDE,emacs,alt,IDE,好用
From: https://blog.51cto.com/u_13682052/5821295

相关文章

  • idea 创建maven项目
    一.版本相关介绍工具:idea2022.2.2apache-maven-3.8.1注意:文件夹尽量不掺杂中文,空格等特殊字符,使用纯英文方式.二.idea端配置File--Settings--"maven"--.........
  • C++17 The Complete Guide 电子书 pdf
    作者:[德]NicolaiM·Josuttis 链接:C++17TheCompleteGuide ......
  • IDEA快捷键
    【常规】Ctrl+Shift+Enter,语句完成“!”,否定完成,输入表达式时按“!”键Ctrl+E,最近的文件Ctrl+Shift+E,最近更改的文件Shift+Click,可以关闭文件Ctrl+[ OR],可以跑到......
  • IDEA中jetty和tomcat的启动
    1.jetty的启动1.1端口在pom.xml中写定的情况        启动成功:  在浏览器中查看一下:成功  1.2端口不在pom.xml中写定,可以在(EditConfiguration......
  • IDEA翻译插件Translation失效
     这是因为dns无法解析google的域名,所以在hosts文件中配置如下配置即可172.253.124.90translate.googleapis.com配置后,翻译成功 ......
  • IDEA用Java创建删除文件,获取文件相关信息,创建删除目录操作
     目录   一、Java创建文件的三种方式二、Java删除文件三、Java获取文件相关信息四、创建删除目录操作五、Java删除目......
  • IDEA调出maven项目窗口
    IDEA调出maven项目窗口方法一(WSG:实测可以)1、在IDEA中,同时按下Ctrl+Shift+A键呼出快捷指令栏,并在搜索框中输入Maven2、点击AddMavenProjects3、选择项目中的pom.xml文件4......
  • 关于java.lang.IllegalArgumentException: Unknown URL content://com.example.databa
    在学习《Android第一行代码》第八章的ProviderTest项目的时候,运行之后点击“AddToBook”按钮,出现如下问题:java.lang.IllegalArgumentException:UnknownURLcontent://......
  • 清除 idea 中 xml 文件的黄色区域
    我们在使用IDEA编写MyBatis的xml文件时,会发现出现一大片的黄色背景提示,每次编写代码的时候都感觉很突兀,所以在这里说下如何解决这个问题。设置->编辑器->代......
  • idea插件Tranlation配置有道搜索引擎
    idea配置有道翻译引擎一、更换翻译引擎原因由于Google在2022年9月末宣布关闭GoogleTranslate在中国的服务,原本在chrome浏览器和idea上使用的google翻译引擎也不能正常使......