Emilio Jesús Gallego Arias

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...

Great, I'll have a look!

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...

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...

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...

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!

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

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

If I do: ``` lisp $ 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 :=...

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...