0

在Coq 的 XML 协议文档（用于 Add 操作）中，一行读取<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 是做什么的，我应该如何处理这个错误？感谢您的帮助！

4

2 回答 2

1

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

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

但是，如果发生解析器错误，则异步反馈系统需要一个时间标识符，以达到edit_id此目的。

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

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

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

于 2017-12-06T02:17:57.393 回答
0

editid即使在 8.7 中，发送for an似乎也没有什么坏处Add，即使它在 Coq 端没有使用。

我的基于 XML 的 Proof General 分支在 8.7 中包含一个editidfor Add，因此不会发生错误。

于 2017-12-06T22:35:24.867 回答