coq - 如何对 Coq 代码进行分区以提供 Coq ideslave(XML 协议(protocol))？

Question

我认为 Coq ideslave(也称为 Coq XML 协议(protocol))的“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 _]；精确的 H。 在另一种情况下，

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

应该分为三个部分，{，destruct Hl； [ 右 |破坏佛罗里达| ];假设。 和 }。我在 CoqIDE 中观察到了这些行为，我认为 CoqIDE 内部使用了 Coq ideslave。

我的第一个问题:这些是将 .v 文件分区为 block 以供“Add”调用使用的完整规则吗？如果不是，完整的规则是什么？

第二个问题:如果我只使用“按周期分区”规则，假设我尝试输入 { destruct Hl; [ 右 |破坏佛罗里达| ];假设。 } 作为一次“Add”调用而不是三次，XML 不会立即引发错误。然而，经过几个证明步骤后，它可能会引发一个错误(Thisproof is focused, but can't be unfocused this way)，该错误永远不会出现在 Coq IDE 中，并且我无法通过

撤消该错误

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

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

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

非常感谢您的帮助!

Answer 1

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

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

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

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

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