Some Feedback Message Errors mention a fresh state id

[Ptival]

I don't think this is coq-serapi's fault per se, but I find this behavior a little annoying to deal with:

(0 (Control (StmAdd () "Require Import List.")))
(Answer 0 Ack)
(Feedback((id(State 1))(contents Processed)(route 0)))
(Feedback((id(State 2))(contents(ProcessingIn master))(route 0)))
(Feedback((id(State 1))(contents Processed)(route 0)))

(Feedback((id(State 2))(contents(Message Error(((fname"")(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 15)(ep 19)))(Element(_()((PCData"Error: Unable to locate library List."))))))(route 0)))

(Answer 0(CoqExn(Errors.UserError(locate_library"Unable to locate library List."))))
(Answer 0 Completed)

My issue is that I'd like to know to what input sentence the feedback message that's highlighted belongs to. Usually, I first receive a (Answer 0 (StmAdded 2 ...)) which lets me relate query 0 to state id 2. Then upon receiving the feedback message, I know that if it says id(State 2), the error location relates to the sentence 0.

But for such a failure, I see id(State 2) in the feedback message without ever having received any information linking command 0 to state id 2.

This looks like I'm going to have to be more "stateful", do you know if there's any way to go around this?

[ejgallego]

Hi @Ptival , indeed this is due to https://coq.inria.fr/bugs/show_bug.cgi?id=4972 and is IMHO a serious Coq bug, but I need to investigate more (it could also be due to the way SerAPI does message processing).

So far, the best strategy is to ignore messages that refer to non-seen stateIds; I've been thinking on what the proper workaround would be.

I don't recommend you add any extra logic to PeaCoq; this should be solved in the SerAPI/Coq side.

[ejgallego]

So indeed the current situation about what should happen at Add time is far from specified, both upstream and in SerAPI (see #2, also coq/coq#203)

I think I'm gonna solve this for now as follows:

• Any feedback with a non seen StateId should be ignored.
• Any feedback containing EditId should be ignored.
• StmAdd is synchronous: Consumers must wait for either an Ack or a CoqExn signalling an error in the add.
• CoqExn will include information about location.

Note that unfortunately, due to coq/coq#203 not making it on time IDEs may have to figure out the position in a multi-add sentence.

[Ptival]

Seems like this would work for me, I would be able to link the CoqExn back to the sentence that failed and perform the proper error highlighting.

Why the synchronous requirement?

[ejgallego]

In fact, ide_slave provides the state id previous to the sentence that produced the error; however, I was told that doing so is wrong, but that is what CoqIDE does... it looks a bit messy...

Currently I think the only sensible thing to do is to consider StmAdd as synchronous: that is, no more messages should be sent before getting a reply. The main reason is that StmAdd may, in fact, observe all the document!

This is very inconvenient, but hard to fix with the current Coq "extensible" infrastructure. AFAICT Enrico has explored some possible solutions in https://github.com/coq/ceps/blob/master/text/001-v-file-format.md

[Ptival]

Anyway, at the moment I have to send my StmAdd synchronously either way (because my HTTP server runs its handlers in parallel and the writes to sertop are not done atomically, if I send multiple adds they might become tangled... :s)

So, at the moment this works for me, but if I ever switch to websockets and atomic IOs then I will have to be careful. I was just asking for documentation purposes.

[gares]

I confirm that Add (as well as all other XML messages from the UI to Coq) is synchronous. The only asynchronous messages are from Coq to the UI and are the feedback ones.

[ejgallego]

Hi @gares, thanks for the information; but note than in the SerAPI protocol all the messages (except StmAdd for now) are not "synchronous" by design, that is to say, the UI doesn't need to wait for an answer. Actually StmAdd could become "asynchronous" too if was not for the bugs in the upstream protocol.

[gares]

Hum, if you go that direction then beware that there are some complications. Coq receives a stream of commands, and all of them needs to be processed. If this takes time the UI will inevitably produce new commands on an outdated state. Isabelle went this way and added a interrupt message to essentially flush such queue plus a little more ids to be sure that UI and prover agrees on the last "version" of the document. And this in turn complicates the UI/protocol, while my guess is that by making all asynchronous the objective was to simplify the UI: just stream all action and handle feedback.