Enable Async support in SerAPI. about coq-serapi HOT 32 CLOSED

a5b5bf9 added some preliminary flags.

from coq-serapi.

I don't quite understand it either.

There seem to be many flags:

https://github.com/coq/coq/blob/trunk/toplevel/coqtop.ml#L493

-async-proofs on seems like the first step.

from coq-serapi.

Yeah I tried to imitate that, but I'm kind of doing things blindly here 💃

from coq-serapi.

This script https://github.com/coq/coq/blob/trunk/test-suite/interactive/proof_block.v seems to be processed asynchronously now. YMMV.

from coq-serapi.

Ok I did some more changes and arrived to this:

(Control (StmObserve 22))
....
sertop: unknown option `-m'.
Usage: sertop [OPTION]... 
Try `sertop --help' for more information.
(Feedback ...
     "Anomaly: Uncaught exception (Failure \"The spawned process did not connect back in 2.0s\").\
    \nPlease report.")))

So indeed this looks promising! We just need to instruct the Stm not to call sertop but the regular coqtop for child processes.

from coq-serapi.

Hey Emilio,

Pretty cool :) Things seem to be going very nicely.
Question: after compiling the latest build and passing async, I can see states being processed in parallel, but I'm not getting feedback for states inside of a proof. Here is an example of a transcript:

(add-ltac (Control (StmAdd 1 None "Ltac slow := do 1000 (do 1000 idtac).")))
  (Answer add-ltac Ack)
  (Answer add-ltac
          (StmAdded 3
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 0)
                     (ep 37))
                    NewTip))
  (Answer add-ltac Completed)
(add-lemma (Control (StmAdd 2 (Some 3) "Lemma a : True. Proof.")))
  (Answer add-lemma Ack)
  (Answer add-lemma
          (StmAdded 4
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 0)
                     (ep 15))
                    NewTip))
  (Answer add-lemma
          (StmAdded 5
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 16)
                     (ep 22))
                    NewTip))
  (Answer add-lemma Completed)
(add-proof (Control (StmAdd 4 (Some 5) "slow. slow. slow. auto.")))
  (Answer add-proof Ack)
  (Answer add-proof
          (StmAdded 6
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 0)
                     (ep 5))
                    NewTip))
  (Answer add-proof
          (StmAdded 7
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 6)
                     (ep 11))
                    NewTip))
  (Answer add-proof
          (StmAdded 8
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 12)
                     (ep 17))
                    NewTip))
  (Answer add-proof
          (StmAdded 9
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 18)
                     (ep 23))
                    NewTip))
  (Answer add-proof Completed)
(add-qed (Control (StmAdd 2 (Some 9) "Qed.")))
  (Answer add-qed Ack)
  (Answer add-qed
          (StmAdded 10
                    ((fname "")
                     (line_nb 1)
                     (bol_pos 0)
                     (line_nb_last 1)
                     (bol_pos_last 0)
                     (bp 0)
                     (ep 4))
                    NewTip))
  (Answer add-qed Completed)
(Control (StmObserve 10))
  (Answer 4 Ack)
  (Feedback
   ((id
     (State 10))
    (contents
     (ProcessingIn master))
    (route 0)))
  (Feedback
   ((id
     (State 5))
    (contents
     (ProcessingIn master))
    (route 0)))
  (Feedback
   ((id
     (State 4))
    (contents
     (ProcessingIn master))
    (route 0)))
  (Feedback
   ((id
     (State 3))
    (contents
     (ProcessingIn master))
    (route 0)))
  (Feedback
   ((id
     (State 2))
    (contents Processed)
    (route 0)))
  (Feedback
   ((id
     (State 3))
    (contents
     (Message Info
              (Element
               (_ nil
                  ((PCData "slow is defined"))))))
    (route 0)))
  (Feedback
   ((id
     (State 3))
    (contents Processed)
    (route 0)))
  (Feedback
   ((id
     (State 4))
    (contents Processed)
    (route 0)))
  (Feedback
   ((id
     (State 5))
    (contents Processed)
    (route 0)))
  (Feedback
   ((id
     (State 5))
    (contents Processed)
    (route 0)))
  (Feedback
   ((id
     (State 4))
    (contents Processed)
    (route 0)))
  (Feedback
   ((id
     (State 10))
    (contents
     (Message Info
              (Element
               (_ nil
                  ((PCData "a is defined"))))))
    (route 0)))
  (Feedback
   ((id
     (State 10))
    (contents Incomplete)
    (route 0)))
  (Feedback
   ((id
     (State 10))
    (contents Processed)
    (route 0)))
  (Answer 4 Completed)

Although I get a message from state 10 saying that a is defined, I don't get anything for states 6, 7, 8, 9 (the ones inside the Proof .. Qed block). Am I doing something wrong?

from coq-serapi.

Data point: apparently it works if I call observe separately on the last state of each proof.

from coq-serapi.

Cool ! :) Here we are walking a bit on unexplored territory, it will be hard to figure things out if we cannot get @gares on board :)

A guess, does using the Join method change things?

from coq-serapi.

Also a good reference is to use CoqIde an see how it behaves. The mapping roughly is:

• Go to point icon: Add the document up to point, does Observe in the tip of the Stm.
• Gears icon: does Join on the document.

from coq-serapi.

Ok; let me try join :) Can you reproduce the thing I'm seeing in the example above btw?

from coq-serapi.

I see exactly what you see. Plus if I do join:

(Control StmJoin)
(Answer 5 Ack)
(Feedback ((id (State 10)) (contents Processed) (route 0)))
(Feedback ((id (State 9)) (contents (ProcessingIn master)) (route 0)))
(Feedback ((id (State 8)) (contents (ProcessingIn master)) (route 0)))
(Feedback ((id (State 7)) (contents (ProcessingIn master)) (route 0)))
(Feedback ((id (State 6)) (contents (ProcessingIn master)) (route 0)))
(Feedback ((id (State 5)) (contents Processed) (route 0)))
(Feedback ((id (State 6)) (contents Processed) (route 0)))
(Feedback ((id (State 7)) (contents Processed) (route 0)))
(Feedback ((id (State 8)) (contents Processed) (route 0)))
(Feedback ((id (State 9)) (contents Processed) (route 0)))
(Feedback ((id (State 10)) (contents Complete) (route 0)))
(Answer 5 Completed)

from coq-serapi.

Cool, thanks. Implemented Join in cpitclaudel/elcoq@17c73f1. It seems to only process the last proof though (that is, if there are, say, 10 closed proofs, it just observes the last closed one).

https://asciinema.org/a/cqmk80fnyfn26xlvcmu9ttf61

from coq-serapi.

Great, I'll have a look!

from coq-serapi.

Wow it is beautiful !!! wrt to the join, indeed when you join the Stm goes backwards on the document (I have no clue if there is any reason for that), the moment it finds an error, it stops.

This is due to join checking the whole document I think, it really checks that the proofs the worker generated are right and this needs to be done somehow in a single threaded fashion to still ensure consistency wrt the kernel.

from coq-serapi.

I guess that it depends on the interpretation we do of the feedback messages, I see in this example you get a few Incomplete messages. This may indicate that the STM is being very very lazy....

But somehow I'm seeing now a different parallelism than before. I wonder why.

from coq-serapi.

Wow it is beautiful !!!

Thanks 😊

from coq-serapi.

Now workers are created again, there was a problem with the ordering of flag-setting. I've chosen a conservative flag setup: SerAPI imitates CoqIDE. Feel free to play thou with the flags in sertop_init.ml and in particular with setting async_proofs_full back to true.

from coq-serapi.

Note however that there is a race condition in printing. I have no clue how to the workers send the feedback messages so I'll have to look into it!

from coq-serapi.

Did you use a mutex as CoqIDE?
https://github.com/coq/coq/blob/trunk/ide/ide_slave.ml#L467

from coq-serapi.

Sorry, I did not see the commit. IIRC It is needed because the Stm uses 1 thread per worker, and feedback coming from workers is forwarded. A thread may be interrupted while sending a XML tree, hence you need the mutex. The feeder code is called by the thread.

from coq-serapi.

Now that I think about it, I guess the proper place for the mutex is Pp.feedback ...

from coq-serapi.

@gares IMHO it is not so bad to require clients to assume a re-entrant callback, but it should be documented of course.

from coq-serapi.

Catching up with this thread. Stm.finish is like observing the tip (what the "satus false" XML message does, IIRC); while Stm.join also joins the environment ("status true" in XML) that means all proof terms produced by workers are type-checked by the kernel of main Coqtop and all universe constraints are also checked. A worker typechecks in his corner the proof term, but 1) I don't want to trust workers, 2) only the main coqtop has a complete view and can check universes (a worker alone can only check satisfiability locally to his constraints).

Both calls are blocking, but the latter waits for a complete checking of everything, while the former does not wait for delegated proofs (as GoTo-Point in CoqIDE).

from coq-serapi.

Thanks Enrico! Note that Stm.join seems broken for me when using --async_full. Are we missing something there?

from coq-serapi.

I think it is untested, since Coqoon has no join buttun. But should work (I see no if async_proofs_full in the code path). Broken in which way.

from coq-serapi.

If I do:

$ rlwrap ./sertop.native --human --prelude ~/external/coq-git --async ~/external/coq-git/bin/coqtop --async-full
(Control (StmAdd 100 None "
Ltac slow := do 1000 (do 1000 idtac).
Ltac wrong := intro.

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

Lemma b: True.
Proof. slow. slow. slow. auto. Qed.

Lemma c: True.
Proof. slow. slow. slow. auto. Qed.

Lemma d: True.
Proof. slow. slow. slow.
"))
(Control StmJoin)

master never responds again, it seems hung. Of course, it could well be a SerAPI bug.

from coq-serapi.

Hum, I guess you need to observe the tip first... I can't say why now, I've to check.

from coq-serapi.

I guess join crawls the document for futures, but nobody scheduled them... observe does.

from coq-serapi.

It is a combination CoqIDE does not let you do, since adds are always followed by observe.

from coq-serapi.

We do an observe first, but something seems to be going on... We need to investigate more. Somehow with our --async-full we are getting very strange things.

It is a combination CoqIDE does not let you do, since adds are always followed by observe.

I see, thanks, we do n adds one observe; with usual CoqIDE mode it seems to work well.

from coq-serapi.

By the way, I'd swear that I witnessed a race condition just now: somehow, after an observe that triggered async checking, a worker produced a spurious error! Interesting!

from coq-serapi.

We don't plan to support STM-specific features.

from coq-serapi.