State id to `Add` the first sentence to about coq-serapi

[cpitclaudel]

I've pushed it here. Demo @ https://asciinema.org/a/b84ph360841x3c9lwq6pyihm9

[ejgallego]

Hi Clément, I am a bit confused here, are you are talking about sending the whole document to Coq with Add?

[ejgallego]

With regards to (STM == Coq) states, State 1 is the root state, State 0 is reserved for the "dummy" state (o_o)

SerAPI does indeed add a command if you use --prelude: Require Import Coq.Init.Prelude. We could import prelude in a different way without using the Stm, but I much prefer to make prelude loading explicit. Some users like the HoTT folks don't want indeed to load Coq's Prelude.

[ejgallego]

Oh I think I see what you mean.

[ejgallego]

Is cd293d8 what you had in mind?

Note that in the async case, you may have several tips where to add stuff to I think.
Thus I made the ontop an option type for now instead of getting rid of it.

[cpitclaudel]

Hmm no, that's not exactly what I meant (sorry for the delayed answer). In fact, I'm not sure it's too good to allow this default, since it indirectly exposes to the user the fact that there exists a "current state". Thus I think that ontop should be mandatory :)

My suggestion was a bit different. In almost all cases I know which state to attach to: the one that's (textually) the closest before the current edition point. There's just one case where I don't know; namely, when I'm at the very beginning of the document and I haven't sent any sentences yet.

I'd just like to have a way to know to which state ID I should attach the first sentence that I send :)

Sorry for not making this clear :/ Is it better now?

[cpitclaudel]

Actually, thinking more about it, let me backtrack slightly on this. Keeping cd293d8, we could just make None throw an exception if there's more than one tip. This way it can be used for the first sentence, and there's no risk of getting into a confusing state in async mode if there are multiple tips.

What do you think?

[ejgallego]

Umm, I didn't understand why (StmState) didn't work for you? The initial State is always 1 but Coq doesn't guarantee you can rely on that, you need to use the number coming from Stm.get_current_state.

I think keeping cd293d8 is OK, you can always use (Some stateid) if you want to be explicit; and None if you want to add at the end of the document. IMHO throwing an exception is overkill. The current "tip" of the Stm is a perfectly well defined notion even in async mode, so I'd say let's just make None = current tip.

[ejgallego]

"this very notion of "current state" will go away at some point (right? "

Current state here really means the end of the document, so indeed, you are right that even if internally the Stm needs to keep track of it, it is useless for the document.

I see what you mean now and I'm not sure what is the cleanest way... It looks like we need a special case one way or another.

[cpitclaudel]

I think None works very nicely when there are no branches (i.e. a single tip). In async mode with multiple tips, it probably doesn't hurt to have None mean the current tip; but it any case, I think in the long run we can simplify the protocol by not exposing the notion of current state; instead, we can translate any Add into an EditAt followed by an Add (and we can make Add fail if it's not adding to an actual tip).

Bottom line: I'm happy with cd293d8 :)

[ejgallego]

Oh that is interesting; I didn't think so much of the async mode yet so excuse me if I look lost there.

What would be the case for Add behaving like EditAt ? Presumably, you first cancel, then allow the user to edit, then Add. Where would the new input for such an Add come from?

I'm sure I've been missing something in this issue all the time, maybe a concrete example would help :)

[ejgallego]

[edit]: This comment doesn't seem to be true.
Note something very important indeed:

In almost all cases I know which state to attach to: the one that's (textually) the closest before the current edition point. There's just one case where I don't know

I'm much afraid this doesn't hold if I understood the Stm correctly. Imagine:

1. You add 10 independent proofs, you observe all of them, 9 check OK, 1 proof fails. The current tip is in the last added sentence, let's say id = 100.
2. You then want to do an edit_at at the proper place, let's say 35. This will return a focus = { start = 30; stop = 40; tip = 101} !! You invalidate the 35-40 range. But note the new tip! You add on top of 101 until you get an Unfocus 105 from Add.
3. You want to add at the end of the document. Now, you cannot look at the previous sentence, given the way document versioning works, looking at previous sentence doesn't work anymore.

I think it works this way but I am not 100% sure yet, so please bear with any error.

I am not sure either what this implies for the IDE design, certainly a possibility would the to split the document pointer into a "version" field and a stint field, but I guess we need to think a bit more.

[cpitclaudel]

Hmm. Not sure I understand this in full.
What I could see working well here is changing the semantics of Add in the following way:

• From the IDE perspective, there is no "current tip". There's just a collection of sentences, some that Coq knows about and some that it doesn't.
• The ones that Coq knows about have a state id (except during a small time window after they are are Added, until the response for the Adds comes). The ones that Coq doesn't know about are free form text.
• The way to let Coq know about a sentence is to connect it to a previously known sentence. This is done using Add, passing the state to which the new sentence connects. If there are no previous states, passing None instead of a state ID is fine. (More generally, if there is only one possible addition point, then passing None instead of a state ID is fine. This is useful for the document's very first sentence).
• The way to tell Coq to forget about a sentence is to use Cancel on that sentence.
• When Coq forgets about a sentence, it may need to forget about others. These are all the ones that don't have a parent anymore. Typically all the ones inside of a Proof-Qed block, but it could be all of the document as well. In the future, it could be more fine grained.

This is the basic logic. When looking for a sentence to attach to, the closest preceeding "known to Coq" one is always the right one, I think. There are multiple possible failures:

• Add can fail if the sentence that we're trying to attach to is unknown to Coq. This could happen if Coq has issued a Canceled message for that sentence and the IDE hasn't processed it yet. In that case, we mark the sentence that we tried to add as unknown to Coq. The IDE must handle this failure, as it is expected to happen, albeit rarely.
• Add can also fail if we try to add a sentence to a state id that already has children. This would be a logic error in the IDE; it is not an expected failure case.
• Cancel can fail if the state is already unknown to Coq. In that case, Coq can just ignore the stale Cancel message. This doesn't return an error to the IDE; the IDE can expect the cancellation to have succeeded.

The underlying Stm has a notion of current state, but it doesn't seem useful to expose it to the outside world. Add (as specified in this proposal) doesn't need it; Cancel doesn't either. Goals doesn't, as long as its allowed to pass a state id.

What do you think? If this more understandable? :)

[ejgallego]

Thanks, I think I see what you mean, but honestly I don't understand the STM well enough. I need to think more about this. There is a DAG, an internal VCS, the states (that are kind of chronologically ordered).

I guess a possible way to proceed would be to assemble a set of interesting examples, and have a "tracing" mode to see what the STM does.

[ejgallego]

I think my previous comment about Unfocus was wrong, however I cannot really test what I want as CoqIDE crashes...

[ejgallego]

Regarding your comment, I think this is mostly how things are working right now, modulo bugs. Do you see any important deviation?

[cpitclaudel]

Hmm, which one was my first comment?

[ejgallego]

I meant this comment: #14 (comment)

In fact, I'd consider any deviation from it a bug.

[cpitclaudel]

Cool :) I think I need more testing. I'll push my work somewhere soon if you want a quick peek :)
But if you agree with that comment, then awesome! This sounds like a simple and sweet protocol.

[ejgallego]

Cool thanks! I'd love to see it! I'm not an expert on elisp but I'll be able to survive I think :D

Yeah, I think that the protocol you've proposed is something sensible to strive for, let's see what we find with async, etc... and how we can manage to connect to the STM.

[ejgallego]

Amazing!!!!

[ejgallego]

wrt to the original question in this issue, see also this comment in #11.

[ejgallego]

Note that older versions of SerAPI had a bug and didn't forward to the client the initial feedback. Indeed, when SerAPI starts the STM will emit a feedback message providing the location of the root state:

(Feedback ((id (State 1)) (contents (ProcessingIn master)) (route 0)))
(Feedback ((id (State 1)) (contents Processed) (route 0)))

[ejgallego]

Hi, so I'm thinking of closing this issue soon. My plan of action is:

• 1 is guaranteed to be the initial state.
• A cancel on 1 has no effect.
• We usually may need to perform some pre-STM initialization like setting load paths, loading the prelude, options, etc... before creating the initial state (and thus are not reversible). There are two possibilities:
  • Add a new Init control call to the protocol. Clients will then do (Control (Init (opts))) and can start sending commads. (No need to wait for the (Feedback ((id (State 1)) (contents Processed) (route 0))) event.)
• Another option would be to handle "init" by command line arguments, thus clients can assume that SerAPI always starts initialized. This may be indeed simpler.

What do you think?

Cheers,
E.

[ejgallego]

Almost done, will close when the docs are ready.

[ejgallego]

A further update on this issue, Coq upstream has gained a new API point new_doc, thus the root of the document will be chosen by the client in the document creation call.