在 Windows 10 上安装 Coq 库 Mathematical Components

初学 Coq 时看的是 Mathematical Components 这本书，它自带了一个 Coq 的库，这是它的安装教程

这个库的安装要用到 OCaml Package Manager (OPAM) ，而它在本文所写之时（2021/9/25）仍不支持 Windows

我采用作者推荐的方式安装：采用 WSL 2

以下为步骤

确认 Windows 版本为 1903 及以上

可在终端内输入winver，在打开的窗口中查看
确认以下 Windows 功能均已启动：
- 适用于 Linux 的 Windows 子系统
- 虚拟机平台
可以在这里查看：控制面板 > 程序 > 程序和功能 > 启用或关闭 Windows 功能

或者直接在终端中输入以下两行指令以打开：
```
dism.exe /online /enable-feature /featurename:Microsoft-Windows-Subsystem-Linux /all /norestart
dism.exe /online /enable-feature /featurename:VirtualMachinePlatform /all /norestart
```
若未启用功能，要在启用后重启电脑。
升级 WSL
- 下载并安装 Linux 内核升级包：wsl_update_x64.msi
- 在终端输入wsl --set-default-version 2
为 WSL 下载 GNU/Linux 发行版

在 Microsoft Store 中选择

这里我使用 Debian

安装完后运行，按提示设置好用户名、密码

运行下列指令以安装一些基础应用
- sudo apt update
- sudo apt-get install emacs
安装 X.org 服务器以便在 WSL 中使用图形界面应用
- 下载并安装 VcXsrv Windows X Server
- 打开 XLaunch，依次选择 Multiple windows、Start no client，勾上 Disable access control之后每次用 WSL 都需打开并设置一次
- 打开控制面板 > 系统和安全 > Windows Defender 防火墙 > 高级设置 > 入站规则
- 找到名称为VcXsrv windows xserver的两项，分别双击打开并检查：
  - 确认常规 > 操作一栏中选择了允许连接
  - 确认作用域中两栏均选择了任何 IP 地址
- 在 WSL 终端内输入emacs ~/.bashrc，在代码末尾添加一行：（这需要一点点的 Emacs 基础知识）
```
export DISPLAY=$(awk '/nameserver / {print $2; exit}' /etc/resolv.conf 2>/dev/null):0
```
- 重启 XLaunch，WSL 终端，这时启动 Emacs 等图形界面应用就应该会弹出一个独立的窗口了

依次在 WSL 终端中执行下列命令，其中的一些可能需要等待较长时间

sudo apt install opam libgmp3-dev libcairo2-dev libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev

```
opam init
```
```
opam switch create 4.11.2
```

opam repo add coq-released https://coq.inria.fr/opam/released

```
opam install coq
```
```
opam install coqide
```
```
opam install coq-mathcomp-ssreflect
```

此时就已经安装完了，输入coqide便可进入 Coq 的集成开发环境

参考：Installation of MathComp on Windows 10

在 Windows 10 上安装 Coq 库 Mathematical Components相关推荐

如何在Windows 10上安装Python
Installing and using Python on Windows 10 is very simple. The installation procedure involves just t ...
如何在 Windows 10 上安装 WSL 2
翻译自 Joey Sneddon 2020年10月30日的文章<How to Install WSL 2 on Windows 10> [1] 如果您想在最新的 Windows 版本中尝试 ...
如何在Windows 10 上安装SQL Server 2000数据库?
Win10本身是一个兼容性较好的操作系统,目前有很多人在咨询如何在Windows 10 上安装 SQL Server 2000数据库,都没有成功过.主要是卡在了安装过程中的mdac2.6 安装上,一直 ...
如何在 Windows 10 上安装和配置 SNMP 服务并通过组策略配置 SNMP 设置
简单网络管理协议或 SNMP用于企业网络上的监控.事件通知和网络设备管理.该协议由一组网络管理标准组成,包括应用层协议.数据库模式和一组数据对象.SNMP 可以从任何网络设备接收各种类型的信息(正常运 ...
如何在Windows 10上安装PowerShell 7
Microsoft 微软 Microsoft announced PowerShell 7.0 on March 4, 2020. It's the latest major update to Po ...
如何在 Windows 10 上安装华为模拟器eNSP？保姆级的教程来喽，附安装包下载
由于最新版本的 eNSP不再包含必备组件 VirtualBox 和 WinPcap,为了使安装生效,我们需要预先安装这些组件.在这篇文章中,我将向您介绍如何在 Windows 10 中安装 eNSP ...
如何在没有微软商店的情况下在Windows 10上安装应用程序
如何在没有微软商店的情况下在Windows 10上安装应用程序通过微软商店,你可以轻松地在Windows 10设备上安装应用程序,就像使用Google Play或AppleStore一样.IT部门经 ...
Windows 10 上安装 3D Studio Max 2016 报错的解决办法
在 Windows 10 上安装 3D Stuido Max 2016 报错,无法正常安装,查看日志是 VC 运行时安装错误,经过分析发现在 Windows 10 上已经有这些运行时并且版本比安装包中 ...
如何在Windows 10上安装MySQL数据库服务器8.0.19
In this article, I am going to explain the step by step installation process of MySQL database serve ...
python安装环境变量出错_在windows 10上安装twisted时出错。INCLUDE环境变量为空
我已经在我的windows机器上安装了python3.4.4,并试图在我的机器上安装twisted库.在>>>python Python 3.4.4 (v3.4.4:737efcad ...

在 Windows 10 上安装 Coq 库 Mathematical Components

在 Windows 10 上安装 Coq 库 Mathematical Components相关推荐

最新文章

热门文章