问题标签 [coqide]

抱歉这个琐碎的问题 --- CoqIDE 在 Coq 8.5 中的默认字体是什么？试用 Coq 8.6nix-shell -p coq_8_6 --run coqide并更改了我的旧 CoqIDE 字体（和键绑定）；我想要他们回来，但不记得字体名称。确切的版本（不确定这是否重要）是 8.5pl1。可悲的是，重新启动甚至nix-env --rollback没有恢复设置（我的 8.5 安装了 w/nix并且nix-shell -p coq_8_6 --run coqide不应该安装任何 AFAIK）

我使用 frama-C WP 并想调试我的 ACSL 注释（以了解为什么证明者说我“不知道”）。我有一些绿色或橙色的结果。我打开 why3 IDE 并查看生成的脚本。然后我从列表中选择一个理论/目标并能够启动 Alt-Ergo 或 Coq IDE。我想在 Coq IDE 中使用生成的代码。我看到一些公理，然后是 Theorem WP，然后，例如：

当我在 Coq 中“走到最后”时，我看到一个错误“尝试保存不完整的证明”。如何在 Coq IDE 中获得我在 frama-c 或 why3 结果窗口中看到的结果“已证明”或“未知”？还有什么更好的方法来理解为什么我从证明者那里得到“我不知道”的消息，并确定我的程序是否存在错误或错误的 ACSL 规范？

我有两个短文件： cc_test Lemma cc: 4 = 4. Proof. auto. Qed. 和 libtest 给出 Require Import cc_test. Check cc.

当我 coqc -R . ClosureLib -top ClosureLib cc_test 在目录“/home/barry/svn/Coq/Closure_Calculus” coqc -R "/home/barry/svn/Coq/Closure_Calculus" ClosureLib libtest 及其目录中执行时，我得到了预期的输出 cc: 4 = 4

但是，当上面的 coqc 的参数（从 -R 到结尾）放在 _CoqProject 文件中，然后我从 coqide 菜单中调用Make makefile，Makecc_test 没问题，但 libtest 产生输出 File "./libtest.v", line 1, characters 15-22: Error: Unable to locate library cc_test.

我应该如何修改项目文件以使其工作？

评论：coq 参考手册（第 15 章）没有提到这些方法之间的任何区别。此外，参数“-top ClosureLib”在命令行方法中似乎是必需的，但似乎并不重要，make因为在其他实验中，我经常收到错误消息，说它找到了 Top.foo 但没有找到 ClosureLib.foo。

我有GnuWin32 Make和GnuWin32 Coreutils，安装在我的PATH. 这有效：

但是，如果我Frap.v在 CoqIDE 中打开并执行Compile > Make，我看到的唯一输出是：

这是预期的吗？我怎样才能让 Coq 构建它？

在Coq 的 XML 协议文档（用于 Add 操作）中，一行读取<int>${editId}</int>. 这里的editID是什么？

我问这个是因为我无法在 ideslave 模式下与 coqtop 交互。举coq-8.6.1/theories/FSets/FSetCompat.v个例子，我输入

,

,

， 接着

他们都产生了正确的输出。但是，此时我输入

我收到以下错误：

我怀疑这个错误是因为多行字符串，也许如果我改变editId，我应该得到正确的答案。我对吗？如果不是，editID 是做什么的，我应该如何处理这个错误？感谢您的帮助！

I am using the XML Protocol from Coq 8.6.1. When I tried the PrintAst call, I failed to get an AST, but got an "todo" instead. Is this a malfunction or did I do something wrong? How should I get an AST from a print AST call?

Here is my case: I used coqtop -toploop coqidetop -main-channel stdfds to open an ideslave process, an then input the Coq code from coq-8.6.1/theories/FSets/FSetCompat.v.

Here I use "<<<<<<<" to enclose some detailed procedures if you would like to repeat my experiment.

<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<

First, I input

then

then

and finally

<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<

At this time, I called <call val="PrintAst"><state_id val="5"/></call>, which I expect to return the AST of

To my disappointment, I got

By pretty printing it is

But this is merely a copy of the code! It even didn't apply a lexer... Why would this happen? Could somebody help? Thank you so much!

我认为 Coq ideslave（也称为 Coq XML 协议）的“添加”调用一次需要一段代码，由句点 ( .) 分隔。在大多数情况下，我仍然相信这是真的。例如，

尽管这个代码块有几行，它应该由一个“添加”调用输入，因为只有最后一行有一个句点。

+但是，当存在项目符号（ 、-、*、{和}）时，情况并非如此。例如，

应该由两个“添加”调用输入，-在intros [H _]; exact H.另一种情况下，

应分三部分输入，{、destruct Hl; [ right | destruct Fl | ]; assumption.和}。我在 CoqIDE 中观察到了这些行为，我认为它在内部使用了 Coq ideslave。

我的第一个问题：这些是将 .v 文件划分为块以使用“添加”调用的完整规则吗？如果不是，完整的规则是什么？

第二个问题：如果我只使用“partitioned-by-period”规则，假设我尝试{ destruct Hl; [ right | destruct Fl | ]; assumption. }作为一个“Add”调用而不是三个调用，XML 不会立即引发错误。但是，经过几个证明步骤后，它可能会引发一个This proof is focused, but cannot be unfocused this way从未出现在 Coq IDE 中的错误 ( )，我无法通过以下方式撤消该错误

如果我尝试撤消错误，Coq XML 会给出相同的错误消息。这个错误是否与将子弹作为一个块喂食有关？如果是，为什么 Coq XML 不会在我提供该块时抱怨这个？

另一个问题：我想在不久的将来尝试 SerAPI。SerAPI 是否共享相同的提供代码块的规则？

非常感谢您的帮助！

我正在关注 cpdt ( http://adam.chlipala.net/cpdt/html/Universes.html ) 中的 Universes 章节，该章节运行Set Printing Universes.以查看有关类型的其他评论。但是，我正在运行 CoqIde 8.6，它没有任何效果。

以下代码

输出

而这本书说它应该输出

我错过了一些命令吗？我应该使用不同版本的 Coq 吗？

编辑：我只是在命令行中尝试了这个，coqtop它确实打印了类型注释。也许我必须在 CoqIDE 中启用一些额外的选项？

由于某种原因，我的 Coq 文件无法编译。我在 Windows 10 上使用 CoqIDE。当我使用该Compile->Compile buffer工具时，我得到

另一方面，当我使用该Compile->Make工具时，我得到

文件的完整代码在图片中给出。它也包括在下面。它缺少什么吗？我四处张望，想知道发生了什么。我发现的只是 Coq GitHub页面上的这个不祥的陈述：

“在 Windows 上编译 Coq 绝非易事。除非你是真正的 Windows 专家，否则不要尝试。如果你需要使用非发布版本的 Coq，或者你只是想让你的生活更轻松，你可以考虑将 Coq 安装到虚拟化 Linux 中，如下所述。”

我已经安装了 Coq，现在我正在尝试在 Mac 上安装 CoqIDE。我正在关注Coq wiki。第二步构建失败。当我跑

sh gtk-osx-build-setup.sh

这是我得到的错误：

我很感激任何帮助。