[controller] [js] Initial javascript JSSO coq-lsp controller

Bootstrapped and working!

DONE:

 - interrupt support
 - 32bit compilation without hacks
 - CI + artifact

TODO:

  minimal package manager:
  + try to load .vo files
  + hand write dune files for cma and coq-pkg for the prelude
  + bind jszip or some other zip lib
  + fetch package prelude.coq-pkg, unzip and register

TODOS:

  - WASM
  - Package manager (v3)
  - jsCoq SDK (v2)

CONTRIBUTING.md

@@ -255,6 +255,11 @@ ideal would be for LSP clients to catch up and allow UTF-8 encodings
 (so no conversion is needed, at least for Coq), but it seems that we
 will take a while to get to this point.
 
+## Worker version (and debugging tips)
+
+See https://github.com/ocsigen/js_of_ocaml/issues/410 for debugging
+tips with `js_of_ocaml`.
+
 ## Client guide (VS Code Extension)
 
 The VS Code extension is setup as a standard `npm` Typescript + React package

Makefile

@@ -47,6 +47,8 @@ build-all: coq_boot
 vendor/coq:
 	$(error Submodules not initialized, please do "make submodules-init")
 
+COQVM=yes
+
 # We set -libdir due to a Coq bug on win32, see
 # https://github.com/coq/coq/pull/17289 , this can be removed once we
 # drop support for Coq 8.16
@@ -55,6 +57,7 @@ vendor/coq/config/coq_config.ml: vendor/coq
 	&& cd vendor/coq \
 	&& ./configure -no-ask -prefix "$$EPATH/_build/install/default/" \
 	        -libdir "$$EPATH/_build/install/default/lib/coq" \
+	        -bytecode-compiler $(COQVM) \
 		-native-compiler no \
 	&& cp theories/dune.disabled theories/dune \
 	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
@@ -72,6 +75,13 @@ winconfig:
 	&& cp theories/dune.disabled theories/dune \
 	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
 
+
+.PHONY: js
+js: COQVM = no
+js: coq_boot
+	dune build --profile=release 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
 coq_boot: vendor/coq/config/coq_config.ml
 

controller-js/README.md

@@ -0,0 +1,10 @@
+## coq-lsp Web Worker README
+
+This directory contains the implementation of our LSP-compliant web
+worker for Coq / coq-lsp.
+
+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.
+

controller-js/coq_lsp_worker.ml

@@ -0,0 +1,207 @@
+(* Coq JavaScript API.
+ *
+ * Copyright (C) 2016-2019 Emilio J. Gallego Arias, Mines ParisTech, Paris.
+ * Copyright (C) 2018-2023 Shachar Itzhaky, Technion
+ * Copyright (C) 2019-2023 Emilio J. Gallego Arias, INRIA
+ * LICENSE: GPLv3+
+ *
+ * We provide a message-based asynchronous API for communication with
+ * Coq.
+ *)
+
+module U = Yojson.Safe.Util
+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
+  let typeof_cobj = to_string (typeof cobj) in
+  match typeof_cobj with
+  | "string" -> `String (to_string @@ coerce cobj)
+  | "boolean" -> `Bool (to_bool @@ coerce cobj)
+  | "number" -> `Int (int_of_float @@ float_of_number @@ coerce cobj)
+  | _ ->
+    if instanceof cobj array_empty then
+      `List Array.(to_list @@ map obj_to_json @@ to_array @@ coerce cobj)
+    else if instanceof cobj Typed_array.arrayBuffer then
+      `String (Typed_array.String.of_arrayBuffer @@ coerce cobj)
+    else if instanceof cobj Typed_array.uint8Array then
+      `String (Typed_array.String.of_uint8Array @@ coerce cobj)
+    else
+      let json_string = Js.to_string (Json.output cobj) in
+      Yojson.Safe.from_string json_string
+
+let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t =
+  let open Js.Unsafe in
+  let ofresh j = json_to_obj (obj [||]) j in
+  match json with
+  | `Bool b -> coerce @@ Js.bool b
+  | `Null -> pure_js_expr "null"
+  | `Assoc l ->
+    List.iter (fun (p, js) -> set cobj p (ofresh js)) l;
+    cobj
+  | `List l -> Array.(Js.array @@ map ofresh (of_list l))
+  | `Float f -> coerce @@ Js.number_of_float f
+  | `String s -> coerce @@ Js.string s
+  | `Int m -> coerce @@ Js.number_of_float (float_of_int m)
+  | `Intlit s -> coerce @@ Js.number_of_float (float_of_string s)
+  | `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 setup_pseudo_fs () =
+  (* '/static' is the default working directory of jsoo *)
+  (* Sys_js.unmount ~path:"/static"; *)
+  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))); *)
+  ()
+
+let post_message (msg : Lsp.Base.Message.t) =
+  let json = Lsp.Base.Message.to_yojson msg in
+  let js = json_to_obj (Js.Unsafe.obj [||]) json in
+  Worker.post_message js
+
+type opaque
+
+external interrupt_setup : opaque (* Uint32Array *) -> unit = "interrupt_setup"
+
+let interrupt_is_setup = ref false
+
+let parse_msg msg =
+  if Js.instanceof msg Js.array_length then (
+    let _method_ = Js.array_get msg 0 in
+    let handle = Js.array_get msg 1 |> Obj.magic in
+    interrupt_setup handle;
+    interrupt_is_setup := true;
+    Error "processed interrupt_setup")
+  else obj_to_json msg |> Lsp.Base.Message.of_yojson
+
+let on_msg msg =
+  match parse_msg msg with
+  | Error _ ->
+    Lsp.Io.logMessage ~lvl:Lsp.Io.Lvl.Error
+      ~message:"Error in JSON RPC Message Parsing"
+  | Ok msg ->
+    (* Lsp.Io.trace "interrupt_setup" (string_of_bool !interrupt_is_setup); *)
+    Lsp_core.enqueue_message msg
+
+let setTimeout cb d = Dom_html.setTimeout cb d
+
+module CB = Controller.Lsp_core.CB (struct
+  let ofn n = Lsp.Base.Message.notification n |> post_message
+end)
+
+let rec process_queue ~state () =
+  match
+    Lsp_core.dispatch_or_resume_check ~io:CB.cb ~ofn:post_message ~state
+  with
+  | None ->
+    Fleche.Io.Log.trace "proccess queue" "ended";
+    ()
+  | Some (Yield state) -> ignore (setTimeout (process_queue ~state) 0.1)
+  (* We need to yield so [on_msg] above has the chance to run and add the
+     command(s) to the queue. *)
+  | Some (Cont state) -> ignore (setTimeout (process_queue ~state) 0.)
+
+let on_init ~io ~root_state ~cmdline ~debug msg =
+  match parse_msg msg with
+  | Error _ -> ()
+  | Ok msg -> (
+    match
+      Lsp_core.lsp_init_process ~ofn:post_message ~io ~cmdline ~debug msg
+    with
+    | Lsp_core.Init_effect.Exit -> (* XXX: bind to worker.close () *) ()
+    | Lsp_core.Init_effect.Loop -> ()
+    | Lsp_core.Init_effect.Success workspaces ->
+      Worker.set_onmessage on_msg;
+      let default_workspace = Coq.Workspace.default ~debug ~cmdline in
+      let state =
+        { Lsp_core.State.root_state; cmdline; workspaces; default_workspace }
+      in
+      ignore (setTimeout (process_queue ~state) 0.1))
+
+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 })
+
+external coq_vm_trap : unit -> unit = "coq_vm_trap"
+
+(* This code is executed on Worker initialization *)
+let main () =
+  (* This is needed if dynlink is enabled in 4.03.0 *)
+  Sys.interactive := false;
+
+  Coq.Limits.(select Coq);
+  Coq.Limits.start ();
+
+  setup_pseudo_fs ();
+  setup_std_printers ();
+
+  (* setup_interp (); *)
+  coq_vm_trap ();
+
+  Lsp.Io.set_log_fn (fun n -> Lsp.Base.Message.notification n |> post_message);
+  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
+    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"
+      ; vo_load_path = [ stdlib ]
+      ; ml_include_path = []
+      ; require_libraries = []
+      ; args = [ "-noinit" ]
+      }
+  in
+  let debug = true in
+  let root_state = coq_init ~debug in
+  Worker.set_onmessage (on_init ~io ~root_state ~cmdline ~debug);
+  ()
+
+let () = main ()

controller-js/dune

@@ -0,0 +1,59 @@
+(executable
+ (name coq_lsp_worker)
+ (modes js)
+ (preprocess
+  (pps js_of_ocaml-ppx))
+ (js_of_ocaml
+  (javascript_files
+   js_stub/mutex.js
+   js_stub/unix.js
+   js_stub/coq_vm.js
+   js_stub/coq_perf.js
+   js_stub/interrupt.js
+   marshal-arch.js)
+  (flags
+   :standard
+   --dynlink
+   +dynlink.js
+   ; (:include .extraflags)
+   ; +toplevel.js
+   ; --enable
+   ; with-js-error
+   ; --enable
+   ; debuginfo
+   ; --no-inline
+   ; --debug-info
+   ; --source-map
+   ; no coq-fs yet
+   ; --file=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))
+
+(rule
+ (target coq_lsp_worker.bc.cjs)
+ (mode promote)
+ (action
+  (copy coq_lsp_worker.bc.js coq_lsp_worker.bc.cjs)))
+
+(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})))
+
+; Set debug flags if JSCOQ_DEBUG environment variable is set.
+; (ugly, but there are no conditional expressions in Dune)
+
+(rule
+ (targets .extraflags)
+ (deps
+  (env_var JSCOQ_DEBUG))
+ (action
+  (with-stdout-to
+   %{targets}
+   (bash
+    "echo '(' ${JSCOQ_DEBUG+ --pretty --noinline --disable shortvar --debug-info} ')'"))))

controller-js/js_stub/coq_perf.js

@@ -0,0 +1,17 @@
+//Provides: CAML_init
+function CAML_init() {
+  return;
+}
+
+//Provides: CAML_peek
+//Requires: caml_int64_of_int32
+function CAML_peek() {
+  return caml_int64_of_int32(0);
+}
+
+
+//Provides: CAML_drop
+function CAML_drop() {
+  return;
+}
+