Emilio Jesús Gallego Arias

jsoo = js_of_ocaml , this is relevant because we currently have a jsoo backend and a wasm backend We haven't still decided what will the relationship between jsCoq and `coq-lsp`...

Thanks for the kind words @herbelin , I'm just stating the current state of affairs so indeed everyone can plan accordingly their time investments. There are many people interesting in...

> @ejgallego the default branch seems to be 8.17+lsp, but IMO it is not really functional - so unless there are any plans to revive it perhaps we should fall...

> After you have built a working jsCoq with 8.20 you can try to port the v8.17+lsp branch as well. I do hope it does not require changes to the...

In fact the local branch in my computer had already a port of the 8.17+lsp branch to latest (0.2.0) Flèche. I did also push a branch 8.20+lsp to this repos,...

Did some quick testing, stubs and patches needed update, used the ones in coq-lsp repos; @herbelin it would be good to compare those with your updates. Also Dune is still...

> > @herbelin it would be good to compare those with your updates > > My changes are in https://github.com/herbelin/jscoq/tree/v8.20bis. Does not seem directly related to yours. Thanks for the...

8.20 branch updated, it compiles fine, but when running it I get: ``` Doc.create, internal error: Anomaly "File "_vendor+v8.20+32bit/coq/lib/objFile.ml", line 110, characters 11-17: Assertion failed." ``` when loading the first...

Did some more experiments, things work fine with Flèche 0.1.7 and jsoo 4.0.0. So we have two problems: - port to Flèche 0.2.0 broke plugin loading, this is easy to...

I have good news! Actually the plugin loading error was due to our tooling for some reason not correctly generating the `.cma.js` files, once I went back to JSOO 4.0.0,...