如何确认lin-alg-8.10在Coq环境中正确安装？

一、确认lin-alg-8.10适配的Coq版本 #

从Coq库的常规版本命名规则来看，lin-alg-8.10默认适配Coq 8.10（这类库的版本号通常与目标支持的Coq版本对齐），可通过以下方式验证：

• 查看安装源的opam包定义文件（比如proverbot9001仓库内的相关配置），其中会包含depends: ["coq" {= "8.10"}]这类字段，明确标注依赖的Coq版本。
• 若为源码编译安装，检查Makefile中的COQVERSION配置项，或编译日志里的Coq版本信息。

二、确认lin-alg-8.10是否正确安装 #

针对你遇到的opam list无法查询到的情况，按以下步骤排查：

1. 确认当前opam switch环境 #

先确保你处于coq-8.10的本地switch中：

opam switch show

若输出不是coq-8.10，重新切换并加载环境：

opam switch coq-8.10
eval $(opam env)

之后再次执行opam list查询。

2. 排查是否为非opam源码安装 #

如果proverbot9001的指引是从源码编译安装（而非opam install命令），lin-alg不会出现在opam的包列表中，可通过以下方式验证：

• 创建测试文件test.v：

Require Import lin_alg.

用当前switch的Coq编译器编译：

coqc test.v

若未报错，说明库已成功安装到当前Coq的库路径中。

• 查看Coq的库根目录：

coqtop -where

检查该路径下的user-contrib或site-contrib文件夹，是否存在lin_alg相关的.vo、.v文件。

3. 检查opam包名是否有误 #

部分Coq库的opam包名会带前缀（比如coq-lin-alg），尝试用模糊搜索确认：

opam list | grep -i lin
# 或直接搜索包
opam search lin-alg

4. 排查opam缓存问题 #

若通过opam安装但列表无显示，执行opam update刷新缓存后再查询；或重新执行安装命令，查看日志是否有实际安装记录。

内容的提问来源于stack exchange，提问作者Charlie Parker