[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

@@ -113,20 +113,20 @@ nix build .?submodules=1
 This currently only applies to building the default package (coq-lsp), which is
 the server. Clients don't have specific submodules as of yet.
 
-#### Releasing
+### Releasing
 
 `coq-lsp` is released using `dune-release tag` + `dune-release`.
 
 The checklist for the release as of today is:
 
-##### Client:
+#### Client:
 
 - update the client changelog at `editor/code/CHANGELOG.md`, commit
 - for the `main` branch: `dune release tag $coq_lsp_version`
 - check with `vsce ls` that the client contents are OK
 - `vsce publish`
 
-##### Server:
+#### Server:
 
 - sync branches for previous Coq versions, using `git merge`, test and push to CI.
 - `dune release tag` for each `$coq_lsp_version+$coq_version`
@@ -163,6 +163,11 @@ Some tips:
 
 [ocamlformat]: https://github.com/ocaml-ppx/ocamlformat
 
+### Worker version (and debugging tips)
+
+See https://github.com/ocsigen/js_of_ocaml/issues/410 for debugging
+tips with `js_of_ocaml`.
+
 ## VS Code Extension guide
 
 The VS Code extension is setup as a standard `npm` type-script + 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,234 @@
+(* 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 Js_util
+open Controller
+
+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"
+
+(* This is an internal js_of_ocaml primitive... *)
+external string_bytes : string -> Typed_array.uint8Array Js.t
+  = "caml_convert_bytes_to_array"
+
+(* (following is a reference implementation) *)
+(** let string_bytes s : Typed_array.uint8Array Js.t = let ta = new%js
+    Typed_array.uint8Array (String.length s) in String.iteri (fun i c ->
+    Typed_array.set ta i (Char.code c)) s; ta *)
+
+let _post_file tag filename content : unit =
+  let open Js.Unsafe in
+  let array, buf = buffer_of_uint8array (string_bytes content) in
+  let msg =
+    Js.array
+      [| inject @@ Js.string tag
+       ; inject @@ Js.string filename
+       ; inject @@ array
+      |]
+  in
+  Js.Unsafe.global##postMessage msg (Js.array [| buf |])
+(* use `transfer` *)
+
+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";
+  (* XXX Fixme, workspace manager *)
+  (* Sys_js.mount ~path:"/static/" (fun ~prefix:_ ~path -> Jslibmng.coq_vo_req
+     path); *)
+  (* '/lib' is the target for Put commands *)
+  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))); *)
+  ()
+
+external coq_vm_trap : unit -> unit = "coq_vm_trap"
+
+let post_message (json : Yojson.Safe.t) =
+  let js = json_to_obj (Js.Unsafe.obj [||]) json in
+  Worker.post_message js
+
+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 Js_util.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 log_workspace (dir, w) =
+  let message, extra = Coq.Workspace.describe w in
+  Lsp.Io.trace "workspace" ("initialized " ^ dir) ~extra;
+  Lsp.Io.logMessage ~lvl:3 ~message
+
+let version () =
+  let dev_version =
+    match Build_info.V1.version () with
+    | None -> "N/A"
+    | Some bi -> Build_info.V1.Version.to_string bi
+  in
+  Format.asprintf "version %s, dev: %s, Coq version: %s" Version.server
+    dev_version Coq_config.version
+
+let rq_answer ~ofn ~id result =
+  (match result with
+  | Result.Ok result -> Lsp.Base.mk_reply ~id ~result
+  | Error (code, message) -> Lsp.Base.mk_request_error ~id ~code ~message)
+  |> ofn
+
+let on_init ~root_state ~cmdline ~debug msg =
+  match parse_msg msg with
+  | Ok (Lsp.Base.Message.Request { method_ = "initialize"; id; params }) ->
+    (* At this point logging is allowed per LSP spec *)
+    let message =
+      Format.asprintf "Initializing coq-lsp server %s" (version ())
+    in
+    Lsp.Io.logMessage ~lvl:3 ~message;
+    let result, dirs = Rq_init.do_initialize ~params in
+    (* Workspace initialization *)
+    let debug = debug || !Fleche.Config.v.debug in
+    let workspaces =
+      List.map (fun dir -> (dir, Coq.Workspace.guess ~cmdline ~debug ~dir)) dirs
+    in
+    List.iter log_workspace workspaces;
+    let state = { Lsp_core.State.root_state; cmdline; workspaces } in
+    Worker.set_onmessage on_msg;
+    rq_answer ~ofn:post_message ~id (Result.ok result);
+    Lsp.Io.logMessage ~lvl:3 ~message:"Server initialized";
+    ignore (setTimeout (process_queue ~state) 0.1)
+  | Ok (Lsp.Base.Message.Request { id; _ }) ->
+    (* per spec *)
+    Lsp.Base.mk_request_error ~id ~code:(-32002)
+      ~message:"server not initialized"
+    |> post_message
+  | Ok (Lsp.Base.Message.Notification { method_ = "exit"; params = _ })
+  | Error _ -> raise Lsp_core.Lsp_exit
+  | Ok (Lsp.Base.Message.Notification _) ->
+    (* We can't log before getting the initialize message *)
+    ()
+
+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)
+    }
+
+(* 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} ')'"))))