`coqc -Q`returns "coqc：-Q:没有这样的文件或目录“
`coqc -Q`returns "coqc：-Q:没有这样的文件或目录“
提问于 2020-12-03 14:07:26
当我尝试用coqc -Q . LF编译文件时，我得到了错误：
coqc: -Q: no such file or directorycoqc信息：
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。
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-12-03 16:10:19
Coq版本8.4.6不支持-Q选项，可以通过查看手册确认这一点，手册中没有记录此类选项。我还检查了源文件:它们可以从https://github.com/coq/coq/releases/tag/V8.4pl6下载。对字符串-R的系统搜索表明，它确实出现在文件scripts/coqc.ml中，但在源代码中的任何地方都没有出现字符串-Q。
你没有告诉我们整个故事。你不是在复制完全相同的尝试。到目前为止，您一定一直在使用更新的版本。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/65120702
复制相关文章
相似问题
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号