Как разделить код Coq для подачи Coq ideslave (протокол XML)?

Question

Я думал, что вызов "Добавить" 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 на куски для использования вызовов "Добавить"? Если нет, каковы полные правила?

Второй вопрос: если я использую только правило "разбито по периодам", скажите, если я пытаюсь кормить { destruct Hl; [ right | destruct Fl | ]; assumption. } как один вызов "Добавить" вместо трех, 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 одинаковые правила подачи кусков кода?

Большое спасибо за помощь!

Answer 1

Джим, на самом деле, расщепление команд Coq - нетривиальная задача, я бы сказал, что метод de-facto - это тот, который использует CoqIDE, см. Лексер CoqIDE, также эту почту, regexp Emacs и токенизатор CodeMirror.

Для Add вызов протокола, вы должны отправить одно предложение! Остальное игнорируется, и действительно, предложения включают в себя фигурные скобки. Вот где возникла ваша проблема.

SerAPI действительно включает дополнительную поддержку, чтобы помочь инструментам с расщеплением. Наиболее важные отличия:

• Когда вы отправите одно предложение, SerAPI ответит с фактическим местоположением конца предложения. Таким образом, вы можете точно проанализировать документ Coq, позволив SerAPI выполнить разбиение.
• SerAPI может анализировать полный документ Coq за один раз (и ответит с точками разделения).

Есть еще несколько технических деталей, касающихся полной поддержки документов, но их лучше рассмотреть на странице проекта.