正在学习形式语义这门课,需要使用到Coq作为辅助语言进行描述。因此,需要在熟悉Coq语言。然而,直接百度Coq会出现很多奇奇怪怪的结果(Google更准确,但是我在加载自定义库遇到的问题没有直接找到答案),因此特别在这里做个笔记,以备后来查验。

Coq的核心下载地址:https://coq.inria.fr/download,我选择的是Windows下的8.8.1版本。安装之后,记得将安装目录下的bin文件夹(In my case, that is "C:\\Coq\\bin")加入环境变量Path。Coq安装中会自己携带IDE,通常情况下已经够用了,如果有需要,可以考虑Emacs的插件ProofGeneral(项目地址:https://github.com/ProofGeneral/PG),解压之后记得在配置文件.emacs中加入load-file指令加载PG的proof-site.el文件;在VSCode中也有vscoq的插件,安装之后记得加入Coq的bin文件夹地址。

这个时候Coq已经安装完毕,就可以进行相关的操作了。如果需要加载自定义库,记得将.v文件Compile buffer成.vo文件等一系列文件,否则可能出现`Unable to locate library XXX`等问题。

推荐Coq教程:https://softwarefoundations.cis.upenn.edu/current/index.html

学习Coq笔记(一):Windows下安装Coq相关推荐

  1. Memcached学习---(3)Windows 下安装 Memcached

    Windows 下安装 Memcached 官网上并未提供 Memcached 的 Windows 平台安装包,我们可以使用以下链接来下载,你需要根据自己的系统平台及需要的版本号点击对应的链接下载即可 ...

  2. python开发工具及环境配置_python_在windows下安装配置python开发环境及Ulipad开发工具...

    最近开始学习Python,在网上寻找一下比较好的IDE.因为以前用C#做开发的,用Visual Studio作为IDE,鉴于用惯了VS这么强大的IDE,所以对IDE有一定的依赖性. Python的ID ...

  3. 学习笔记(1)centos7 下安装nginx

    学习笔记(1)centos7 下安装nginx 这里我是通过来自nginx.org的nginx软件包进行安装的. 1.首先为centos设置添加nginx的yum存储库 1.通过vi命令创建一个rep ...

  4. MongoDB学习之在Windows下安装MongoDB

    前言:这篇文章主要介绍在Windows下安装MongoDB 首先,第一步,下载Windows版本的MongoDB,其中有Windows 32位和64位的MongoDB下载,下载地址为:MongoDB下 ...

  5. Windows 下安装 CUDA 和 Pytorch 跑深度学习

    Windows 下安装 CUDA 和 Pytorch 跑深度学习 一.安装cuda 11.3 1.1 download cuda 11.3 1.2 双击解压 1.3 测完安装是否成功 二.安装Anac ...

  6. python学习--windows下安装Numpy包的错误:Unable to find vcvarsall.bat

    今天在安装numpy包的时候,无论是通过pip install numpy 还是上网下载numpy包后安装都是出现问题:error: Unable to find vcvarsall.bat,于是百度 ...

  7. 【深度学习】windows下安装TensorFlow

    本文主要介绍如何在Windows下安装TensorFlow.当然建议还是在linux下安装,在windows下开发不太方便. 相关背景 网上现有的方法都是教如何在windows下安装虚拟机或者安装do ...

  8. 在python中requests模块怎么安装_Python requests模块在Windows下安装

    发现一个爬虫库太方便了,而且支持python3! 安装方法在http://docs.python-requests.org/en/latest/user/install/#install很详细 只不过 ...

  9. mysql5.7.25安装包,Mysql5.7.25在windows下安装

    在网上看到了很多安装方法,也试了很多,md,网上资源多了也是有各种坑,这里只说在windows下安装mysql5.7.25 一.下载安装包 下载后解压到自己想要安装的目录,我的是:D:\MYSQL\ ...

最新文章

  1. 常见却又不太了解的一些Windows文件类型
  2. vue是什么_什么是VUE?vue有什么作用?
  3. CSS_03_04_CSS伪元素选择器
  4. 【教女朋友学网络系列4】之今天教她一些简单的交换机实验
  5. mysql查看导入大小_mysql 数据导入、导出,及库大小查看
  6. android 应用无法安装程序,朋友android设备无法安装我的Android应用程序,我甚至不能为我自己做...
  7. 远程连接管理软件 v1.0
  8. 超干货!为了让你彻底弄懂 MySQL 事务日志,我通宵搞出了这份图解!
  9. 深入理解 C 语言的函数调用过程
  10. ORA-27125: unable to create shared memory segment
  11. Java dicom查看_验证DICOM文件
  12. unity3d补间动画DoTween
  13. Cesium中的primitive流光轨迹
  14. case when 语句用法
  15. [转载]【电子书下载神器】太给力了!你还找不到想要的电子书吗?
  16. Tesseract(识别验证码)
  17. 台式计算机win如何联网,Win10台式机怎么连接无线网(wifi)?
  18. Android后台监听耳机(线控、蓝牙)按键事件
  19. 分享一款多功能免费SEO工具箱-从0开始打造高流量网站
  20. 括号配对c语言,括号匹配(c语言实现)

热门文章

  1. 为什么哲学是最难的学科_高中所有科目难度排行 哪门学科最难
  2. Hit the Lottery
  3. 多元线性回归--正规方程解 以及线性回归的可解释性和其他思考
  4. 【对讲机的那点事】九招帮你轻松选购数字对讲机
  5. 5G移动通信系统设计与标准详解-学习笔记
  6. 机器学习——牛顿法详解
  7. Export for iTunes Mac(音乐文件管理软件)
  8. django常见启动报错总结
  9. 实现数据字典的缓存、加载、刷新和映射的集成框架
  10. css泡泡,CSS 气泡写法