coq - `coqc -Q`返回“coqc：-Q：没有这样的文件或目录”

Question

当我尝试使用 编译文件时coqc -Q . LF，出现错误：

coqc: -Q: no such file or directory

coqc信息：

The Coq Proof Assistant, version 8.4pl6 (December 2020)
compiled on Dec 02 2020 23:06:36 with OCaml 4.02.0

奇怪的是它以前对我有用。我将磁盘格式化为相同的操作系统，安装了相同的 opam，但我遇到了一个以前没有的错误。也8.4.6出于遗留原因使用。

标签： coq

Answer 1

Coq 8.4.6 版不支持-Q选项，这可以通过查看手册来确认，其中没有记录此类选项。我还签入了源文件：它们可以从https://github.com/coq/coq/releases/tag/V8.4pl6. 对字符串的系统搜索-R表明它确实出现在文件中，但在源中的任何地方都scripts/coqc.ml没有出现字符串。-Q

你没有告诉我们整个故事。您没有复制完全相同的尝试...直到现在您一定一直在使用更新的版本。