Coq 的 XML 协议文档中的 "editId" 是什么？

Question

在 Coq's XML Protocol document (for the Add operation) 中，一行显示为 <int>${editId}</int>。这里的editID是什么？

我问这个是因为在ideslave模式下与coqtop交互失败。以coq-8.6.1/theories/FSets/FSetCompat.v为例，我输入了

<call val="Init"><option val="none"/></call>

,

<call val="Add"><pair><pair><string>Require Import FSetInterface FSetFacts MSetInterface MSetFacts.</string><int>1</int></pair><pair><state_id val="1"/><bool val="true"/></pair></pair></call>

,

<call val="Add"><pair><pair><string>Set Implicit Arguments.</string><int>1</int></pair><pair><state_id val="2"/><bool val="true"/></pair></pair></call>

，然后

<call val="Add"><pair><pair><string>Unset Strict Implicit.</string><int>1</int></pair><pair><state_id val="3"/><bool val="true"/></pair></pair></call>

它们都生成了正确的输出。然而，此时当我输入

<call val="Add"><pair><pair><string>Module Backport_WSets
    (E:DecidableType.DecidableType)
    (M:MSetInterface.WSets with Definition E.t := E.t
                           with Definition E.eq := E.eq)
<: FSetInterface.WSfun E.</string><int>1</int></pair><pair><state_id val="4"/><bool val="true"/></pair></pair></call>

我收到以下错误：

[pid 48519] XML syntax error: Attribute value expected
[pid 48519] XML syntax error: Xml node expected
[pid 48519] XML syntax error: Xml node expected
[pid 48519] Unexpected XML message
[pid 48519] Expected XML node: call
[pid 48519] XML tree received: <int>1</int>
[pid 48519] XML syntax error: Xml node expected
[pid 48519] Unexpected XML message
[pid 48519] Expected XML node: call
[pid 48519] XML tree received: <pair>
  <state_id val="4"/>
  <bool val="true"/>
</pair>
[pid 48519] XML syntax error: Xml node expected
[pid 48519] XML syntax error: Xml node expected

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

Answer 1

EditId 在 Coq 8.7 中被移除；由于协议的复杂性和历史问题，其最初的目的和历史有点复杂。

也就是说，Add 操作是同步的，因为用户界面必须等待使用新分配的标识符 (Stateid.t) 为添加的跨度做出回复。

但是，如果发生解析器错误，异步反馈系统需要一个时间标识符，edit_id 可满足该目的。

我们删除了 edit_id，因为 Add 无论如何都是同步的，因此 Add 的调用者使用同步错误处理程序而不是 edit_id- 是有意义的基于反馈。

请注意，我强烈建议不要使用Add的当前同步版本。它迫使客户端实现一个复杂的阻塞系统，并且它很快就会被一个异步友好的版本所取代[其中UI预先选择span_id]。这样的版本已经在 ML API 中可用，并由 SerAPI (*) 公开，并且很可能由 8.8.XML 协议本身公开。

(*) 通常的免责声明适用：我是 SerAPI 的作者，还要注意我是从 Coq 8.7 中删除 edit_id 的幕后黑手。

Answer 2

为 Add 发送 editid 似乎没有什么坏处，即使在 8.7 中，即使它在 Coq 方面未被使用。

我的基于 XML 的 Proof General 分支包括 editid for Add with 8.7，结果没有错误发生。

Coq 的 XML 协议文档中的 "editId" 是什么？

what is the "editId" in Coq's XML Protocol document?

xml

coq

coq-tactic

coqide