Enrico Tassi

the problem is that elpi links ppx stuff, which is also linked by serapi. Use 4.07 for generating the doc :-/ which tolerates double linking of the same module. We...

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

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

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

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

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.

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

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

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

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