CoqのXMLプロトコル文書の「editId」とは何ですか？

Question

Coq's XML Protocol document (for the Add operation)には、<int>${editId}</int>と表示されています。ここでeditIDは何ですか？

私はサイドバイトモードで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を変更するかもしれない場合は、I疑います正しい答えが得られるはずです。私は正しい？そうでない場合、editIDは何を行いますか、このエラーをどのように扱うべきですか？助けてくれてありがとう！

Answer 1

EditIdをCoq 8.7で除去した。プロトコルと歴史的な問題の複雑さのために、その本来の目的と歴史は少し複雑です。

つまり、Addの操作は、追加されたスパンのためにユーザーインターフェイスが新しく割り当てられた識別子（Stateid.t）で返信を待たなければならないという意味で同期しています。

ただし、パーサーエラーが発生した場合、非同期フィードバックシステムには一時識別子が必要です。edit_idがこの目的に役立ちました。

私たちは、とにかく同期しているので、Addの呼び出し側が、同期エラーハンドラの代わりに、edit_idベースのフィードバックを使用することは理にかなってAddとしてedit_idを削除しました。

I は、現在の同期バージョン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フォークには、Addの8.32のeditidが含まれています。その結果、エラーは発生しません。