How does EditAt work? / EditAt limitations about coq-serapi

[cpitclaudel]

Wonderful, thanks!

Btw suggestion/request: maybe the Cancel command and Canceled message could take/return a list of states instead of a single one? This way if Coq needs to tell the IDE to cancel many states, it can do so in a single message. Same on the IDE side.

[ejgallego]

Ok 8dfd67a

[ejgallego]

Yes, NewTip means that as far as I can tell. In jsCoq we need to keep a linked list of things to invalidate :S

I totally agree this is not optimal, I'm working on a better system following your recommendations.

[ejgallego]

Ok, 6a3a973 deprecates StmEditAt and introduces a prototype of StmCancel. Beware of bugs!

[ejgallego]

A weird thing that I've noticed the STM do is that if you do an EditAt at some state, the STM observes all the states leading up to it! Weird, how is that supposed to work? Maybe @gares can comment?

[ejgallego]

Very interestingly, if I enable some async flags this is not the case anymore, interesting!

[cpitclaudel]

re "Canceled": Cool, thanks!

[cpitclaudel]

re EditAt: Indeed, I observed the same thing.

[cpitclaudel]

Which flags are you enabling to get async processing though? Even with -async-proofs-j 4, I'm still seeing this behaviour.

I'm using the following example:

<call val="Init"><option val="none"/></call>
<call val="Add">
  <pair>
    <pair>
      <string>Goal True.</string>
      <int>0</int>
    </pair>
    <pair>
      <state_id val="1"/>
      <bool val="true"/>
    </pair>
  </pair>
</call>
<call val="Add">
  <pair>
    <pair>
      <string>do 1000 (do 1000 idtac).</string>
      <int>1</int>
    </pair>
    <pair>
      <state_id val="2"/>
      <bool val="true"/>
    </pair>
  </pair>
</call>
<call val="Add">
  <pair>
    <pair>
      <string>do 1000 (do 1000 idtac).</string>
      <int>2</int>
    </pair>
    <pair>
      <state_id val="3"/>
      <bool val="true"/>
    </pair>
  </pair>
</call>
<call val="Add">
  <pair>
    <pair>
      <string>do 1000 (do 1000 idtac).</string>
      <int>3</int>
    </pair>
    <pair>
      <state_id val="4"/>
      <bool val="true"/>
    </pair>
  </pair>
</call>
<call val="Add">
  <pair>
    <pair>
      <string>do 1000 (do 1000 idtac).</string>
      <int>4</int>
    </pair>
    <pair>
      <state_id val="5"/>
      <bool val="true"/>
    </pair>
  </pair>
</call>
<call val="Edit_at"><state_id val="5"/></call>
<call val="Edit_at"><state_id val="2"/></call>

[ejgallego]

See the --async option and flags sertop_init. I do this:

$ rlwrap ./sertop.native --prelude ~/external/coq-git/ --human --async
(adding-goal (Control (StmAdd 5 2 "Goal True. do 1000 (do 1000 idtac). do 1000 (do 1000 idtac). do 1000 (do 1000 idtac). do 1000 (do 1000 idtac).")))
(adding-goal (Control (StmCancel 2)))

Seems to work pretty well.

[ejgallego]

Concretely: https://github.com/ejgallego/coq-serapi/blob/master/sertop/sertop_init.ml#L60

[ejgallego]

An additional comment: I am implement a document DAG in SerAPI, which is necessary for the cancel feature. This will liberate jsCoq of having to maintain a global document model.

At least, in the SerAPI side, there's hope of syncing such DAG with the STM DAG in race-free manner. In the medium term, both DAGs implementation should merge IMO.

[cpitclaudel]

Very nice, thanks. Can you help me derive the right sequence of calls for the following, though?

• Users adds "Goal true. slow."
• User edits "slow." into "fast."

I was expecting something along the lines of:

(adding-goal (Control (StmAdd 1 2 "Goal True.")))
  (Answer adding-goal Ack)
  (Answer adding-goal
          (StmAdded 3
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 0)
                     (ep 10))
                    NewTip))
  (Answer adding-goal Completed)
(adding-slow-idtac (Control (StmAdd 1 3 "do 1000 (do 1000 idtac).")))
  (Answer adding-slow-idtac Ack)
  (Answer adding-slow-idtac
          (StmAdded 4
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 0)
                     (ep 24))
                    NewTip))
  (Answer adding-slow-idtac Completed)
(canceling-slow-idtac (Control (StmCancel 4)))
  (Answer canceling-slow-idtac Ack)
  (Answer canceling-slow-idtac Completed)
(adding-fast-idtac (Control (StmAdd 1 3 "do 1000 idtac.")))
  (Answer adding-fast-idtac Ack)
  (Answer adding-fast-idtac
          (CoqExn
           ("\"Anomaly: Not yet implemented, the GUI should not try this\"")))

Is that the correct sequence?

[ejgallego]

Oh I see, Cancel currently takes the first valid state like EditAt! So you should have passed 3. Let me fix it!

[cpitclaudel]

Ah, got it! Thanks :)

[ejgallego]

Ok fixed in ab23c0a ! Keep in mind that the internal document model is linear for now!

[ejgallego]

This works from me ™ :

(adding-goal (Control (StmAdd 2 2 "Goal True. do 1000 (do 1000 idtac).")))
(cancel-goal (Control (StmCancel 4)))

[ejgallego]

It is still not clear what to with answer batching, I guess we are a bit inconsistent now but hopefully we can get to reexamine that invariants when we are happy with a running, async API.

[ejgallego]

One possible invariant for answers to control commands is to be a bit more RPC-iy, that is, be strict in allowing only an answer Ack+ a Completed result, but I'm not sure this is possible/optimal in all cases.

[cpitclaudel]

Not sure either :) In any case, this Cancel/Canceled thing works very nicely (just tried it) :)) Thanks!

[ejgallego]

Great, thanks Clément! I cannot wait to see your stuff working. Using your Cancel model will allow for great simplifications in jsCoq.

Let me know BTW if you have comments on Adding multiple sentences in one go. I didn't do any batching there, mainly because we may emit an exception but still parse a few valid ones.

[ejgallego]

Also, I dunno if we should emit a "cancelled" reponse in EditAt. Adding it now for consistency but it is non standard.

[cpitclaudel]

Thanks; I don't care too much about EditAt since I'm not using it for now, but we'll see.
Do you think we could extend Goals to take a state id? What are other places that still need EditAt?

[ejgallego]

Do you think we could extend Goals to take a state id?

Ah! That's a tricky one... :D We'll be able to figure something out, but this should better go in their own issue #15

What are other places that still need EditAt?

It should not be needed in other places, but having it around is very convenient for instance for the CoqIDE port.

[cpitclaudel]

It should not be needed in other places, but having it around is very convenient for instance for the CoqIDE port.

Of course :) I'm thinking about simplifications of the protocol in the long run. I think or SerAPI as the basis on which most Coq IDEs will be built in the future, and it would be nice to streamline it as much as possible. With the Add/Cancel stuff that I outlined earlier I think we'd have a very nice interface, with little complexity on the IDE side and lost of opportunities for improving things under the hood without breaking IDE compatibility.

[ejgallego]

+1 ! Indeed all the comments are great, thanks. I am struggling a bit on trying to understand how the imperative state is managed now.

[ejgallego]

Ok, so I have finally found how EditAt works!!

• In most configurations I've tried, it will just invalidate the whole document after the edit.
• In the CoqIDE configuration it invalides a zone. However, and this is very important, you can only Add on top of the edited id. Until you add a closing token (usually Qed), it won't allow you to append at the end of the document.

CoqIDE shows this behavior well. I think this is not how we'd like it to work, so I'm assigning this upstream, to give feedback for 8.7.

[ejgallego]

Thus in our current configuration we should be safe wrt to elcoq, at the cost that any edit indeed seems to invalidate the whole doc after it.

[cpitclaudel]

Makes sense, thanks for the explanation!

Until you add a closing token (usually Qed), it won't allow you to append at the end of the document.

What happens if you call EditAt on the last state of the document before trying to append?

[ejgallego]

It seems to work fine, it is basically a noop.

[ejgallego]

My test case, to be used with option --deep-edits:

(Control (StmAdd 100 None "
Ltac slow := do 400 (do 800 idtac).
Ltac wrong := intro.

Lemma a: True.
Proof. slow. wrong. auto. Qed.

Lemma d: True.
Proof. slow.
"))

(Control (StmObserve 13))
(Control (StmEditAt 7))
(Control (StmAdd 10 (Some 7) "auto."))
(Control (StmAdd 10 (Some 14) "Qed."))

[cpitclaudel]

It works fine, it is basically a noop.

So that means that it's enough to do edit at at the end of the document to be able to append to the end of the document again, right? (If I understand correctly, then that's neat!) And your example shows that, right? (except for the fact that SerAPI makes all the jumping around and EditAt transparent to the IDE :)

Do I understand this properly?

[ejgallego]

Ah! I misunderstood. This is what happens:

(Control (StmEditAt 13))
(Answer 3
 (CoqExn ("\"Anomaly: edit_at 13: Cannot leave an `Edit branch open.\"")))

So it seems that unless you give a Qed, you are stuck in the EditAt forever. @gares?

[gares]

I don't have the code at hand but once you reopen a proof branch you are supposed to add a Qed/Admitted node before editing at something that (IIRC) follows the proof. This is natural in CoqIDE, since the "Qed" text is still there, so jumping forward re-closes the proof.

[gares]

If you don't, then the document structure changes in a drastic way, so kaboom. A proof has to be replaced by a proof, nothing more.

[ejgallego]

I see, thanks Enrico! I guess it would be great if we could focus on other parts of the document while leaving a branch open, do you think it is possible? (Maybe the editAt would just admit the old branch?)

Both in CoqIDE and emacs, it feels a bit unnatural to edit a branch and not be able to write at the end of the document.

[ejgallego]

Hi, so I think I've got a lead on how to close this issue: SerAPI will allow arbitrary cancels/add at the document, and will try to work around the current Stm limitation of a single "Adding Point".

IMHO this will simplify IDE's writers life a lot: they will just inform SerAPI of cancels and additions.

There are a couple of details to figure out, yet. Internally, we maintain our own document model (need to port the code form jscoq_doc.ml). If the user wants to edit somewhere else, we will just admitted the current open proof, and refocus appropriately.

However, given the way the STM works, this admit will create a new stateid. This may mean that the IDE may need to listen to the Admitted event and insert a token to be canceled on future additions.

[ejgallego]

We had some more discussion about this and the plan is for SerAPI to hide this internal admitted stateid. Thus, when you refocus, and later add, SerAPI will take care of handling the special case of adding just after a special admitted node.

[gares]

Hum, I think you can just "add" the Qed, no need to complete the proof. An unfinished proof is a broken proof that is syntactically complete. The Qed gets no new state id (IIRC).

[gares]

It is like commenting out all the text between the last added sentence in the re-opened proof and the Qed, add the Qed, re-open another proof.

[ejgallego]

Interesting, thanks Enrico.