2

我正在使用《Certified Programming with Dependent Types》一书，但每次我都发现不同的错误。在我看来，错误来自 Proof General 的编译过程与本书来源的 makefile 之间的不匹配。

  1. 如果我使用 make 编译源代码并尝试在 Proof-General 中运行例如 Subset.v，我会得到：

错误：文件 /home/usuario/Desktop/Coq/cpdt/src/CpdtTactics.vo 有错误的幻数 81100（预期为 8600）。它已损坏或使用其他版本的 Coq 编译。

  1. 如果我用 make clean 清理 makefile 编译文件并尝试继续使用选项 Coq -> Auto Compilation -> Compile before require 那么它是以下行：

需要提取。

那失败了。最初它因错误而失败：

错误：无法找到库提取。

但是使用上面的选项启用它会给出类似的东西：

回声“需要提取。” > /tmp/ProofGeneral-coqQPJTf0.v coqdep -Q /home/usuario/Desktop/Coq/cpdt/src/ -R /home/usuario/Desktop/Coq/cpdt/src Cpdt /tmp/ProofGeneral-coqQPJTf0.v * 警告: 在文件/tmp/ProofGeneral-coqQPJTf0.v 中，库提取是必需的，并且在加载路径中没有找到！*警告：在文件 /tmp/ProofGeneral-coqQPJTf0.v 中，库提取是必需的，并且在加载路径中没有找到！/tmp/ProofGeneral-coqQPJTf0.vo /tmp/ProofGeneral-coqQPJTf0.glob /tmp/ProofGeneral-coqQPJTf0.v.beautified：/tmp/ProofGeneral-coqQPJTf0.v /tmp/ProofGeneral-coqQPJTf0.vio：/tmp/ProofGeneral-coqQPJTf0 .v

我该如何解决这个问题？

4

1 回答 1

3

附带问题：您使用的是哪个操作系统？你靠opam吗？

关于你得到的第一个错误，它肯定来自以下事实：

  • 在 proofgeneral 之外，coqc二进制对应于 Coq 8.11，而在 ProofGeneral 中，coqtop二进制对应于 Coq 8.6。可能是因为PATH两个上下文中的变量不一样。

  • 要确定找到哪个二进制文件，您可以在终端which coqtop和 Emacs 中进行，M-! which coqtop RET因此您应该获得不同的路径。

  • 有时，emacs直接从终端 ( emacs &) 打开可以帮助解决此类问题。

  • 但是，如果您想更改coqtopProofGeneral 中使用的二进制文件，您可以coq-prog-name使用以下步骤之一设置该选项：

    • 以交互方式输入C-u C-c C-x（杀死 Coq）M-: (setq coq-prog-name "…/coqtop")、 和C-c C-n

    • 或者在项目根目录中创建一个.dir-locals.el文件（Emacs 的标准配置文件），其中包含：

      ((coq-mode . ((coq-prog-name . "…/coqtop"))))

      并关闭/重新打开有风险的….v文件（或者只是做M-x normal-mode RET或C-x C-v RET在已经打开的….v缓冲区中）

关于你得到的第二个错误，我有点困惑Require Extraction触发这个错误，因为这个库确实存在于 Coq 8.6 和 8.11 中。

乍一看，我建议用 Coq 8.11 重新测试自动编译，断言From Coq Require Extraction.（而不是仅仅Require Extraction.）

但也许PG的Auto Compilation -> Compile before require功能有一个bug；无论如何，如果需要，请随时在 PG 跟踪器中打开相关问题，非常欢迎错误报告和功能请求：https ://github.com/ProofGeneral/PG/issues

于 2020-04-19T11:15:02.667 回答