Coq新手求教：如何编译.vo文件并在命令行运行相关指令？

第一步：配置Coq环境变量 #

Windows终端识别不了coqc的核心原因是Coq的可执行文件路径没有加入系统环境变量，按以下步骤操作即可：

• 找到你的Coq安装目录，默认路径一般为C:\Coq-platform\bin或者C:\Program Files\Coq\bin，确认该文件夹下存在coqc.exe文件
• 右键「此电脑」→「属性」→「高级系统设置」→「环境变量」
• 在「用户变量」或「系统变量」列表中找到Path条目，点击「编辑」
• 新建一条记录，将刚才找到的Coq的bin文件夹完整路径粘贴进去，依次点击确定保存所有配置
• 重启所有已经打开的终端窗口，环境变量修改才会生效

第二步：验证coqc指令可用性 #

Windows自带的cmd、PowerShell、Windows Terminal都可以使用，随便打开任意一款终端，输入指令：
coqc --version
如果终端输出Coq的版本信息，说明配置已经生效。

第三步：编译Basics.v文件 #

• 找到你本地存放Basics.v的文件夹，比如路径为D:\study\sf\Basics.v
• 在终端中用cd指令切换到该文件夹，示例：

  cd D:\study\sf
  # 如果是cmd终端，切换盘符后需要额外输入盘符指令
  D:
  

• 执行编译指令：coqc Basics.v
• 没有报错的情况下，文件夹内会生成对应的.vo文件，即编译成功。

常见问题排查 #

• 若还是提示找不到coqc：可以直接使用绝对路径调用指令，比如"C:\Program Files\Coq\bin\coqc.exe" Basics.v，路径包含空格的话需要包裹双引号
• 若编译时报代码错误：先在CoqIDE或者VSCode+Coq插件中逐行校验代码，确认所有语法、证明逻辑没有问题后再执行编译。

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