2

我认为 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 不会立即引发错误。但是，经过几个证明步骤后，它可能会引发一个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 是否共享相同的提供代码块的规则？

非常感谢您的帮助！

4

1 回答 1

3

吉姆，事实上，拆分 Coq 命令是一项不平凡的任务，我想说事实上的方法是 CoqIDE 使用的方法，请参阅CoqIDE 的 lexer，还有这个 mail，Emacs 的 regexp和CodeMirror 的 tokenizer。

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

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

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

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

于 2017-12-19T10:40:12.370 回答