You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Not clear if we want to patch Coq (could be tricky due to current code ignoring special files), or patch JSOO, which could be complex, or just stub Unix.stat enough for Coq code to work. Seems like the latest would be our preferred option, as upstream use of Unix.stat is also due to non-regular files.
Coq uses findlib'sFl_dynload to load plugins, which we override to use our own, cache-aware .cma loader. Patch can be dropped once [fl_dynload] Allow overriding low-level module loader ocaml/ocamlfind#81 is merged. Note that our current scheme requires pre-compilation of all .cma to .js, however using Dynlink.loadfile would also work in JSOO, but it is quite slow in general. A combination of our cache method with JSOO Dynlink seems to fail trivially, but that would also be a nice option, but increases the worker size by 3MiB as we need to bundle JSOO.
[minor] we need to patch threads/META as to avoid lack of threads on JSOO
The text was updated successfully, but these errors were encountered:
#433 added a Web Worker for
coq-lsp
that is compatible with code Web Extensions.The Web Worker is runnable by downloading the artifact directly from our CI, see the README at
controller-js
.However, there are some upstream issues that we'd like to get fixed as to make the worker better supported:
Coq uses
Unix.stat
when scanning for theories, however JSOO doesn't support it for our FS, see Unix.stat on autoloaded files ocsigen/js_of_ocaml#650Not clear if we want to patch Coq (could be tricky due to current code ignoring special files), or patch JSOO, which could be complex, or just stub
Unix.stat
enough for Coq code to work. Seems like the latest would be our preferred option, as upstream use ofUnix.stat
is also due to non-regular files.Coq uses
findlib's
Fl_dynload
to load plugins, which we override to use our own, cache-aware.cma
loader. Patch can be dropped once [fl_dynload] Allow overriding low-level module loader ocaml/ocamlfind#81 is merged. Note that our current scheme requires pre-compilation of all.cma
to.js
, however usingDynlink.loadfile
would also work in JSOO, but it is quite slow in general. A combination of our cache method with JSOODynlink
seems to fail trivially, but that would also be a nice option, but increases the worker size by 3MiB as we need to bundle JSOO.[minor] we need to patch
threads/META
as to avoid lack ofthreads
on JSOOThe text was updated successfully, but these errors were encountered: