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

Question

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

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

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

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

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

- intros [H _]; exact H.

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

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

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

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

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

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

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

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

非常感谢您的帮助！

Answer 1

Jim，事实上，拆分 Coq 命令是一项不平凡的任务，我想说事实上的方法是 CoqIDE 使用的方法，参见 CoqIDE's lexer，还有 this mail，Emacs' regexp 和CodeMirror's tokenizer.

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

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

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

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