From c9c974ed1dfc01890611dbdc7dcb19142df93871 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 31 Jan 2023 16:58:27 +0100 Subject: [PATCH 1/6] [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 | 5 + Makefile | 10 + controller-js/README.md | 10 + controller-js/coq_lsp_worker.ml | 181 +++++++++++ controller-js/coq_lsp_worker.mli | 0 controller-js/dune | 59 ++++ controller-js/js_stub/coq_perf.js | 17 + controller-js/js_stub/coq_vm.js | 296 +++++++++++++++++ controller-js/js_stub/interrupt.js | 27 ++ controller-js/js_stub/marshal32.js | 4 + controller-js/js_stub/marshal64.js | 206 ++++++++++++ controller-js/js_stub/mutex.js | 93 ++++++ controller-js/js_stub/unix.js | 502 +++++++++++++++++++++++++++++ editor/code/src/browser.ts | 72 ++++- examples/documentSymbol.v | 2 +- flake.nix | 2 +- 16 files changed, 1479 insertions(+), 7 deletions(-) create mode 100644 controller-js/README.md create mode 100644 controller-js/coq_lsp_worker.ml create mode 100644 controller-js/coq_lsp_worker.mli create mode 100644 controller-js/dune create mode 100644 controller-js/js_stub/coq_perf.js create mode 100644 controller-js/js_stub/coq_vm.js create mode 100644 controller-js/js_stub/interrupt.js create mode 100644 controller-js/js_stub/marshal32.js create mode 100644 controller-js/js_stub/marshal64.js create mode 100644 controller-js/js_stub/mutex.js create mode 100644 controller-js/js_stub/unix.js diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index d49232c5..8255adc7 100644 --- a/CONTRIBUTING.md +++ b/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 diff --git a/Makefile b/Makefile index 90201847..ec08903c 100644 --- a/Makefile +++ b/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 diff --git a/controller-js/README.md b/controller-js/README.md new file mode 100644 index 00000000..6b2ec291 --- /dev/null +++ b/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. + diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml new file mode 100644 index 00000000..91e19577 --- /dev/null +++ b/controller-js/coq_lsp_worker.ml @@ -0,0 +1,181 @@ +(* 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 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=\"/static/lib\"path=\"/static/lib\"" +let findlib_path = "/static/lib/findlib.conf" + +let setup_pseudo_fs () = + (* '/static' is the default working directory of jsoo *) + Sys_js.create_file ~name:findlib_path ~content:findlib_conf; + () + +let setup_std_printers () = + 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) = + 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 + (* 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" + +(* 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/coqlib" + ; coqcorelib = "/static/lib/coq-core" + ; findlib_config = Some findlib_path + ; ocamlpath = [] + ; 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 () diff --git a/controller-js/coq_lsp_worker.mli b/controller-js/coq_lsp_worker.mli new file mode 100644 index 00000000..e69de29b diff --git a/controller-js/dune b/controller-js/dune new file mode 100644 index 00000000..af7826f5 --- /dev/null +++ b/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} ')'")))) diff --git a/controller-js/js_stub/coq_perf.js b/controller-js/js_stub/coq_perf.js new file mode 100644 index 00000000..41ba8c4c --- /dev/null +++ b/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; +} + diff --git a/controller-js/js_stub/coq_vm.js b/controller-js/js_stub/coq_vm.js new file mode 100644 index 00000000..cf86e905 --- /dev/null +++ b/controller-js/js_stub/coq_vm.js @@ -0,0 +1,296 @@ +// Provides: vm_ll +function vm_ll(s, args) { + if (vm_ll.log) joo_global_object.console.warn(s, args); + if (vm_ll.trap) throw new Error("vm trap: '"+ s + "' not implemented"); +} + +vm_ll.log = false; // whether to log calls +vm_ll.trap = false; // whether to halt on calls + +// Provides: init_coq_vm +// Requires: vm_ll +function init_coq_vm() { + vm_ll('init_coq_vm', arguments); + return; +} + +// EG: Coq VM's code is evil and performs static initialization... the +// best option would be to disable the VM code entirely as before. + +// Provides: coq_vm_trap +// Requires: vm_ll +function coq_vm_trap() { // will cause future calls to vm code to fault + vm_ll.log = vm_ll.trap = true; // (called after initialization) +} + +// Provides: accumulate_code +// Requires: vm_ll +function accumulate_code() { + // EG: Where the hell is that called from + vm_ll('accumulate_code', arguments); + return []; +} + +// Provides: coq_pushpop +// Requires: vm_ll +function coq_pushpop() { + vm_ll('coq_pushpop', arguments); + return []; +} + +// Provides: coq_closure_arity +// Requires: vm_ll +function coq_closure_arity() { + vm_ll('coq_closure_arity', arguments); + return []; +} + +// Provides: coq_eval_tcode +// Requires: vm_ll +function coq_eval_tcode() { + vm_ll('coq_eval_tcode', arguments); + return []; +} + +// Provides: coq_int_tcode +// Requires: vm_ll +function coq_int_tcode() { + vm_ll('coq_int_tcode', arguments); + return []; +} + +// Provides: coq_interprete_ml +// Requires: vm_ll +function coq_interprete_ml() { + vm_ll('coq_interprete_ml', arguments); + return []; +} + +// Provides: coq_is_accumulate_code +// Requires: vm_ll +function coq_is_accumulate_code() { + vm_ll('coq_is_accumulate_code', arguments); + return []; +} + +// Provides: coq_kind_of_closure +// Requires: vm_ll +function coq_kind_of_closure() { + vm_ll('coq_kind_of_closure', arguments); + return []; +} + +// Provides: coq_makeaccu +// Requires: vm_ll +function coq_makeaccu() { + vm_ll('coq_makeaccu', arguments); + return []; +} + +// Provides: coq_offset +// Requires: vm_ll +function coq_offset() { + vm_ll('coq_offset', arguments); + return []; +} + +// Provides: coq_offset_closure +// Requires: vm_ll +function coq_offset_closure() { + vm_ll('coq_offset_closure', arguments); + return []; +} + +// Provides: coq_offset_tcode +// Requires: vm_ll +function coq_offset_tcode() { + vm_ll('coq_offset_tcode', arguments); + return []; +} + +// Provides: coq_push_arguments +// Requires: vm_ll +function coq_push_arguments() { + vm_ll('coq_push_arguments', arguments); + return []; +} + +// Provides: coq_push_ra +// Requires: vm_ll +function coq_push_ra() { + vm_ll('coq_push_ra', arguments); + return []; +} + +// Provides: coq_push_val +// Requires: vm_ll +function coq_push_val() { + vm_ll('coq_push_val', arguments); + return []; +} + +// Provides: coq_push_vstack +// Requires: vm_ll +function coq_push_vstack() { + vm_ll('coq_push_vstack', arguments); + return []; +} + +// Provides: coq_set_transp_value +// Requires: vm_ll +function coq_set_transp_value() { + vm_ll('coq_set_transp_value', arguments); + return []; +} + +// Provides: coq_set_bytecode_field +// Requires: vm_ll +function coq_set_bytecode_field() { + vm_ll('coq_set_bytecode_field', arguments); + return [0]; +} + +// Provides: coq_tcode_of_code +// Requires: vm_ll +function coq_tcode_of_code() { + vm_ll('coq_tcode_of_code', arguments); + return []; +} + +// Provides: coq_accumulate +// Requires: vm_ll +function coq_accumulate() { + // This is called on init, so let's be more lenient + // vm_ll('coq_accumulate', arguments); + return []; +} + +// Provides: coq_obj_set_tag +// Requires: vm_ll +function coq_obj_set_tag() { + vm_ll('coq_obj_set_tag', arguments); + return []; +} + +// Provides: coq_uint63_to_float_byte +// Requires: vm_ll +function coq_uint63_to_float_byte() { + // First element of the array is the length! + vm_ll('coq_uint63_to_float_byte', arguments); + return [0]; +} + +// Provides: get_coq_atom_tbl +// Requires: vm_ll +function get_coq_atom_tbl() { + // First element of the array is the length! + vm_ll('get_coq_atom_tbl', arguments); + return [0]; +} + +// Provides: get_coq_global_data +// Requires: vm_ll +function get_coq_global_data() { + vm_ll('get_coq_global_data', arguments); + return []; +} + +// Provides: get_coq_transp_value +// Requires: vm_ll +function get_coq_transp_value() { + vm_ll('get_coq_transp_value', arguments); + return []; +} + +// Provides: realloc_coq_atom_tbl +// Requires: vm_ll +function realloc_coq_atom_tbl() { + vm_ll('realloc_coq_atom_tbl', arguments); + return; +} + +// Provides: realloc_coq_global_data +// Requires: vm_ll +function realloc_coq_global_data() { + vm_ll('realloc_coq_global_data', arguments); + return; +} + +// Provides: coq_interprete_byte +// Requires: vm_ll +function coq_interprete_byte() { vm_ll('coq_interprete_byte', arguments); } +// Provides: coq_set_drawinstr +// Requires: vm_ll +function coq_set_drawinstr() { vm_ll('coq_set_drawinstr', arguments); } +// Provides: coq_tcode_array +// Requires: vm_ll +function coq_tcode_array() { vm_ll('coq_tcode_array', arguments); } + +// Provides: coq_fadd_byte +function coq_fadd_byte(r1, r2) { + return r1 + r2; +} + +// Provides: coq_fsub_byte +function coq_fsub_byte(r1, r2) { + return r1 - r2; +} + +// Provides: coq_fmul_byte +function coq_fmul_byte(r1, r2) { + return r1 * r2; +} + +// Provides: coq_fdiv_byte +function coq_fdiv_byte(r1, r2) { + return r1 / r2; +} + +// Provides: coq_fsqrt_byte +// Requires: vm_ll +function coq_fsqrt_byte() { + vm_ll('coq_fsqrt_byte', arguments); + return; +} + +// Provides: coq_is_double +// Requires: vm_ll + function coq_is_double() { + vm_ll('coq_is_double', arguments); + return; +} + +// Provides: coq_next_down_byte +// Requires: vm_ll + function coq_next_down_byte() { + vm_ll('coq_next_down_byte', arguments); + return; +} + +// Provides: coq_next_up_byte +// Requires: vm_ll + function coq_next_up_byte() { + vm_ll('coq_next_up_byte', arguments); + return; +} + +// Provides: coq_current_fix +// Requires: vm_ll +function coq_current_fix() { + vm_ll('coq_current_fix', arguments); + return []; +} + +// Provides: coq_last_fix +// Requires: vm_ll +function coq_last_fix() { + vm_ll('coq_last_fix', arguments); + return []; +} + +// Provides: coq_shift_fix +// Requires: vm_ll +function coq_shift_fix() { + vm_ll('coq_shift_fix', arguments); + return []; +} diff --git a/controller-js/js_stub/interrupt.js b/controller-js/js_stub/interrupt.js new file mode 100644 index 00000000..6b14c1ce --- /dev/null +++ b/controller-js/js_stub/interrupt.js @@ -0,0 +1,27 @@ +// Provides: interrupt_setup +function interrupt_setup(shmem) { + var Int32Array = joo_global_object.Int32Array, + SharedArrayBuffer = joo_global_object.SharedArrayBuffer; + + if (Int32Array && SharedArrayBuffer) { + shmem = shmem || new Int32Array(new SharedArrayBuffer(4)); + interrupt_setup.vec = shmem; + interrupt_setup.checkpoint = 0; + return shmem; + } +} + +// Provides: interrupt_pending +// Requires: interrupt_setup +function interrupt_pending() { + var Atomics = joo_global_object.Atomics; + + if (Atomics && interrupt_setup.vec) { + var ld = Atomics.load(interrupt_setup.vec, 0); + if (ld > interrupt_setup.checkpoint) { + interrupt_setup.checkpoint = ld; + return true; + } + } + return false; +} diff --git a/controller-js/js_stub/marshal32.js b/controller-js/js_stub/marshal32.js new file mode 100644 index 00000000..93a769d0 --- /dev/null +++ b/controller-js/js_stub/marshal32.js @@ -0,0 +1,4 @@ +/* (Blank) + * For 64-bit compilation, marshal64.js is selected. + * For 32-bit compilation, nothing further is required. + */ diff --git a/controller-js/js_stub/marshal64.js b/controller-js/js_stub/marshal64.js new file mode 100644 index 00000000..90b368a1 --- /dev/null +++ b/controller-js/js_stub/marshal64.js @@ -0,0 +1,206 @@ +/** + * This is a hack to circumvent a discrepancy arising when Coq is compiled + * as a 64-bit library and then passed through js_of_ocaml, resulting in + * 32-bit JavaScript code. + * As a whole, the Coq codebase makes little use of integer arithmetic and + * does not create huge arrays of more than 2^31-1 elements. An exception + * to this is hash values calculated for storing various Coq types in maps + * and hash tables and to speed up comparisons. + * Though the values themselves are meaningless, they are unfortunately + * stored in .vo files through use of the Marshal module, and lead to files + * that cannot be read back via 32-bit code. + * + * As 32-bit support is declining (e.g. the following issue relating to + * macOS builds of OCaml: https://github.com/ocaml/ocaml/issues/6900), + * there may be no escape from building 64-bit Coq, both core and libraries. + * This requires a patch to jsoo's Marshal primitive that will not throw + * when encountering a 64-bit integer. The version below truncates such + * values. It may be extremely fragile, but so far, seems to work. + */ + + +//Provides: caml_input_value_from_reader mutable +//Requires: caml_failwith +//Requires: caml_float_of_bytes, caml_custom_ops + +/*** !!! This overrides the implementation from js_of_ocaml !!! ***/ + +function caml_input_value_from_reader(reader, ofs) { + var _magic = reader.read32u () + var _block_len = reader.read32u (); + var num_objects = reader.read32u (); + var _size_32 = reader.read32u (); + var _size_64 = reader.read32u (); + var stack = []; + var intern_obj_table = (num_objects > 0)?[]:null; + var obj_counter = 0; + function intern_rec () { + var code = reader.read8u (); + if (code >= 0x40 /*cst.PREFIX_SMALL_INT*/) { + if (code >= 0x80 /*cst.PREFIX_SMALL_BLOCK*/) { + var tag = code & 0xF; + var size = (code >> 4) & 0x7; + var v = [tag]; + if (size == 0) return v; + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + stack.push(v, size); + return v; + } else + return (code & 0x3F); + } else { + if (code >= 0x20/*cst.PREFIX_SMALL_STRING */) { + var len = code & 0x1F; + var v = reader.readstr (len); + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + } else { + switch(code) { + case 0x00: //cst.CODE_INT8: + return reader.read8s (); + case 0x01: //cst.CODE_INT16: + return reader.read16s (); + case 0x02: //cst.CODE_INT32: + return reader.read32s (); + case 0x03: //cst.CODE_INT64: + reader.read32s (); return reader.read32s (); // <------------ HERE + //caml_failwith("input_value: integer too large"); // (ouch) + break; + case 0x04: //cst.CODE_SHARED8: + var offset = reader.read8u (); + return intern_obj_table[obj_counter - offset]; + case 0x05: //cst.CODE_SHARED16: + var offset = reader.read16u (); + return intern_obj_table[obj_counter - offset]; + case 0x06: //cst.CODE_SHARED32: + var offset = reader.read32u (); + return intern_obj_table[obj_counter - offset]; + case 0x08: //cst.CODE_BLOCK32: + var header = reader.read32u (); + var tag = header & 0xFF; + var size = header >> 10; + var v = [tag]; + if (size == 0) return v; + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + stack.push(v, size); + return v; + case 0x13: //cst.CODE_BLOCK64: + caml_failwith ("input_value: data block too large"); + break; + case 0x09: //cst.CODE_STRING8: + var len = reader.read8u(); + var v = reader.readstr (len); + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + case 0x0A: //cst.CODE_STRING32: + var len = reader.read32u(); + var v = reader.readstr (len); + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + case 0x0C: //cst.CODE_DOUBLE_LITTLE: + var t = new Array(8);; + for (var i = 0;i < 8;i++) t[7 - i] = reader.read8u (); + var v = caml_float_of_bytes (t); + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + case 0x0B: //cst.CODE_DOUBLE_BIG: + var t = new Array(8);; + for (var i = 0;i < 8;i++) t[i] = reader.read8u (); + var v = caml_float_of_bytes (t); + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + case 0x0E: //cst.CODE_DOUBLE_ARRAY8_LITTLE: + var len = reader.read8u(); + var v = new Array(len+1); + v[0] = 254; + var t = new Array(8);; + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + for (var i = 1;i <= len;i++) { + for (var j = 0;j < 8;j++) t[7 - j] = reader.read8u(); + v[i] = caml_float_of_bytes (t); + } + return v; + case 0x0D: //cst.CODE_DOUBLE_ARRAY8_BIG: + var len = reader.read8u(); + var v = new Array(len+1); + v[0] = 254; + var t = new Array(8);; + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + for (var i = 1;i <= len;i++) { + for (var j = 0;j < 8;j++) t[j] = reader.read8u(); + v [i] = caml_float_of_bytes (t); + } + return v; + case 0x07: //cst.CODE_DOUBLE_ARRAY32_LITTLE: + var len = reader.read32u(); + var v = new Array(len+1); + v[0] = 254; + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + var t = new Array(8);; + for (var i = 1;i <= len;i++) { + for (var j = 0;j < 8;j++) t[7 - j] = reader.read8u(); + v[i] = caml_float_of_bytes (t); + } + return v; + case 0x0F: //cst.CODE_DOUBLE_ARRAY32_BIG: + var len = reader.read32u(); + var v = new Array(len+1); + v[0] = 254; + var t = new Array(8);; + for (var i = 1;i <= len;i++) { + for (var j = 0;j < 8;j++) t[j] = reader.read8u(); + v [i] = caml_float_of_bytes (t); + } + return v; + case 0x10: //cst.CODE_CODEPOINTER: + case 0x11: //cst.CODE_INFIXPOINTER: + caml_failwith ("input_value: code pointer"); + break; + case 0x12: //cst.CODE_CUSTOM: + case 0x18: //cst.CODE_CUSTOM_LEN: + case 0x19: //cst.CODE_CUSTOM_FIXED: + var c, s = ""; + while ((c = reader.read8u ()) != 0) s += String.fromCharCode (c); + var ops = caml_custom_ops[s]; + var expected_size; + if(!ops) + caml_failwith("input_value: unknown custom block identifier"); + switch(code){ + case 0x12: // cst.CODE_CUSTOM (deprecated) + break; + case 0x19: // cst.CODE_CUSTOM_FIXED + if(!ops.fixed_length) + caml_failwith("input_value: expected a fixed-size custom block"); + expected_size = ops.fixed_length; + break; + case 0x18: // cst.CODE_CUSTOM_LEN + expected_size = reader.read32u (); + // Skip size64 + reader.read32s(); reader.read32s(); + break; + } + var old_pos = reader.i; + var size = [0]; + var v = ops.deserialize(reader, size); + if(expected_size != undefined){ + if(expected_size != size[0]) + caml_failwith("input_value: incorrect length of serialized custom block"); + } + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + default: + caml_failwith ("input_value: ill-formed message"); + } + } + } + } + var res = intern_rec (); + while (stack.length > 0) { + var size = stack.pop(); + var v = stack.pop(); + var d = v.length; + if (d < size) stack.push(v, size); + v[d] = intern_rec (); + } + if (typeof ofs!="number") ofs[0] = reader.i; + return res; +} diff --git a/controller-js/js_stub/mutex.js b/controller-js/js_stub/mutex.js new file mode 100644 index 00000000..d4a9acb6 --- /dev/null +++ b/controller-js/js_stub/mutex.js @@ -0,0 +1,93 @@ +// Whether to log. +var v_log = false; +function ll(s) { if (v_log) console.log(s); } + +//Provides: caml_condition_broadcast +function caml_condition_broadcast() { + // ll("***caml_condition_broadcast"); + return 0; +} + +//Provides: caml_condition_new +function caml_condition_new() { + // ll("***caml_condition_new"); + return 0; +} + +//Provides: caml_condition_signal +function caml_condition_signal() { + // ll("***caml_condition_signal"); + return 0; +} + +//Provides: caml_condition_wait +function caml_condition_wait() { + // ll("***caml_condition_wait"); + return 0; +} + +//Provides: caml_thread_initialize +function caml_thread_initialize() { + // ll("***caml_thread_initialize"); + return 0; +} + +//Provides: caml_thread_new +function caml_thread_new() { + // ll("***caml_thread_new"); + return 0; +} + +//Provides: caml_thread_self +function caml_thread_self() { + // ll("***caml_thread_self"); + return [0,0]; +} + +//Provides: caml_thread_uncaught_exception +function caml_thread_uncaught_exception() { + // ll("***caml_thread_uncaught_exception"); + return 0; +} + +//Provides: caml_thread_yield +function caml_thread_yield() { + // ll("***caml_thread_yield"); + return 0; +} + +//Provides: caml_mutex_lock +function caml_mutex_lock() { + // ll("***caml_mutex_lock"); + return 0; +} + +//Provides: caml_mutex_new +function caml_mutex_new() { + // ll("***caml_mutex_new"); + return 0; +} + +//Provides: caml_mutex_unlock +function caml_mutex_unlock() { + // ll("***caml_mutex_unlock"); + return 0; +} + +//Provides: caml_thread_cleanup +function caml_thread_cleanup() { + // ll("***caml_thread_cleanup"); + return 0; +} + +//Provides: caml_thread_exit +function caml_thread_exit() { + // ll("***caml_thread_exit"); + return 0; +} + +//Provides: caml_thread_id +function caml_thread_id() { + // ll("***caml_thread_id"); + return 0; +} diff --git a/controller-js/js_stub/unix.js b/controller-js/js_stub/unix.js new file mode 100644 index 00000000..a606d9bb --- /dev/null +++ b/controller-js/js_stub/unix.js @@ -0,0 +1,502 @@ +//Provides: unix_ll +function unix_ll(s, args) { + if (unix_ll.log) joo_global_object.console.warn(s, args); + if (unix_ll.trap) throw new Error("unix trap: '"+ s + "' not implemented"); +} +unix_ll.log = true; // whether to log calls +unix_ll.trap = false; // whether to halt on calls + +//Provides: caml_raise_unix_error +//Requires: caml_named_value, caml_raise_with_arg, caml_new_string +function caml_raise_unix_error(msg) { + var tag = caml_named_value("Unix.Unix_error"); + // var util = require('util'); + // console.log(util.inspect(chan, {showHidden: false, depth: null})); + caml_raise_with_arg (tag, caml_new_string (msg)); +} + +//Provides: unix_access +//Requires: unix_ll +function unix_access() { + unix_ll("unix_access", arguments); + return 0; +} + +//Provides: unix_alarm +//Requires: unix_ll +function unix_alarm() { + unix_ll("unix_alarm", arguments); + return 0; +} + +//Provides: unix_bind +//Requires: unix_ll +function unix_bind() { + unix_ll("unix_bind", arguments); + return 0; +} + +//Provides: unix_close +//Requires: unix_ll +function unix_close() { + unix_ll("unix_close", arguments); + return 0; +} + +//Provides: unix_connect +//Requires: unix_ll +function unix_connect() { + unix_ll("unix_connect", arguments); + return 0; +} + +//Provides: unix_dup +//Requires: unix_ll +function unix_dup() { + unix_ll("unix_dup", arguments); + return 0; +} + +//Provides: unix_dup2 +//Requires: unix_ll +function unix_dup2() { + unix_ll("unix_dup2", arguments); + return 0; +} + +//Provides: unix_environment +//Requires: unix_ll +function unix_environment() { + unix_ll("unix_environment", arguments); + return 0; +} + +//Provides: unix_error_message +//Requires: unix_ll +function unix_error_message() { + unix_ll("unix_error_message", arguments); + return 0; +} + +//Provides: unix_execve +//Requires: unix_ll +function unix_execve() { + unix_ll("unix_execve", arguments); + return 0; +} + +//Provides: unix_execvp +//Requires: unix_ll +function unix_execvp() { + unix_ll("unix_execvp", arguments); + return 0; +} + +//Provides: unix_execvpe +//Requires: unix_ll +function unix_execvpe() { + unix_ll("unix_execvpe", arguments); + return 0; +} + +//Provides: unix_getcwd +//Requires: unix_ll +function unix_getcwd() { + unix_ll("unix_getcwd", arguments); + return 0; +} + +//Provides: unix_fork +//Requires: unix_ll +function unix_fork() { + unix_ll("unix_fork", arguments); + return 0; +} + +//Provides: unix_getpid +//Requires: unix_ll +function unix_getpid() { + unix_ll("unix_getpid", arguments); + return 0; +} + +//Provides: unix_getpwnam +//Requires: unix_ll +function unix_getpwnam() { + unix_ll("unix_getpwnam", arguments); + return 0; +} + +//Provides: unix_getsockname +//Requires: unix_ll +function unix_getsockname() { + unix_ll("unix_getsockname", arguments); + return 0; +} + +//Provides: unix_kill +//Requires: unix_ll +function unix_kill() { + unix_ll("unix_kill", arguments); + return 0; +} + +//Provides: unix_listen +//Requires: unix_ll +function unix_listen() { + unix_ll("unix_listen", arguments); + return 0; +} + +//Provides: unix_pipe +//Requires: unix_ll +function unix_pipe() { + unix_ll("unix_pipe", arguments); + return 0; +} + +//Provides: unix_read +//Requires: unix_ll +function unix_read() { + unix_ll("unix_read", arguments); + return 0; +} + +//Provides: unix_opendir +//Requires: unix_ll +function unix_opendir(dir) { + unix_ll("unix_opendir", arguments); + + // caml_raise_unix_error("opendir", arguments); + return []; +} + +//Provides: unix_readdir +//Requires: unix_ll, caml_raise_constant, caml_global_data +function unix_readdir(dir) { + unix_ll("unix_readdir", arguments); + + // caml_raise_unix_error("readdir", arguments); + caml_raise_constant(caml_global_data.End_of_file); + return []; +} + +//Provides: unix_closedir +//Requires: unix_ll +function unix_closedir() { + unix_ll("unix_closedir", arguments); + return []; +} + +//Provides: unix_select +//Requires: unix_ll +function unix_select() { + unix_ll("unix_select", arguments); + return 0; +} + +//Provides: unix_set_close_on_exec +//Requires: unix_ll +function unix_set_close_on_exec() { + unix_ll("unix_set_close_on_exec", arguments); + return 0; +} + +//Provides: unix_set_nonblock +//Requires: unix_ll +function unix_set_nonblock() { + unix_ll("unix_set_nonblock", arguments); + return 0; +} + +//Provides: unix_sleep +//Requires: unix_ll +function unix_sleep() { + unix_ll("unix_sleep", arguments); + return 0; +} + +//Provides: unix_socket +//Requires: unix_ll +function unix_socket() { + unix_ll("unix_socket", arguments); + return 0; +} + +//Provides: unix_string_of_inet_addr +//Requires: unix_ll +function unix_string_of_inet_addr() { + unix_ll("unix_string_of_inet_addr", arguments); + return 0; +} + +//Provides: unix_times +//Requires: unix_ll +function unix_times() { + unix_ll("unix_times", arguments); + return 0; +} + +//Provides: unix_wait +//Requires: unix_ll +function unix_wait() { + unix_ll("unix_wait", arguments); + return 0; +} + +//Provides: unix_waitpid +//Requires: unix_ll +function unix_waitpid() { + unix_ll("unix_waitpid", arguments); + return 0; +} + +// Provides: unix_accept +// Requires: unix_ll +function unix_accept() { unix_ll("unix_accept", arguments); } +// Provides: unix_chdir +// Requires: unix_ll +function unix_chdir() { unix_ll("unix_chdir", arguments); } +// Provides: unix_chmod +// Requires: unix_ll +function unix_chmod() { unix_ll("unix_chmod", arguments); } +// Provides: unix_chown +// Requires: unix_ll +function unix_chown() { unix_ll("unix_chown", arguments); } +// Provides: unix_chroot +// Requires: unix_ll +function unix_chroot() { unix_ll("unix_chroot", arguments); } +// Provides: unix_clear_close_on_exec +// Requires: unix_ll +function unix_clear_close_on_exec() { unix_ll("unix_clear_close_on_exec", arguments); } +// Provides: unix_clear_nonblock +// Requires: unix_ll +function unix_clear_nonblock() { unix_ll("unix_clear_nonblock", arguments); } +// Provides: unix_environment_unsafe +// Requires: unix_ll +function unix_environment_unsafe() { unix_ll("unix_environment_unsafe", arguments); } +// Provides: unix_execv +// Requires: unix_ll +function unix_execv() { unix_ll("unix_execv", arguments); } +// Provides: unix_fchmod +// Requires: unix_ll +function unix_fchmod() { unix_ll("unix_fchmod", arguments); } +// Provides: unix_fchown +// Requires: unix_ll +function unix_fchown() { unix_ll("unix_fchown", arguments); } +// Provides: unix_fstat +// Requires: unix_ll +function unix_fstat() { unix_ll("unix_fstat", arguments); } +// Provides: unix_fstat_64 +// Requires: unix_ll +function unix_fstat_64() { unix_ll("unix_fstat_64", arguments); } +// Provides: unix_ftruncate +// Requires: unix_ll +function unix_ftruncate() { unix_ll("unix_ftruncate", arguments); } +// Provides: unix_ftruncate_64 +// Requires: unix_ll +function unix_ftruncate_64() { unix_ll("unix_ftruncate_64", arguments); } +// Provides: unix_getaddrinfo +// Requires: unix_ll +function unix_getaddrinfo() { unix_ll("unix_getaddrinfo", arguments); } +// Provides: unix_getegid +// Requires: unix_ll +function unix_getegid() { unix_ll("unix_getegid", arguments); } +// Provides: unix_geteuid +// Requires: unix_ll +function unix_geteuid() { unix_ll("unix_geteuid", arguments); } +// Provides: unix_getgid +// Requires: unix_ll +function unix_getgid() { unix_ll("unix_getgid", arguments); } +// Provides: unix_getgrgid +// Requires: unix_ll +function unix_getgrgid() { unix_ll("unix_getgrgid", arguments); } +// Provides: unix_getgrnam +// Requires: unix_ll +function unix_getgrnam() { unix_ll("unix_getgrnam", arguments); } +// Provides: unix_getgroups +// Requires: unix_ll +function unix_getgroups() { unix_ll("unix_getgroups", arguments); } +// Provides: unix_gethostbyaddr +// Requires: unix_ll +function unix_gethostbyaddr() { unix_ll("unix_gethostbyaddr", arguments); } +// Provides: unix_gethostbyname +// Requires: unix_ll +function unix_gethostbyname() { unix_ll("unix_gethostbyname", arguments); } +// Provides: unix_gethostname +// Requires: unix_ll +function unix_gethostname() { unix_ll("unix_gethostname", arguments); } +// Provides: unix_getitimer +// Requires: unix_ll +function unix_getitimer() { unix_ll("unix_getitimer", arguments); } +// Provides: unix_getlogin +// Requires: unix_ll +function unix_getlogin() { unix_ll("unix_getlogin", arguments); } +// Provides: unix_getnameinfo +// Requires: unix_ll +function unix_getnameinfo() { unix_ll("unix_getnameinfo", arguments); } +// Provides: unix_getpeername +// Requires: unix_ll +function unix_getpeername() { unix_ll("unix_getpeername", arguments); } +// Provides: unix_getppid +// Requires: unix_ll +function unix_getppid() { unix_ll("unix_getppid", arguments); } +// Provides: unix_getprotobyname +// Requires: unix_ll +function unix_getprotobyname() { unix_ll("unix_getprotobyname", arguments); } +// Provides: unix_getprotobynumber +// Requires: unix_ll +function unix_getprotobynumber() { unix_ll("unix_getprotobynumber", arguments); } +// Provides: unix_getservbyname +// Requires: unix_ll +function unix_getservbyname() { unix_ll("unix_getservbyname", arguments); } +// Provides: unix_getservbyport +// Requires: unix_ll +function unix_getservbyport() { unix_ll("unix_getservbyport", arguments); } +// Provides: unix_getsockopt +// Requires: unix_ll +function unix_getsockopt() { unix_ll("unix_getsockopt", arguments); } +// Provides: unix_initgroups +// Requires: unix_ll +function unix_initgroups() { unix_ll("unix_initgroups", arguments); } +// Provides: unix_link +// Requires: unix_ll +function unix_link() { unix_ll("unix_link", arguments); } +// Provides: unix_lockf +// Requires: unix_ll +function unix_lockf() { unix_ll("unix_lockf", arguments); } +// Provides: unix_lseek +// Requires: unix_ll +function unix_lseek() { unix_ll("unix_lseek", arguments); } +// Provides: unix_lseek_64 +// Requires: unix_ll +function unix_lseek_64() { unix_ll("unix_lseek_64", arguments); } +// Provides: unix_mkfifo +// Requires: unix_ll +function unix_mkfifo() { unix_ll("unix_mkfifo", arguments); } +// Provides: unix_nice +// Requires: unix_ll +function unix_nice() { unix_ll("unix_nice", arguments); } +// Provides: unix_open +// Requires: unix_ll +function unix_open() { unix_ll("unix_open", arguments); } +// Provides: unix_putenv +// Requires: unix_ll +function unix_putenv() { unix_ll("unix_putenv", arguments); } +// Provides: unix_recv +// Requires: unix_ll +function unix_recv() { unix_ll("unix_recv", arguments); } +// Provides: unix_recvfrom +// Requires: unix_ll +function unix_recvfrom() { unix_ll("unix_recvfrom", arguments); } +// Provides: unix_rename +// Requires: unix_ll +function unix_rename() { unix_ll("unix_rename", arguments); } +// Provides: unix_rewinddir +// Requires: unix_ll +function unix_rewinddir() { unix_ll("unix_rewinddir", arguments); } +// Provides: unix_send +// Requires: unix_ll +function unix_send() { unix_ll("unix_send", arguments); } +// Provides: unix_sendto +// Requires: unix_ll +function unix_sendto() { unix_ll("unix_sendto", arguments); } +// Provides: unix_setgid +// Requires: unix_ll +function unix_setgid() { unix_ll("unix_setgid", arguments); } +// Provides: unix_setgroups +// Requires: unix_ll +function unix_setgroups() { unix_ll("unix_setgroups", arguments); } +// Provides: unix_setitimer +// Requires: unix_ll +function unix_setitimer() { unix_ll("unix_setitimer", arguments); } +// Provides: unix_setsid +// Requires: unix_ll +function unix_setsid() { unix_ll("unix_setsid", arguments); } +// Provides: unix_setsockopt +// Requires: unix_ll +function unix_setsockopt() { unix_ll("unix_setsockopt", arguments); } +// Provides: unix_setuid +// Requires: unix_ll +function unix_setuid() { unix_ll("unix_setuid", arguments); } +// Provides: unix_shutdown +// Requires: unix_ll +function unix_shutdown() { unix_ll("unix_shutdown", arguments); } +// Provides: unix_sigpending +// Requires: unix_ll +function unix_sigpending() { unix_ll("unix_sigpending", arguments); } +// Provides: unix_sigprocmask +// Requires: unix_ll +function unix_sigprocmask() { unix_ll("unix_sigprocmask", arguments); } +// Provides: unix_sigsuspend +// Requires: unix_ll +function unix_sigsuspend() { unix_ll("unix_sigsuspend", arguments); } +// Provides: unix_single_write +// Requires: unix_ll +function unix_single_write() { unix_ll("unix_single_write", arguments); } +// Provides: unix_socketpair +// Requires: unix_ll +function unix_socketpair() { unix_ll("unix_socketpair", arguments); } +// Provides: unix_tcdrain +// Requires: unix_ll +function unix_tcdrain() { unix_ll("unix_tcdrain", arguments); } +// Provides: unix_tcflow +// Requires: unix_ll +function unix_tcflow() { unix_ll("unix_tcflow", arguments); } +// Provides: unix_tcflush +// Requires: unix_ll +function unix_tcflush() { unix_ll("unix_tcflush", arguments); } +// Provides: unix_tcgetattr +// Requires: unix_ll +function unix_tcgetattr() { unix_ll("unix_tcgetattr", arguments); } +// Provides: unix_tcsendbreak +// Requires: unix_ll +function unix_tcsendbreak() { unix_ll("unix_tcsendbreak", arguments); } +// Provides: unix_tcsetattr +// Requires: unix_ll +function unix_tcsetattr() { unix_ll("unix_tcsetattr", arguments); } +// Provides: unix_truncate +// Requires: unix_ll +function unix_truncate() { unix_ll("unix_truncate", arguments); } +// Provides: unix_truncate_64 +// Requires: unix_ll +function unix_truncate_64() { unix_ll("unix_truncate_64", arguments); } +// Provides: unix_umask +// Requires: unix_ll +function unix_umask() { unix_ll("unix_umask", arguments); } +// Provides: unix_utimes +// Requires: unix_ll +function unix_utimes() { unix_ll("unix_utimes", arguments); } +// Provides: unix_write +// Requires: unix_ll +function unix_write() { unix_ll("unix_write", arguments); } +// Provides: unix_exit +// Requires: unix_ll +function unix_exit() { unix_ll("unix_exit", arguments); } +// Provides: unix_spawn +// Requires: unix_ll +function unix_spawn() { unix_ll("unix_spawn", arguments); } +// Provides: unix_fsync +// Requires: unix_ll +function unix_fsync() { unix_ll("unix_fsync", arguments); } +// Provides: unix_inchannel_of_filedescr +// Requires: unix_ll +function unix_inchannel_of_filedescr() { unix_ll("unix_inchannel_of_filedescr", arguments); } +// Provides: unix_outchannel_of_filedescr +// Requires: unix_ll +function unix_outchannel_of_filedescr() { unix_ll("unix_outchannel_of_filedescr", arguments); } +// Provides: caml_mutex_try_lock +// Requires: unix_ll +function caml_mutex_try_lock() { unix_ll("caml_mutex_try_lock", arguments); } +// Provides: caml_thread_join +// Requires: unix_ll +function caml_thread_join() { unix_ll("caml_thread_join", arguments); } +// Provides: caml_thread_sigmask +// Requires: unix_ll +function caml_thread_sigmask() { unix_ll("caml_thread_sigmask", arguments); } +// Provides: caml_unix_map_file_bytecode +// Requires: unix_ll +function caml_unix_map_file_bytecode() { unix_ll("caml_unix_map_file_bytecode", arguments); } +// Provides: caml_wait_signal +// Requires: unix_ll +function caml_wait_signal() { unix_ll("caml_wait_signal", arguments); } diff --git a/editor/code/src/browser.ts b/editor/code/src/browser.ts index 3164eb48..0b45263e 100644 --- a/editor/code/src/browser.ts +++ b/editor/code/src/browser.ts @@ -1,19 +1,81 @@ -import { ExtensionContext } from "vscode"; -import { LanguageClient } from "vscode-languageclient/browser"; +import { ExtensionContext, Uri } from "vscode"; +import { + LanguageClient, + LanguageClientOptions, +} from "vscode-languageclient/browser"; import { activateCoqLSP, ClientFactoryType, deactivateCoqLSP } from "./client"; +import { workspace } from "vscode"; + +class InterruptibleLC extends LanguageClient { + private readonly interrupt_vec?: Int32Array; + + constructor( + id: string, + name: string, + clientOptions: LanguageClientOptions, + worker: Worker + ) { + super(id, name, clientOptions, worker); + + // We don't fail if COI is not enabled, as of Feb 2023 you must either: + // - pass --enable-coi to vscode + // - use `?enable-coi= in the vscode dev setup + // See https://code.visualstudio.com/updates/v1_72#_towards-cross-origin-isolation + // See https://github.com/microsoft/vscode-wasm + if (typeof SharedArrayBuffer !== "undefined") { + this.interrupt_vec = new Int32Array(new SharedArrayBuffer(4)); + worker.postMessage(["SetupInterrupt", this.interrupt_vec]); + } + + this.middleware.sendRequest = (type, param, token, next) => { + this.interrupt(); + return next(type, param, token); + }; + this.middleware.sendNotification = (type, next, params) => { + this.interrupt(); + return next(type, params); + }; + + this.middleware.didChange = (data, next) => { + this.interrupt(); + return next(data); + }; + } + + public interrupt() { + if (this.interrupt_vec) { + Atomics.add(this.interrupt_vec, 0, 1); + } + } +} export function activate(context: ExtensionContext): void { const cf: ClientFactoryType = (context, clientOptions, wsConfig) => { // Pending on having the API to fetch the worker file. - throw "Worker not found"; - let worker = new Worker(""); - return new LanguageClient( + // throw "Worker not found"; + const coqWorker = Uri.joinPath( + context.extensionUri, + "out/coq_lsp_worker.bc.js" + ); + console.log(coqWorker); + + let worker = new Worker(coqWorker.toString(true)); + let client = new InterruptibleLC( "coq-lsp", "Coq LSP Worker", clientOptions, worker ); + return client; }; + + // let files = Uri.joinPath(context.extensionUri, "out/files.json"); + + // workspace.fs.readFile(files).then((content) => { + // let s = new TextDecoder().decode(content); + // console.log(`files: `, JSON.parse(s)); + // }); + activateCoqLSP(context, cf); } diff --git a/examples/documentSymbol.v b/examples/documentSymbol.v index a0149e94..78044a02 100644 --- a/examples/documentSymbol.v +++ b/examples/documentSymbol.v @@ -42,4 +42,4 @@ Module Bar. Theorem not : False. Qed. -End Bar. \ No newline at end of file +End Bar. diff --git a/flake.nix b/flake.nix index 0b4f98d6..5e130af7 100644 --- a/flake.nix +++ b/flake.nix @@ -75,7 +75,7 @@ flakeFormatter = true; - settings.global.excludes = ["./vendor/**"]; + settings.global.excludes = ["./vendor/**" "controller-js/js_stub/**"]; programs.alejandra.enable = true; programs.ocamlformat = { From 81b490c6b910350cdb8f999fbe82f7fff7fa05a5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Sep 2024 17:38:37 +0200 Subject: [PATCH 2/6] [ci] [js] Build JS worker on CI. --- .github/workflows/build.yml | 46 +++++++++++++++ Makefile | 5 ++ etc/0001-coq-lsp-patch.patch | 59 +++++++++++++++++++ ...001-jscoq-lib-system.ml-de-unix-stat.patch | 31 ++++++++++ 4 files changed, 141 insertions(+) create mode 100644 etc/0001-coq-lsp-patch.patch create mode 100644 etc/0001-jscoq-lib-system.ml-de-unix-stat.patch diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 21416bab..3d1bd616 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -85,6 +85,52 @@ jobs: - name: 🐛 Test fcc run: opam exec -- make test-compiler + build-js: + name: Web Worker Build + strategy: + fail-fast: false + runs-on: ubuntu-latest + + steps: + # OPAM figures out everything but the libgmp-dev:i386 + # dependency, maybe worth fixing this upstream in the opam + # repository + - name: Install apt dependencies + run: | + sudo apt-get install aptitude + sudo dpkg --add-architecture i386 + sudo aptitude -o Acquire::Retries=30 update -q + sudo aptitude -o Acquire::Retries=30 install gcc-multilib g++-multilib pkg-config libgmp-dev libgmp-dev:i386 -y + + - name: 🔭 Checkout code + uses: actions/checkout@v4 + with: + submodules: recursive + + - name: 🐫 Setup OCaml + uses: ocaml/setup-ocaml@v2 + with: + ocaml-compiler: "ocaml-variants.4.14.2+options,ocaml-option-32bit" + dune-cache: true + + - 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 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 + + - name: Upload artifact + uses: actions/upload-artifact@v4 + with: + name: coq-lsp_worker and front-end + path: editor/code/out/ build-opam: name: Opam dev install strategy: diff --git a/Makefile b/Makefile index ec08903c..030891c7 100644 --- a/Makefile +++ b/Makefile @@ -144,3 +144,8 @@ opam-update-and-reinstall: git pull --recurse-submodules for pkg in coq-core coq-stdlib coqide-server coq; do opam install -y vendor/coq/$$pkg.opam; done opam install . + +.PHONY: patch-for-js +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 diff --git a/etc/0001-coq-lsp-patch.patch b/etc/0001-coq-lsp-patch.patch new file mode 100644 index 00000000..f42d9cd4 --- /dev/null +++ b/etc/0001-coq-lsp-patch.patch @@ -0,0 +1,59 @@ +From aa1c239f64a703785d9c4a520eee3aa4f97fa3ba Mon Sep 17 00:00:00 2001 +From: Emilio Jesus Gallego Arias +Date: Thu, 26 Sep 2024 21:46:55 +0200 +Subject: [PATCH] coq-lsp patch + +--- + lib/control.ml | 7 +++++++ + lib/dune | 4 ++++ + lib/jscoq_extern.c | 4 ++++ + 3 files changed, 15 insertions(+) + create mode 100644 lib/jscoq_extern.c + +diff --git a/lib/control.ml b/lib/control.ml +index 2480821c61..49ddb6e7e3 100644 +--- a/lib/control.ml ++++ b/lib/control.ml +@@ -18,7 +18,14 @@ let enable_thread_delay = ref false + + exception Timeout + ++(* implemented in backend/jsoo/js_stub/interrupt.js *) ++external interrupt_pending : unit -> bool = "interrupt_pending" ++ ++let jscoq_event_yield () = ++ if interrupt_pending () then interrupt := true ++ + let check_for_interrupt () = ++ jscoq_event_yield (); + if !interrupt then begin interrupt := false; raise Sys.Break end; + if !enable_thread_delay then begin + incr steps; +diff --git a/lib/dune b/lib/dune +index e7b1418c9b..f23338c03c 100644 +--- a/lib/dune ++++ b/lib/dune +@@ -4,6 +4,10 @@ + (public_name coq-core.lib) + (wrapped false) + (modules_without_implementation xml_datatype) ++ (foreign_stubs ++ (language c) ++ (names jscoq_extern) ++ (flags :standard (:include %{project_root}/config/dune.c_flags))) + (libraries + coq-core.boot coq-core.clib coq-core.config + (select instr.ml from +diff --git a/lib/jscoq_extern.c b/lib/jscoq_extern.c +new file mode 100644 +index 0000000000..7d0bb8c8bc +--- /dev/null ++++ b/lib/jscoq_extern.c +@@ -0,0 +1,4 @@ ++#include ++ ++// jsCoq Stub; actual implementation is in backend/jsoo/js_stub/interrupt.js ++value interrupt_pending() { return Val_false; } +-- +2.43.0 + diff --git a/etc/0001-jscoq-lib-system.ml-de-unix-stat.patch b/etc/0001-jscoq-lib-system.ml-de-unix-stat.patch new file mode 100644 index 00000000..49e45b9d --- /dev/null +++ b/etc/0001-jscoq-lib-system.ml-de-unix-stat.patch @@ -0,0 +1,31 @@ +From 389853f5b1cfd0d9af413f52a8a766dc15107806 Mon Sep 17 00:00:00 2001 +From: Emilio Jesus Gallego Arias +Date: Fri, 27 Sep 2024 16:39:19 +0200 +Subject: [PATCH] [jscoq] [lib/system.ml] de-unix-stat + +--- + lib/system.ml | 8 ++++---- + 1 file changed, 4 insertions(+), 4 deletions(-) + +diff --git a/lib/system.ml b/lib/system.ml +index 8f1315c159..a2473c11c9 100644 +--- a/lib/system.ml ++++ b/lib/system.ml +@@ -69,10 +69,10 @@ let apply_subdir f path name = + let base = try Filename.chop_extension name with Invalid_argument _ -> name in + if ok_dirname base then + let path = if path = "." then name else path//name in +- match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with +- | Unix.S_DIR when name = base -> f (FileDir (path,name)) +- | Unix.S_REG -> f (FileRegular name) +- | _ -> () ++ if Sys.is_directory path && name = base then ++ f (FileDir (path,name)) ++ else ++ f (FileRegular name) + + let readdir dir = try Sys.readdir dir with Sys_error _ -> [||] + +-- +2.43.0 + From d7e543c49a4a240826f0af2acee5e0d163c17a15 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 27 Sep 2024 00:43:19 +0200 Subject: [PATCH 3/6] [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 | 27 ++++++++++--- Makefile | 50 ++++++++++++++++++++++- controller-js/README.md | 70 ++++++++++++++++++++++++++++++++- controller-js/coq_lsp_worker.ml | 63 +++++++++++++++++++++++------ controller-js/dune | 40 +++++++++++++++---- controller-js/js_stub/unix.js | 3 ++ controller-js/my_dynload.ml | 42 ++++++++++++++++++++ controller-js/my_dynload.mli | 2 + etc/META.threads | 37 +++++++++++++++++ 9 files changed, 308 insertions(+), 26 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/.github/workflows/build.yml b/.github/workflows/build.yml index 3d1bd616..e8ea7dd5 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -116,21 +116,38 @@ 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: 🚀 Setup node + uses: actions/setup-node@v4 + with: + node-version: 22 + + - name: 🦏🧱🦏 Build coq-lsp VSCode extension 🦏🦏🦏 + 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/README.md + editor/code/CHANGELOG.md + editor/code/syntaxes + editor/code/out/ + editor/code/coq.configuration.json + compression-level: 9 build-opam: name: Opam dev install strategy: @@ -195,7 +212,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 diff --git a/Makefile b/Makefile index 030891c7..aadf72e4 100644 --- a/Makefile +++ b/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 + +_LIBROOT=$(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 $(_LIBROOT) -wholename '*/str/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/seq/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/uri/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/base/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/unix/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/zarith/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/yojson/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/findlib/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/dynlink/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/parsexp/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/sexplib/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/sexplib0/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/bigarray/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/cmdliner/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/ppx_hash/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/angstrom/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/stringext/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/ppx_compare/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/ppx_deriving/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/ppx_sexp_conv/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/memprof-limits/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/ppx_deriving_yojson/META' -printf "%p:/static/lib/%P ") + # These libs are actually linked, so no cma is needed. + # $$(find $(_LIBROOT) -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..cd1c4659 100644 --- a/controller-js/README.md +++ b/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` + diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml index 91e19577..2fabd2f7 100644 --- a/controller-js/coq_lsp_worker.ml +++ b/controller-js/coq_lsp_worker.ml @@ -127,9 +127,31 @@ 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 + 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 }) @@ -154,25 +176,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 = + let coqlib = "/static/coqlib" in + let findlib_config = Some findlib_path in + let ocamlpath = [] in + let vo_load_path = List.map (fun f -> f coqlib) [ stdlib; user_contrib ] in Coq.Workspace.CmdLine. - { coqlib = "/static/coqlib" - ; coqcorelib = "/static/lib/coq-core" - ; findlib_config = Some findlib_path - ; ocamlpath = [] - ; vo_load_path = [ stdlib ] + { coqlib + ; coqcorelib = "/static/lib/coq-core" (* deprecated upstream *) + ; findlib_config + ; 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); diff --git a/controller-js/dune b/controller-js/dune index af7826f5..123b03de 100644 --- a/controller-js/dune +++ b/controller-js/dune @@ -10,12 +10,15 @@ js_stub/coq_vm.js js_stub/coq_perf.js js_stub/interrupt.js + coq-fs-core.js + coq-fs.js marshal-arch.js) (flags :standard + --linkall --dynlink - +dynlink.js - ; (:include .extraflags) + ; --toplevel + (:include .extraflags) ; +toplevel.js ; --enable ; with-js-error @@ -24,13 +27,19 @@ ; --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.dynlink + ; js_of_ocaml-compiler.findlib-support + )) (rule (target coq_lsp_worker.bc.cjs) @@ -40,11 +49,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 user-contrib \\( -wholename 'theories/*.vo' -or -wholename 'theories/*.glob' -or -wholename 'theories/*.v' -or -wholename 'user-contrib/*.vo' -or -wholename 'user-contrib/*.v' -or -wholename 'user-contrib/*.glob' \\) -printf '%p:/static/coqlib/%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/js_stub/unix.js b/controller-js/js_stub/unix.js index a606d9bb..07dbbb7c 100644 --- a/controller-js/js_stub/unix.js +++ b/controller-js/js_stub/unix.js @@ -383,6 +383,9 @@ function unix_open() { unix_ll("unix_open", arguments); } // Provides: unix_putenv // Requires: unix_ll function unix_putenv() { unix_ll("unix_putenv", arguments); } +// Provides: unix_realpath +// Requires: unix_ll +function unix_realpath() { unix_ll("unix_realpath", arguments); } // Provides: unix_recv // Requires: unix_ll function unix_recv() { unix_ll("unix_recv", arguments); } diff --git a/controller-js/my_dynload.ml b/controller-js/my_dynload.ml new file mode 100644 index 00000000..bcec1a3d --- /dev/null +++ b/controller-js/my_dynload.ml @@ -0,0 +1,42 @@ +(* 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..f29c74f1 --- /dev/null +++ b/controller-js/my_dynload.mli @@ -0,0 +1,2 @@ +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]" +) + From a304994b1e9fce8f94301bc5c1799cd3658b6a71 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Sep 2024 16:28:55 +0200 Subject: [PATCH 4/6] [js] [doc] [changes] Changes for javascript support. --- CHANGES.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index a3cb25b6..a225207f 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -19,6 +19,10 @@ #829, thanks to @gmalecha for the idea, c.f. Coq issue 19601) - [fleche] Highlight the full first line of the document on initialization error (@ejgallego, #832) + - [fleche] [jscoq] [js] Build worker version of `coq-lsp`. This + provides a full working Coq enviroment in `vscode.dev`. The web + worker version is build as an artifact on CI (@ejgallego + @corwin-of-amber, #433) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- From 9fa6a0f45005e96fff2520aa71fe48541dca676e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Sep 2024 16:32:17 +0200 Subject: [PATCH 5/6] [doc] [js] More docs on our JS setup. --- controller-js/README.md | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/controller-js/README.md b/controller-js/README.md index cd1c4659..244cc00c 100644 --- a/controller-js/README.md +++ b/controller-js/README.md @@ -18,16 +18,23 @@ information. The worker needs two parts to work: - the worker binary -- the worker filesystem +- the worker OCaml filesystem (`controller-js/coq-fs-core.js`) +- the worker Coq filesystem (`controller-js/coq-fs.js`) which are then bundled in a single `.js` file. -Type +The worker OCaml filesystem includes: +- `META` files for anything used by Coq +- transpiled `.cma` to `.js` files for plugins that will be loaded by Coq + +Type: ``` -make controller-js/coq-fs-core.js && make js +make patch-for-js # (only once, patch Coq for JS build) +make controller-js/coq-fs-core.js # build the OCaml filesystem, needed when plugins change +make js # build the worker and link with the FS. ``` -to build the worker filesystem and the worker, which will be placed under `editor/code/out`. +to get a working build in `editor/code/out`. As of now the build is very artisanal and not flexible at all, we hope to improve it soon. @@ -75,4 +82,3 @@ We need to have most `META` files in findlib, plus the Coq and - `/static/coqlib`: Coq root, with regular paths + `/static/coqlib/theories` + `/static/coqlib/user-contrib` - From ba069246fedcdb7a66852afa770c9de3f117344d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Sep 2024 18:44:22 +0200 Subject: [PATCH 6/6] [gitignore] Update for the JS build --- .gitignore | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.gitignore b/.gitignore index 84104728..b0a73c4e 100644 --- a/.gitignore +++ b/.gitignore @@ -14,3 +14,8 @@ nix/profiles/ # examples config, ignore for now examples/.vscode + +# Related to the JS build and testing +/controller-js/coq-fs-core.js +/controller-js/coq_lsp_worker.bc.cjs +/.vscode-test-web/