Emilio Jesús Gallego Arias

@lilred I could give you access to the tree however that wouldn't help a lot; the main issue here and where work is concentrated now is in the base Coq...

Hi @lilred , indeed I think your timeframe should work pretty well. > Can you point me to that work? Or is it not publicly accessible? Sure, I will give...

@lilred for example https://github.com/coq/coq/pull/10681 and https://github.com/coq/coq/pull/10884 and a couple other more that have not been submitted yet. See also https://github.com/coq/coq/issues/10041

Thanks @lilred , I'm unsure if there is any resource that would help right now; hopefully the situation does improve before Christmas.

a5b5bf9d5755787f9d22f1f8794f0ae94423b3d6 added some preliminary flags.

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

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

Ok I did some more changes and arrived to this: ``` lisp (Control (StmObserve 22)) .... sertop: unknown option `-m'. Usage: sertop [OPTION]... Try `sertop --help' for more information. (Feedback...

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

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