Windows 下 VsCoq 配置踩坑记录（基于 wsl）

Posted on Edited on In

Abstract. 是谁没有 Mac 也没装 Linux 就来选 Software Fundations 啊🤣👉

原来是我🤡🤡🤡

讲一下今晚上配置 coq 环境的流程以及踩的所有坑。其实可能有的地方记不太清楚了。

配置时间和环境：2024. 2. 22，本地环境为 Windows 11 22621.3155，vscode 1.86.2，wsl 发行版为 Ubuntu 22.04，但是感觉未必需要对着配置。

Keywords. 环境配置, wsl, WSL_E_CONSOLE, Coq, VsCoq, opam。

首先作者不是原教旨主义者所以不会用 Emacs，于是考虑配一个 VsCoq

坑 1.

虽然可以在 windows 下面安装 coq，但是 VsCoq 的配置需要一个所谓的 code server，这个 server 需要用 opam 来安装，但是 opam 现在暂时没有 windows 版本。

据说 opam 2.2 之后会支持 windows，但是哥们享受不到了。

安装 WSL

考虑电脑上装一个 wsl，然后用 vscode 的远程连接插件连上去。

首先开始菜单搜索「启用或关闭 windows 功能」，在里面勾选

  • 适用于 Linux 的 Windows 子系统
  • 虚拟机平台
  • Windows 虚拟机监控程序平台

不知道有没有多选东西，反正这三个没什么问题。

接下来按指示重启电脑。

坑 2.

接下来应当把 wsl 版本调至 2，否则会寄。

打开 windows terminal，依次运行以下命令：

1
2
3
wsl --set-default-version 2
wsl --update
wsl --install -d Ubuntu-22.04

这样会安装 Ubuntu 22.04。

如果不加后两个参数会安装某个 Ubuntu，经过 lsb_release -a 发现好像也是 22.04。

接下来在 vscode 中安装扩展 WSL，Ctrl + Shift + p 后输入 WSL: Connect to WSL，理论上可以连接到刚才下的 Ubuntu。

坑 3（出现概率不高）.

此处遇到连接时程序反复报错 WSL_E_CONSOLE，无法连接。

一般人不会出现这个问题，因为这里纯粹是学 OI 学的，网上搜索也没有搜索到类似的情况。

这是因为在早年的算法竞赛经历中，为了在紧张调试运行程序时跳过 windows terminal 的动画（加载需要约 1s），选择了默认使用旧版命令行界面。但是 WSL2 并不能在旧版命令行界面中运行。

此时以任意方法打开旧版命令行界面，在左上角属性中将其禁用即可。

接下来所有命令均在 Ubuntu 中执行（在 windows terminal 中打开一个 ubuntu 的终端，或者在连接到 wsl 的 vscode 中开启终端）。

安装 Coq Prover

这一步没什么坑，直接运行

1
sudo snap install coq-prover

即可。

其实有一个，prover 只有一个 o，有傻逼不会英语拼错了。

安装 Opam

接下来的配置过程中需要用到 Opam。按照官网的指示依次执行

1
2
3
add-apt-repository ppa:avsm/ppa
apt update
apt install opam

即可。接下来需要初始化。

坑 4

注意 opam 的源本来是在国外的，接下来你需要下载大量的包，如果不换源后续安装过程极卡。

这里我们使用了 SJTU 提供的国内镜像，可以在初始化时直接使用该源，运行

1
opam init default https://mirrors.sjtug.sjtu.edu.cn/git/opam-repository.git

如果你忘了换源，直接运行了

1
opam init

也可以再运行 

1
opam repo set-url default https://mirrors.sjtug.sjtu.edu.cn/git/opam-repository.git --all --set-default

来切换。

配置 VsCoq

首先在 vscode 中安装扩展 VsCoq。接下来依插件说明页的说明，依次运行两个下载命令：

1
2
opam pin add coq 8.18.0
opam install vscoq-language-server

这会在 ubuntu 上安装 language server，接下来为了让 vscode 找到这个 server，你需要运行

1
which vscoqtop

坑 5.

如果此时没有输出（即失败），可能是没有刷新。运行

1
eval $(opam env)

然后重试。

此时你将得到一个类似于

1
/home/$USERNAME$/.opam/default/bin/vscoqtop

的输出，将其完整地复制下来，填入 VsCoq 的 Extension Setting 中，VsCoq: Path 的值。

坑 6.（舍友踩的）

有人在 Windows 下配环境变量配习惯了，把路径复制到 ../bin 就停了。但是此时必须要完整地复制全部内容。

然后预计就能跑了。为了测试你可以下载 Logical Fundations，然后打开里面的 Basics.v，理论上将会看到如下分栏的界面：

然后可以凭手感写几个前面的作业，有 FP 基础的话不需要读书读下上下文就能写。此时光标放在某个句号后面，右侧边栏就会进入 proof mode，并显示这个句号后面的 goal，举例来说：

然后看起来基本上能用了。