如何划分 Coq 代码以提供 Coq ideslave（XML 协议）？

Question

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

Inductive or (A B:Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B

where "A \/ B" := (or A B) : type_scope.

尽管此代码块有几行，但它应该由一次 "Add" 调用输入，因为只有最后一行有句点。

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

- intros [H _]; exact H.

应该由两个 "Add" 调用输入，- 和 intros [H _]; exact H. 在另一种情况下，

{ destruct Hl; [ right | destruct Fl | ]; assumption. }

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

我的第一个问题：这些是将 .v 文件分成块以供 "Add" 调用使用的完整规则吗？如果没有，完整的规则是什么？

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

撤消错误

<call val="Edit_at">
    <state_id val="..."/>
</call>

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

附加问题：我想在不久的将来试用 SerAPI。 SerAPI 是否共享相同的代码块馈送规则？

非常感谢您的帮助！

Answer 1

Jim，事实上，拆分 Coq 命令是一项非常重要的任务，我想说的是 CoqIDE 使用的实际方法，参见 CoqIDE's lexer, also this mail, Emacs' regexp, and CodeMirror's tokenizer。

对于协议的Add调用，应该单句发送！其余的被忽略，事实上，句子确实包含大括号。这就是您的问题所在。

SerAPI 确实包括额外的支持来帮助工具进行拆分。最重要的区别是：

当您提交单个句子时，SerAPI 将回复实际的句末位置。因此，您可以通过让 SerAPI 进行拆分来准确地解析 Coq 文档。
SerAPI 可以一次性解析一个完整的 Coq 文档（并将返回拆分位置）。

关于全文档支持还有一些更多的技术细节，但这些应该在项目页面上得到更好的解决。

如何划分 Coq 代码以提供 Coq ideslave（XML 协议）？

How to partition Coq code to feed Coq ideslave (XML protocol)?

coq

coqide