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

We also tweak the VM options so they are correct.

.github/workflows/build.yml

@@ -116,21 +116,34 @@ jobs:
       - name: 🐫🐪🐫 Get dependencies
         run: |
           opam exec -- make opam-deps
-          opam pin add js_of_ocaml --dev -y
-          opam pin add js_of_ocaml-compiler --dev -y
+          opam pin add js_of_ocaml-compiler https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y
+          opam pin add js_of_ocaml https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y
           opam install zarith_stubs_js js_of_ocaml-ppx -y
 
       - name: 💉💉💉 Patch Coq
         run: make patch-for-js
 
       - name: 🦏🧱🦏 Build coq-lsp JS version 🦏🦏🦏
-        run: opam exec -- make js
+        run: |
+          opam exec -- make controller-js/coq-fs-core.js
+          opam exec -- make js
+
+      - name: 🦏🧱🦏 Build coq-lsp VSCode extension 🦏🦏🦏
+        uses: actions/setup-node@v4
+        with:
+          node-version: 22
+        run: opam exec -- make extension
 
       - name: Upload artifact
         uses: actions/upload-artifact@v4
         with:
           name: coq-lsp_worker and front-end
-          path: editor/code/out/
+          path: |
+            editor/code/package.json
+            editor/code/syntaxes
+            editor/code/out/
+            editor/code/coq.configuration.json
+          compression-level: 9
   build-opam:
     name: Opam dev install
     strategy:
@@ -195,7 +208,7 @@ jobs:
       - name: 🚀 Setup node
         uses: actions/setup-node@v4
         with:
-          node-version: 18
+          node-version: 22
       - run: npm ci
       - run: npx --yes @vscode/vsce ls
 

Makefile

@@ -1,3 +1,5 @@
+SHELL := /usr/bin/env bash
+
 COQ_BUILD_CONTEXT=../_build/default/coq
 
 PKG_SET= \
@@ -79,7 +81,7 @@ winconfig:
 .PHONY: js
 js: COQVM = no
 js: coq_boot
-	dune build --profile=release controller-js/coq_lsp_worker.bc.cjs
+	dune build --profile=release --display=quiet $(PKG_SET) controller-js/coq_lsp_worker.bc.cjs
 	mkdir -p editor/code/out/ && cp -a controller-js/coq_lsp_worker.bc.cjs editor/code/out/coq_lsp_worker.bc.js
 
 .PHONY: coq_boot
@@ -149,3 +151,49 @@ 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: COQVM = no
+controller-js/coq-fs-core.js: coq_boot
+	dune build --profile=release --display=quiet $(PKG_SET) etc/META.threads
+	for i in $$(find _build/install/default/lib/coq-core/plugins -name *.cma); do js_of_ocaml --dynlink $$i; done
+	for i in $$(find _build/install/default/lib/coq-lsp/serlib -wholename */*.cma); do js_of_ocaml --dynlink $$i; done
+	cd _build/install/default/lib && \
+	  js_of_ocaml build-fs -o coq-fs-core.js \
+	    $$(find coq-core/ \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \
+	    $$(find coq-lsp/  \( -wholename '*/serlib/*/*.js'  -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 '*/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

compiler/driver.ml

@@ -2,7 +2,8 @@
 let coq_init ~debug =
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
-  Coq.Init.(coq_init { debug; load_module; load_plugin })
+  let vm, warnings = (true, None) in
+  Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings })
 
 let replace_test_path exp message =
   let home_re = Str.regexp (exp ^ ".*$") in

controller-js/README.md

@@ -1,10 +1,78 @@
 ## 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.
+
+A quick recipe from the manual is:
+
+```
+$ make controller-js/coq-fs-core.js && make js
+$ npx @vscode/test-web --browser chromium --extensionDevelopmentPath=editor/code
+$ chrome localhost:3000
+```
+
+you can also download the artifacts from the CI build, and point
+`--extensionDevelopmentPath=` to the path you have downloaded the
+extension + Coq build.
+
+## 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

@@ -14,27 +14,6 @@ module LSP = Lsp.Base
 open Js_of_ocaml
 open Controller
 
-let verb = true
-
-let _coq_cma_link ~file_path =
-  let open Format in
-  (* Coq doesn't append the extension anymore when submitting this *)
-  let cmo_file = file_path ^ ".cma" in
-  if verb then eprintf "bytecode file %s requested\n%!" cmo_file;
-  try
-    let js_code = Sys_js.read_file ~name:(cmo_file ^ ".js") in
-    let js_code =
-      if String.sub js_code 0 1 = "(" then js_code
-      else "(" ^ js_code ^ ")" (* jsoo < 4.0 *)
-    in
-    (* When eval'ed, the js_code will return a closure waiting for the jsoo
-       global object to link the plugin. *)
-    Ok Js.Unsafe.((eval_string js_code : < .. > Js.t -> unit) global)
-  with Sys_error _ ->
-    eprintf "!! bytecode file %s{,.js} not found in path. DYNLINK FAILED\n%!"
-      cmo_file;
-    Error cmo_file
-
 let rec obj_to_json (cobj : < .. > Js.t) : Yojson.Safe.t =
   let open Js in
   let open Js.Unsafe in
@@ -71,25 +50,16 @@ 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 lib_fs ~prefix:_ ~path =
-  match path with
-  | "findlib.conf" -> Some findlib_conf
-  | _ -> None
+let findlib_conf = "\ndestdir=\"/static/lib\"path=\"/static/lib\""
 
 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;
   ()
 
 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) =
@@ -156,10 +126,34 @@ let on_init ~io ~root_state ~cmdline ~debug msg =
       in
       ignore (setTimeout (process_queue ~state) 0.1))
 
+let time f x =
+  let time = Sys.time () in
+  let res = f x in
+  let time_new = Sys.time () in
+  Format.eprintf "loadfile [dynlink] took: %f seconds%!" (time_new -. time);
+  res
+
+let loadfile file =
+  let file_js = Filename.remove_extension file ^ ".js" in
+  if Sys.file_exists file_js then (
+    Format.eprintf "loadfile [eval_js]: %s%!" file;
+    let js_code = Sys_js.read_file ~name:file_js in
+    let js_code =
+      Format.asprintf "(function (globalThis) { @[%s@] })" js_code
+    in
+    Js.Unsafe.((eval_string js_code : < .. > Js.t -> unit) global))
+  else (
+    (* Not precompiled *)
+    Format.eprintf "loadfile [dynlink]: %s%!" file;
+    time Dynlink.loadfile file)
+
 let coq_init ~debug =
-  let load_module = Dynlink.loadfile in
-  let load_plugin = Coq.Loader.plugin_handler None in
-  Coq.Init.(coq_init { debug; load_module; load_plugin })
+  let loader = My_dynload.load_packages ~debug:false ~loadfile in
+  let load_module = loadfile in
+  let load_plugin = Coq.Loader.plugin_handler (Some loader) in
+  (* XXX: Fixme at some point? *)
+  let vm, warnings = (false, Some "-vm-compute-disabled") in
+  Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings })
 
 external coq_vm_trap : unit -> unit = "coq_vm_trap"
 
@@ -181,24 +175,42 @@ let main () =
   let io = CB.cb in
   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 stdlib coqlib =
+    let unix_path = Filename.concat coqlib "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 user_contrib coqlib =
+    let unix_path = Filename.concat coqlib "user-contrib" in
+    let coq_path = Names.DirPath.empty in
+    Loadpath.
+      { unix_path
+      ; coq_path
+      ; implicit = false
+      ; has_ml = false
+      ; recursive = true
+      }
+  in
+
   let cmdline =
+    (* Needs overriding as otherwise will use the setting of the
+       compilation context, see if /static/findlib.conf is right *)
+    let ocamlpath = Some "/static/lib" in
+    let coqlib = "/static/coqlib" in
+    let vo_load_path = List.map (fun f -> f coqlib) [ stdlib; user_contrib ] in
     Coq.Workspace.CmdLine.
-      { coqlib = "/static/coq"
-      ; coqcorelib = "/static/coq"
-      ; ocamlpath = Some "/lib"
-      ; vo_load_path = [ stdlib ]
+      { coqlib
+      ; coqcorelib = "/static/lib/coq-core" (* deprecated upstream *)
+      ; ocamlpath
+      ; vo_load_path
       ; 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);