Coq의 XML 프로토콜 문서에서 "editId"는 무엇입니까?

Question

Coq's XML Protocol document (for the Add operation)에서 줄은 <int>${editId}</int>입니다. 편집 ID는 무엇입니까?

ideslave 모드에서 coqtop과 상호 작용하지 못했기 때문에이 질문을했습니다. 예를 들어 coq-8.6.1/theories/FSets/FSetCompat.v를 사용하여, I는

<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 어쨌든 동기이므로 대신 edit_id 피드백 기반의 동기 에러 처리기를 사용 Add의 호출자에 대해 합리적 제거.

은 현재 동기 버전 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의 경우 editid이 포함되어 있으며 결과적으로 오류가 발생하지 않습니다.