[js] Build working filesystem for findlib-based worker.

We hook `loadfile` to use precompiled `.cma.js` files, using our copy
of findlib. The build is very rustical, but works.

Makefile

@@ -149,3 +149,46 @@ opam-update-and-reinstall:
 patch-for-js:
 	cd vendor/coq && patch -p1 < ../../etc/0001-coq-lsp-patch.patch
 	cd vendor/coq && patch -p1 < ../../etc/0001-jscoq-lib-system.ml-de-unix-stat.patch
+
+OPAMROOT=$(shell opam var lib)
+
+# Super-hack
+controller-js/coq-fs-core.js:
+	cd _build/install/default/lib && \
+	  js_of_ocaml build-fs -o coq-fs-core.js \
+	    $$(find coq-core/ -wholename '*/plugins/*/*.cma' -printf "%p:/static/lib/%p " -or -wholename '*/META' -printf "%p:/static/lib/%p ") \
+	    $$(find coq-lsp/ -wholename '*/serlib/*/*.cma' -printf "%p:/static/lib/%p " -or -wholename '*/META' -printf "%p:/static/lib/%p ") \
+	    ../../../../etc/META.threads:/static/lib/threads/META \
+	    $$(find $(OPAMROOT) -wholename '*/str/META'                 -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/seq/META'                 -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/uri/META'                 -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/base/META'                -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/unix/META'                -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/zarith/META'              -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/yojson/META'              -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/findlib/META'             -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/dynlink/META'             -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/parsexp/META'             -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/sexplib/META'             -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/sexplib/META'             -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/sexplib0/META'            -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/bigarray/META'            -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/cmdliner/META'            -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/ppx_hash/META'            -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/angstrom/META'            -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/stringext/META'           -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/ppx_compare/META'         -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/ppx_deriving/META'        -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/ppx_sexp_conv/META'       -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/memprof-limits/META'      -printf "%p:/static/lib/%P ") \
+	    $$(find $(OPAMROOT) -wholename '*/ppx_deriving_yojson/META' -printf "%p:/static/lib/%P ")
+	    # These libs are actually linked, so no cma is needed.
+	    # $$(find $(OPAMROOT) -wholename '*/zarith/*.cma'         -printf "%p:/static/lib/%P " -or -wholename '*/zarith/META'         -printf "%p:/static/lib/%P ")
+	cp _build/install/default/lib/coq-fs-core.js controller-js
+
+# Serlib plugins require:
+#   ppx_compare.runtime-lib
+#   ppx_deriving.runtime
+#   ppx_deriving_yojson.runtime
+#   ppx_hash.runtime-lib
+#   ppx_sexp_conv.runtime-lib

controller-js/README.md

@@ -1,10 +1,66 @@
 ## coq-lsp Web Worker README
 
 This directory contains the implementation of our LSP-compliant web
-worker for Coq / coq-lsp.
+worker for Coq, based on jsCoq.
 
 As you can see the implementation is minimal, thanks to proper
 abstraction of the core of the controller.
 
 For now it is only safe to use the worker in 32bit OCaml mode.
 
+Support for this build is still experimental. See [the javascript
+compilation
+meta-issue](https://github.com/ejgallego/coq-lsp/issues/833) for more
+information.
+
+## Building the Worker
+
+The worker needs two parts to work:
+
+- the worker binary
+- the worker filesystem
+
+which are then bundled in a single `.js` file.
+
+Type
+
+```
+make controller-js/coq-fs-core.js && make js
+```
+to build the worker filesystem and the worker, which will be placed under `editor/code/out`.
+
+As of now the build is very artisanal and not flexible at all, we hope to improve it soon.
+
+## Testing the worker
+
+You can test the server using any of the [official methods](https://code.visualstudio.com/api/extension-guides/web-extensions#test-your-web-extension).
+
+Using the regular setup `dune exec -- code editor/code` and then
+selecting "Web Extension" in the run menu works out of the box.
+
+## COI
+
+As of Feb 2023, due to security restrictions, you may need to either:
+
+ - pass `--enable-coi` to `code`
+ - use ``?enable-coi=` in the vscode dev setup
+
+in order to have interruptions (`SharedBufferArray`) working.
+
+See https://code.visualstudio.com/updates/v1_72#_towards-cross-origin-isolation
+
+## WASM
+
+We hope to have a WASM backend working soon, based on waCoq, see
+https://github.com/microsoft/vscode-wasm
+
+## Filesystem layout
+
+We need to have most `META` files in findlib, plus the Coq and
+`coq-lsp.serlib.*` plugins. These should be precompiled.
+
+- `/static/lib`: OCaml findlib root
+- `/static/coqlib`: Coq root, with regular paths
+  + `/static/coqlib/theories`
+  + `/static/coqlib/user-contrib`
+

controller-js/coq_lsp_worker.ml

@@ -71,25 +71,23 @@ let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t =
   | `Tuple t -> Array.(Js.array @@ map ofresh (of_list t))
   | `Variant (_, _) -> pure_js_expr "undefined"
 
-let findlib_conf = "\ndestdir=\"/lib\"path=\"/lib\""
+let findlib_conf = "\ndestdir=\"/static/lib\"path=\"/static/lib\""
 
-let lib_fs ~prefix:_ ~path =
+let _lib_fs ~prefix:_ ~path =
   match path with
   | "findlib.conf" -> Some findlib_conf
   | _ -> None
 
 let setup_pseudo_fs () =
   (* '/static' is the default working directory of jsoo *)
   (* Sys_js.unmount ~path:"/static"; *)
-  Sys_js.mount ~path:"/lib/" lib_fs;
+  Sys_js.create_file ~name:"/static/lib/findlib.conf" ~content:findlib_conf;
+  (* Sys_js.mount ~path:"/lib/" lib_fs; *)
   ()
 
 let setup_std_printers () =
-  (* XXX Convert to logTrace? *)
-  (* Sys_js.set_channel_flusher stdout (fun msg -> post_answer (Log (Notice,
-     Pp.str @@ "stdout: " ^ msg))); *)
-  (* Sys_js.set_channel_flusher stderr (fun msg -> post_answer (Log (Notice,
-     Pp.str @@ "stderr: " ^ msg))); *)
+  Sys_js.set_channel_flusher stdout (Fleche.Io.Log.trace "stdout" "%s");
+  Sys_js.set_channel_flusher stderr (Fleche.Io.Log.trace "stderr" "%s");
   ()
 
 let post_message (msg : Lsp.Base.Message.t) =
@@ -149,6 +147,9 @@ let on_init ~io ~root_state ~cmdline ~debug msg =
     | Lsp_core.Init_effect.Exit -> (* XXX: bind to worker.close () *) ()
     | Lsp_core.Init_effect.Loop -> ()
     | Lsp_core.Init_effect.Success workspaces ->
+      Fleche.Io.Log.trace "example" "why I don't see this";
+      Format.eprintf "Hello, in static: %d@\n"
+        (Sys.readdir "/static" |> Array.length);
       Worker.set_onmessage on_msg;
       let default_workspace = Coq.Workspace.default ~debug ~cmdline in
       let state =
@@ -182,23 +183,24 @@ let main () =
   Fleche.Io.CallBack.set io;
 
   let stdlib =
-    let unix_path = "/static/coq/theories/" in
-    let coq_path = Names.(DirPath.make [ Id.of_string "Coq" ]) in
+    let unix_path = "/static/theories/" in
+    let coq_path = Names.(DirPath.make [ Id.of_string "Stdlib" ]) in
     Loadpath.
       { unix_path; coq_path; implicit = true; has_ml = false; recursive = true }
   in
 
   let cmdline =
     Coq.Workspace.CmdLine.
-      { coqlib = "/static/coq"
-      ; coqcorelib = "/static/coq"
-      ; ocamlpath = Some "/lib"
+      { coqlib = "/static/"
+      ; coqcorelib = "/static/"
+      ; ocamlpath = Some "/static/lib"
       ; vo_load_path = [ stdlib ]
       ; ml_include_path = []
-      ; require_libraries = []
-      ; args = [ "-noinit" ]
+      ; require_libraries = [ (None, "Stdlib.Init.Prelude") ]
+      ; args = [ "-noinit"; "-boot" ]
       }
   in
+
   let debug = true in
   let root_state = coq_init ~debug in
   Worker.set_onmessage (on_init ~io ~root_state ~cmdline ~debug);

controller-js/dune

@@ -10,12 +10,14 @@
    js_stub/coq_vm.js
    js_stub/coq_perf.js
    js_stub/interrupt.js
-   marshal-arch.js)
+   marshal-arch.js
+   coq-fs-core.js
+   coq-fs.js)
   (flags
    :standard
    --dynlink
    +dynlink.js
-   ; (:include .extraflags)
+   (:include .extraflags)
    ; +toplevel.js
    ; --enable
    ; with-js-error
@@ -24,13 +26,12 @@
    ; --no-inline
    ; --debug-info
    ; --source-map
-   ; no coq-fs yet
-   ; --file=coq-fs
+   ; --file=%{dep:coq-fs}
    --setenv
    PATH=/bin))
  (link_flags -linkall -no-check-prims)
  ; The old makefile set: -noautolink -no-check-prims
- (libraries zarith_stubs_js yojson controller))
+ (libraries zarith_stubs_js yojson controller js_of_ocaml-toplevel js_of_ocaml-compiler.findlib-support))
 
 (rule
  (target coq_lsp_worker.bc.cjs)
@@ -40,11 +41,28 @@
 
 (rule
  (targets marshal-arch.js)
- ; This is to inject the dep of a FS on the executable if we want.
- ; (deps coq-fs)
  (action
   (copy js_stub/marshal%{ocaml-config:word_size}.js %{targets})))
 
+(rule
+ (targets coq-fs.js)
+ (deps
+  (package coq-stdlib))
+ (action
+  (bash
+   "cd ../vendor/coq && js_of_ocaml build-fs -o ../../controller-js/coq-fs.js $(find theories -wholename 'theories/Init/*.vo' -printf '%p:/static/%p ')")))
+
+; for coq-fs-core.js
+; js_of_ocaml build-fs -o coq-fs-core.js $(find coq-core/ -wholename '*/plugins/*/*.cma' -or -wholename '*/META' -printf "%p:/lib/%p")
+
+; (rule
+;  (targets coq-fs-core.js)
+;  (deps
+;   (package coq-core))
+;  (action
+;   (bash
+;    "cd ../vendor/coq && js_of_ocaml build-fs -o ../../controller-js/coq-fs.js $(find theories -wholename 'theories/Init/*.vo' -printf '%p:/static/%p '")))
+
 ; Set debug flags if JSCOQ_DEBUG environment variable is set.
 ; (ugly, but there are no conditional expressions in Dune)
 

controller-js/my_dynload.ml

@@ -0,0 +1,54 @@
+(* Utilities for loading dynamically packages, adapted from ocamlfind,
+   until upstream merges this patch *)
+
+open Printf
+
+let load_pkg ~debug ~loadfile pkg =
+  if not (Findlib.is_recorded_package pkg) then (
+     if debug then
+       eprintf "[DEBUG] Fl_dynload: about to load: %s\n%!" pkg;
+     (* Determine the package directory: *)
+     let d = Findlib.package_directory pkg in
+     (* First try the new "plugin" variable: *)
+     let preds = Findlib.recorded_predicates() in
+     let archive =
+       try
+         Findlib.package_property preds pkg "plugin"
+       with
+         | Not_found ->
+              (* Legacy: use "archive" but require that the predicate
+                 "plugin" is mentioned in the definition
+               *)
+              try
+                let v, fpreds =
+                  Findlib.package_property_2 ("plugin"::preds) pkg "archive" in
+                let need_plugin =
+                  List.mem "native" preds in
+                if need_plugin && not (List.mem (`Pred "plugin") fpreds) then
+                  ""
+                else
+                  v
+              with Not_found -> "" in
+     (* Split the plugin/archive property and resolve the files: *)
+     let files = Fl_split.in_words archive in
+     if debug then
+       eprintf "[DEBUG] Fl_dynload: files=%S\n%!" archive;
+     List.iter
+       (fun file ->
+          if debug then
+            eprintf "[DEBUG] Fl_dynload: loading %S\n%!" file;
+          let file = Findlib.resolve_path ~base:d file in
+          loadfile file
+       ) files;
+     Findlib.record_package Findlib.Record_load pkg
+  )
+  else
+    if debug then
+      eprintf "[DEBUG] Fl_dynload: not loading: %s\n%!" pkg
+
+
+let load_packages ?(debug=false) ?(loadfile=Dynlink.loadfile) pkgs =
+  let preds = Findlib.recorded_predicates() in
+  let eff_pkglist =
+    Findlib.package_deep_ancestors preds pkgs in
+  List.iter (load_pkg ~debug ~loadfile) eff_pkglist

controller-js/my_dynload.mli

@@ -0,0 +1 @@
+val load_packages : ?debug:bool -> ?loadfile:(string -> unit) -> string list -> unit

etc/META.threads

@@ -0,0 +1,37 @@
+# Specifications for the "threads" library:
+version = "[distributed with Ocaml]"
+description = "Multi-threading"
+requires(mt,mt_vm) = "threads.vm"
+# requires(mt,mt_posix) = "threads.posix"
+directory = "^"
+type_of_threads = "posix"
+
+browse_interfaces = ""
+
+warning(-mt) = "Linking problems may arise because of the missing -thread or -vmthread switch"
+warning(-mt_vm,-mt_posix) = "Linking problems may arise because of the missing -thread or -vmthread switch"
+
+package "vm" (
+  # --- Bytecode-only threads:
+  requires = "unix"
+  directory = "+vmthreads"
+  exists_if = "threads.cma"
+  archive(byte,mt,mt_vm) = "threads.cma"
+  version = "[internal]"
+)
+
+package "posix" (
+  # --- POSIX-threads:
+  requires = "unix"
+  directory = "+threads"
+  exists_if = "threads.cma"
+  archive(byte,mt,mt_posix) = "threads.cma"
+  archive(native,mt,mt_posix) = "threads.cmxa"
+  version = "[internal]"
+)
+
+package "none" (
+  error = "threading is not supported on this platform"
+  version = "[internal]"
+)
+