From 2a46a7d174d96da405b653d982c44e506441eb6d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 27 Sep 2024 00:43:19 +0200 Subject: [PATCH] [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 | 43 ++++++++++++++++++++++++ controller-js/README.md | 58 ++++++++++++++++++++++++++++++++- controller-js/coq_lsp_worker.ml | 32 +++++++++--------- controller-js/dune | 32 ++++++++++++++---- controller-js/my_dynload.ml | 54 ++++++++++++++++++++++++++++++ controller-js/my_dynload.mli | 1 + etc/META.threads | 37 +++++++++++++++++++++ 7 files changed, 234 insertions(+), 23 deletions(-) create mode 100644 controller-js/my_dynload.ml create mode 100644 controller-js/my_dynload.mli create mode 100755 etc/META.threads diff --git a/Makefile b/Makefile index 030891c7..390c8750 100644 --- a/Makefile +++ b/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 diff --git a/controller-js/README.md b/controller-js/README.md index 6b2ec291..1564dd1f 100644 --- a/controller-js/README.md +++ b/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` + diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml index 13c7c80f..ff50e1ec 100644 --- a/controller-js/coq_lsp_worker.ml +++ b/controller-js/coq_lsp_worker.ml @@ -71,9 +71,9 @@ 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 @@ -81,15 +81,13 @@ let lib_fs ~prefix:_ ~path = 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); diff --git a/controller-js/dune b/controller-js/dune index af7826f5..85ddcb30 100644 --- a/controller-js/dune +++ b/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) diff --git a/controller-js/my_dynload.ml b/controller-js/my_dynload.ml new file mode 100644 index 00000000..689d6e82 --- /dev/null +++ b/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 diff --git a/controller-js/my_dynload.mli b/controller-js/my_dynload.mli new file mode 100644 index 00000000..ce1b7ec2 --- /dev/null +++ b/controller-js/my_dynload.mli @@ -0,0 +1 @@ +val load_packages : ?debug:bool -> ?loadfile:(string -> unit) -> string list -> unit diff --git a/etc/META.threads b/etc/META.threads new file mode 100755 index 00000000..6e01dec9 --- /dev/null +++ b/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]" +) +