[controller] [js] Initial javascript JSSO controller

Finally bootstrapped and working!

Moreover the version of JSOO we are using is not tested.

TODO before merge:

- Interrupt
- Upstream disable uint size check to Coq

TODO after merge (turn into issues):

- WASM
- Package manager (v3) (likely for other PR)
- jsCoq SDK (v2)

CONTRIBUTING.md

@@ -69,7 +69,7 @@ Dune.
     ```
 
 2. Initialize submodules (the `main` branch uses some submodules, which we plan to get rid of soon. Branches `v8.x` can already skip this step.)
-  
+
     ```sh
     make submodules-init
     ```
@@ -85,7 +85,7 @@ Alternatively, you can also use the regular `dune build @check` etc... targets.
 
 #### Nix
 
-We have a Nix flake that you can use. 
+We have a Nix flake that you can use.
 
 1. Dependencies: for development it suffices to run `nix develop` to spawn a shell with the corresponding dependencies.
 
@@ -100,7 +100,7 @@ We have a Nix flake that you can use.
     ```
 
 2. Initialize submodules (the `main` branch uses some submodules, which we plan to get rid of soon. Branches `v8.x` can already skip this step.)
-  
+
     ```sh
     make submodules-init
     ```
@@ -154,7 +154,7 @@ Some tips:
 
 [ocamlformat]: https://github.com/ocaml-ppx/ocamlformat
 
-### Releasing
+## Releasing
 
 `coq-lsp` is released using `dune-release tag` + `dune-release`.
 
@@ -175,6 +175,11 @@ The checklist for the release as of today is the following:
 - [optional] update pre-release packages to coq-opam-archive
 - [important] bump `version.ml` and `package.json` version string
 
+## 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

@@ -41,11 +41,17 @@ watch: coq_boot
 build-all: coq_boot
 	dune build $(DUNEOPT) @all
 
+.PHONY: js
+js:
+	dune build --profile=release controller-js/coq_lsp_worker.bc.cjs
+	cp controller-js/coq_lsp_worker.bc.cjs editor/code/out/coq_lsp_worker.bc.js
+
 # We set -libdir due to a Coq bug on win32, see https://github.com/coq/coq/pull/17289
 vendor/coq/config/coq_config.ml:
 	cd vendor/coq \
 	&& ./configure -no-ask -prefix $(shell pwd)/_build/install/default/ \
 	        -libdir $(shell pwd)/_build/install/default/lib/coq \
+	        -bytecode-compiler no \
 		-native-compiler no \
 	&& cp theories/dune.disabled theories/dune \
 	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune

controller-js/coq_lsp_worker.ml

@@ -0,0 +1,189 @@
+(* Coq JavaScript API.
+ *
+ * Copyright (C) 2016-2019 Emilio J. Gallego Arias, Mines ParisTech, Paris.
+ * Copyright (C) 2018-2021 Shachar Itzhaky, Technion
+ * Copyright (C) 2019-2021 Emilio J. Gallego Arias, INRIA
+ * LICENSE: GPLv3+
+ *
+ * We provide a message-based asynchronous API for communication with
+ * Coq.
+ *)
+
+module U = Yojson.Safe.Util
+module LIO = Lsp.Io
+module LSP = Lsp.Base
+open Js_of_ocaml
+open Controller
+
+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 (json : Yojson.Safe.t) =
+  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.from_yojson
+
+let on_msg msg =
+  match parse_msg msg with
+  | Error _ ->
+    Lsp.Io.logMessage ~lvl:1 ~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
+
+let rec process_queue ~state () =
+  match Lsp_core.dispatch_or_resume_check ~ofn:post_message ~state with
+  | None ->
+    LIO.trace "proccess queue" "ended";
+    ()
+  | Some (Yield state) -> ignore (setTimeout (process_queue ~state) 0.1)
+  | Some (Cont state) -> process_queue ~state ()
+
+let on_init ~root_state ~cmdline ~debug msg =
+  match parse_msg msg with
+  | Error _ -> ()
+  | Ok msg -> (
+    match Lsp_core.lsp_init_process ~ofn:post_message ~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 state = { Lsp_core.State.root_state; cmdline; workspaces } in
+      ignore (setTimeout (process_queue ~state) 0.1))
+
+let lvl_to_severity (lvl : Feedback.level) =
+  match lvl with
+  | Feedback.Debug -> 5
+  | Feedback.Info -> 4
+  | Feedback.Notice -> 3
+  | Feedback.Warning -> 2
+  | Feedback.Error -> 1
+
+let add_message lvl loc msg q =
+  let lvl = lvl_to_severity lvl in
+  q := (loc, lvl, msg) :: !q
+
+let mk_fb_handler q Feedback.{ contents; _ } =
+  match contents with
+  | Message (lvl, loc, msg) -> add_message lvl loc msg q
+  | _ -> ()
+
+let coq_init ~fb_queue ~debug =
+  let fb_handler = mk_fb_handler fb_queue in
+  let load_module = Dynlink.loadfile in
+  let load_plugin = Coq.Loader.plugin_handler None in
+  Coq.Init.(coq_init { fb_handler; debug; load_module; load_plugin })
+
+let lsp_cb =
+  Fleche.Io.CallBack.
+    { trace = Lsp.Io.trace
+    ; send_diagnostics =
+        (fun ~ofn ~uri ~version diags ->
+          Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn)
+    ; send_fileProgress =
+        (fun ~ofn ~uri ~version progress ->
+          Lsp.JFleche.mk_progress ~uri ~version progress |> ofn)
+    }
+
+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;
+
+  setup_pseudo_fs ();
+  setup_std_printers ();
+
+  (* setup_interp (); *)
+  coq_vm_trap ();
+
+  Lsp.Io.set_log_fn post_message;
+  Fleche.Io.CallBack.set lsp_cb;
+
+  let cmdline =
+    Coq.Workspace.CmdLine.
+      { coqlib = "/lib/coq"
+      ; coqcorelib = "/lib/coq"
+      ; ocamlpath = Some "/lib"
+      ; vo_load_path = []
+      ; ml_include_path = []
+      ; args = [ "-noinit" ]
+      }
+  in
+  let debug = true in
+  let fb_queue = Coq.Protect.fb_queue in
+  let root_state = coq_init ~fb_queue ~debug in
+  Worker.set_onmessage (on_init ~root_state ~cmdline ~debug);
+  ()
+
+let () = main ()

controller-js/dune

@@ -0,0 +1,54 @@
+(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/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
+   --setenv
+   PATH=/bin))
+ (link_flags -linkall -no-check-prims)
+ ; The old makefile set: -noautolink -no-check-prims
+ (libraries zarith_stubs_js js_of_ocaml-lwt 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)
+ (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} ')'"))))