From 7101d36e786ac6f58cc97a76da2ee1871cb19c82 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 31 Jan 2023 16:58:27 +0100 Subject: [PATCH] [controller] [js] Initial javascript JSSO coq-lsp controller Finally bootstrapped and working! TODO before merge: - Interrupt (for some reason not working) + we need to rethink the approach anyways I think - Upstream disable uint size check to Coq - Add README with todo - open issues - minimal distribution setup + 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 TODO after merge (turn into issues): - WASM - Package manager (v3) - jsCoq SDK (v2) --- CONTRIBUTING.md | 13 +- Makefile | 6 + controller-js/coq_lsp_worker.ml | 170 ++++++++++ controller-js/coq_lsp_worker.mli | 0 controller-js/dune | 54 ++++ 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 +++++++++++++++++++++++++++++ controller/lsp_core.ml | 6 +- coq/workspace.mli | 7 +- editor/code/src/browser.ts | 60 +++- editor/code/src/goals.ts | 4 +- etc/jscoq-patch-2.diff | 32 ++ etc/jscoq-patch.diff | 13 + examples/documentSymbol.v | 14 +- 18 files changed, 1491 insertions(+), 16 deletions(-) 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_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 create mode 100644 etc/jscoq-patch-2.diff create mode 100644 etc/jscoq-patch.diff diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 4285ffc7..c19f303c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -69,7 +69,7 @@ Dune. ``` 2. Initialize submodules (the `main` branch uses some submodules, which we plan to get rid of soon. Branches `v8.x` can already skip this step.) - + ```sh make submodules-init ``` @@ -85,7 +85,7 @@ Alternatively, you can also use the regular `dune build @check` etc... targets. #### Nix -We have a Nix flake that you can use. +We have a Nix flake that you can use. 1. Dependencies: for development it suffices to run `nix develop` to spawn a shell with the corresponding dependencies. @@ -100,7 +100,7 @@ We have a Nix flake that you can use. ``` 2. Initialize submodules (the `main` branch uses some submodules, which we plan to get rid of soon. Branches `v8.x` can already skip this step.) - + ```sh make submodules-init ``` @@ -154,7 +154,7 @@ Some tips: [ocamlformat]: https://github.com/ocaml-ppx/ocamlformat -### Releasing +## Releasing `coq-lsp` is released using `dune-release tag` + `dune-release`. @@ -175,6 +175,11 @@ The checklist for the release as of today is the following: - [optional] update pre-release packages to coq-opam-archive - [important] bump `version.ml` and `package.json` version string +## Worker version (and debugging tips) + +See https://github.com/ocsigen/js_of_ocaml/issues/410 for debugging +tips with `js_of_ocaml`. + ## Client guide (VS Code Extension) The VS Code extension is setup as a standard `npm` Typescript + React package diff --git a/Makefile b/Makefile index 2f415656..0af08b26 100644 --- a/Makefile +++ b/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 diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml new file mode 100644 index 00000000..f02ddd46 --- /dev/null +++ b/controller-js/coq_lsp_worker.ml @@ -0,0 +1,170 @@ +(* 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 LIO = Lsp.Io +module LSP = Lsp.Base +open Js_of_ocaml +open Controller + +let rec obj_to_json (cobj : < .. > Js.t) : Yojson.Safe.t = + let open Js in + let open Js.Unsafe in + let typeof_cobj = to_string (typeof cobj) in + match typeof_cobj with + | "string" -> `String (to_string @@ coerce cobj) + | "boolean" -> `Bool (to_bool @@ coerce cobj) + | "number" -> `Int (int_of_float @@ float_of_number @@ coerce cobj) + | _ -> + if instanceof cobj array_empty then + `List Array.(to_list @@ map obj_to_json @@ to_array @@ coerce cobj) + else if instanceof cobj Typed_array.arrayBuffer then + `String (Typed_array.String.of_arrayBuffer @@ coerce cobj) + else if instanceof cobj Typed_array.uint8Array then + `String (Typed_array.String.of_uint8Array @@ coerce cobj) + else + let json_string = Js.to_string (Json.output cobj) in + Yojson.Safe.from_string json_string + +let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t = + let open Js.Unsafe in + let ofresh j = json_to_obj (obj [||]) j in + match json with + | `Bool b -> coerce @@ Js.bool b + | `Null -> pure_js_expr "null" + | `Assoc l -> + List.iter (fun (p, js) -> set cobj p (ofresh js)) l; + cobj + | `List l -> Array.(Js.array @@ map ofresh (of_list l)) + | `Float f -> coerce @@ Js.number_of_float f + | `String s -> coerce @@ Js.string s + | `Int m -> coerce @@ Js.number_of_float (float_of_int m) + | `Intlit s -> coerce @@ Js.number_of_float (float_of_string s) + | `Tuple t -> Array.(Js.array @@ map ofresh (of_list t)) + | `Variant (_, _) -> pure_js_expr "undefined" + +let findlib_conf = "\ndestdir=\"/lib\"path=\"/lib\"" + +let lib_fs ~prefix:_ ~path = + match path with + | "findlib.conf" -> Some findlib_conf + | _ -> None + +let setup_pseudo_fs () = + (* '/static' is the default working directory of jsoo *) + Sys_js.unmount ~path:"/static"; + Sys_js.mount ~path:"/lib/" lib_fs + +let setup_std_printers () = + (* XXX Convert to logTrace? *) + (* Sys_js.set_channel_flusher stdout (fun msg -> post_answer (Log (Notice, + Pp.str @@ "stdout: " ^ msg))); *) + (* Sys_js.set_channel_flusher stderr (fun msg -> post_answer (Log (Notice, + Pp.str @@ "stderr: " ^ msg))); *) + () + +let post_message (json : Yojson.Safe.t) = + let js = json_to_obj (Js.Unsafe.obj [||]) json in + Worker.post_message js + +type opaque + +external interrupt_setup : opaque (* Uint32Array *) -> unit = "interrupt_setup" + +let interrupt_is_setup = ref false + +let parse_msg msg = + if Js.instanceof msg Js.array_length then ( + let _method_ = Js.array_get msg 0 in + let handle = Js.array_get msg 1 |> Obj.magic in + interrupt_setup handle; + interrupt_is_setup := true; + Error "processed interrupt_setup") + else obj_to_json msg |> Lsp.Base.Message.from_yojson + +let on_msg msg = + match parse_msg msg with + | Error _ -> + Lsp.Io.logMessage ~lvl:1 ~message:"Error in JSON RPC Message Parsing" + | Ok msg -> + Lsp.Io.trace "interrupt_setup" (string_of_bool !interrupt_is_setup); + Lsp_core.enqueue_message msg + +let setTimeout cb d = Dom_html.setTimeout cb d + +let rec process_queue ~state () = + match Lsp_core.dispatch_or_resume_check ~ofn:post_message ~state with + | None -> + LIO.trace "proccess queue" "ended"; + () + | Some (Yield state) -> ignore (setTimeout (process_queue ~state) 0.1) + | Some (Cont state) -> process_queue ~state () + +let on_init ~root_state ~cmdline ~debug msg = + match parse_msg msg with + | Error _ -> () + | Ok msg -> ( + match Lsp_core.lsp_init_process ~ofn:post_message ~cmdline ~debug msg with + | Lsp_core.Init_effect.Exit -> (* XXX: bind to worker.close () *) () + | Lsp_core.Init_effect.Loop -> () + | Lsp_core.Init_effect.Success workspaces -> + Worker.set_onmessage on_msg; + let state = { Lsp_core.State.root_state; cmdline; workspaces } in + ignore (setTimeout (process_queue ~state) 0.1)) + +let coq_init ~debug = + let load_module = Dynlink.loadfile in + let load_plugin = Coq.Loader.plugin_handler None in + Coq.Init.(coq_init { debug; load_module; load_plugin }) + +let lsp_cb = + Fleche.Io.CallBack. + { trace = Lsp.Io.trace + ; send_diagnostics = + (fun ~ofn ~uri ~version diags -> + Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn) + ; send_fileProgress = + (fun ~ofn ~uri ~version progress -> + Lsp.JFleche.mk_progress ~uri ~version progress |> ofn) + } + +external coq_vm_trap : unit -> unit = "coq_vm_trap" + +(* This code is executed on Worker initialization *) +let main () = + (* This is needed if dynlink is enabled in 4.03.0 *) + Sys.interactive := false; + + setup_pseudo_fs (); + setup_std_printers (); + + (* setup_interp (); *) + coq_vm_trap (); + + Lsp.Io.set_log_fn post_message; + Fleche.Io.CallBack.set lsp_cb; + + let cmdline = + Coq.Workspace.CmdLine. + { coqlib = "/lib/coq" + ; coqcorelib = "/lib/coq" + ; ocamlpath = Some "/lib" + ; vo_load_path = [] + ; ml_include_path = [] + ; args = [ "-noinit" ] + } + in + let debug = true in + let root_state = coq_init ~debug in + Worker.set_onmessage (on_init ~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..022498a0 --- /dev/null +++ b/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} ')'")))) 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/controller/lsp_core.ml b/controller/lsp_core.ml index ab2541ba..2375b89a 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -23,7 +23,11 @@ module F = Format module J = Yojson.Safe module U = Yojson.Safe.Util -let field name dict = List.(assoc name dict) +let field name dict = + try List.(assoc name dict) + with Not_found -> + raise (U.Type_error ("field " ^ name ^ " not found", `Assoc dict)) + let int_field name dict = U.to_int (field name dict) let dict_field name dict = U.to_assoc (field name dict) let list_field name dict = U.to_list (field name dict) diff --git a/coq/workspace.mli b/coq/workspace.mli index 4aa103e3..1e859af6 100644 --- a/coq/workspace.mli +++ b/coq/workspace.mli @@ -22,15 +22,18 @@ module Flags : sig } end +(* Generated from a _CoqProject, dune (in the future) or command line args *) type t = private { coqlib : string ; coqcorelib : string ; ocamlpath : string option ; vo_load_path : Loadpath.vo_path list - ; ml_include_path : string list + (** List of -R / -Q flags passed to Coq, usually theories we depend on *) + ; ml_include_path : string list (** List of paths to look for Coq plugins *) ; require_libs : (string * string option * Vernacexpr.export_with_cats option) list - ; flags : Flags.t + (** Modules to preload, usually Coq.Init.Prelude *) + ; flags : Flags.t (** Coq-specific flags *) ; kind : string (** How the workspace was built *) ; debug : bool (** Enable backtraces *) } diff --git a/editor/code/src/browser.ts b/editor/code/src/browser.ts index 3164eb48..8d1bdb6d 100644 --- a/editor/code/src/browser.ts +++ b/editor/code/src/browser.ts @@ -1,22 +1,70 @@ -import { ExtensionContext } from "vscode"; -import { LanguageClient } from "vscode-languageclient/browser"; +import { ExtensionContext, Uri } from "vscode"; +import { CancellationToken, LanguageClient, LanguageClientOptions, MessageSignature, NotificationType, NotificationType0, ProtocolNotificationType, ProtocolNotificationType0, ProtocolRequestType, ProtocolRequestType0, RequestType, RequestType0 } from "vscode-languageclient/browser"; import { activateCoqLSP, ClientFactoryType, deactivateCoqLSP } from "./client"; +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]); + } + } + + public interrupt() { + if(this.interrupt_vec) { Atomics.add(this.interrupt_vec, 0, 1); } + } + + public sendRequest(type: ProtocolRequestType0, token?: CancellationToken): Promise; + public sendRequest(type: ProtocolRequestType, params: P, token?: CancellationToken): Promise; + public sendRequest(type: RequestType0, token?: CancellationToken): Promise; + public sendRequest(type: RequestType, params: P, token?: CancellationToken): Promise; + public sendRequest(method: string, token?: CancellationToken): Promise; + public sendRequest(method: string, param: any, token?: CancellationToken): Promise; + public async sendRequest(type: string | MessageSignature, ...params: any[]): Promise { + this.interrupt(); + let ty = type as string; + return super.sendRequest(ty, ...params); + } + + public sendNotification(type: ProtocolNotificationType0): Promise; + public sendNotification(type: ProtocolNotificationType, params?: P): Promise; + public sendNotification(type: NotificationType0): Promise; + public sendNotification

(type: NotificationType

, params?: P): Promise; + public sendNotification(method: string): Promise; + public sendNotification(method: string, params: any): Promise; + public async sendNotification

(type: string | MessageSignature, params?: P): Promise { + this.interrupt(); + let ty = type as NotificationType

; + return super.sendNotification

(ty, params); + } +} + 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; }; activateCoqLSP(context, cf); } export function deactivate() { deactivateCoqLSP(); -} +} \ No newline at end of file diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts index 1866e330..22bb01fd 100644 --- a/editor/code/src/goals.ts +++ b/editor/code/src/goals.ts @@ -12,6 +12,7 @@ import { RequestType, VersionedTextDocumentIdentifier, } from "vscode-languageclient"; +import * as LSP from "vscode-languageserver-types"; import { GoalRequest, GoalAnswer, PpString } from "../lib/types"; const infoReq = new RequestType, void>( @@ -110,12 +111,13 @@ export class InfoPanel { client: BaseLanguageClient, uri: Uri, version: number, - position: Position + vsPos: Position ) { let textDocument = VersionedTextDocumentIdentifier.create( uri.toString(), version ); + let position : LSP.Position = LSP.Position.create(vsPos.line, vsPos.character) let cursor: GoalRequest = { textDocument, position }; this.sendGoalsRequest(client, cursor); } diff --git a/etc/jscoq-patch-2.diff b/etc/jscoq-patch-2.diff new file mode 100644 index 00000000..7a76cb1d --- /dev/null +++ b/etc/jscoq-patch-2.diff @@ -0,0 +1,32 @@ +diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml +index 1d2496e660..0afaaa9bf8 100644 +--- a/kernel/uint63_63.ml ++++ b/kernel/uint63_63.ml +@@ -10,7 +10,7 @@ + + type t = int + +-let _ = assert (Sys.word_size = 64) ++(* let _ = assert (Sys.word_size = 64) *) + + let uint_size = 63 + +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/etc/jscoq-patch.diff b/etc/jscoq-patch.diff new file mode 100644 index 00000000..4c122534 --- /dev/null +++ b/etc/jscoq-patch.diff @@ -0,0 +1,13 @@ +diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml +index 1d2496e660..0afaaa9bf8 100644 +--- a/kernel/uint63_63.ml ++++ b/kernel/uint63_63.ml +@@ -10,7 +10,7 @@ + + type t = int + +-let _ = assert (Sys.word_size = 64) ++(* let _ = assert (Sys.word_size = 64) *) + + let uint_size = 63 + diff --git a/examples/documentSymbol.v b/examples/documentSymbol.v index 06cf6e4f..6a587782 100644 --- a/examples/documentSymbol.v +++ b/examples/documentSymbol.v @@ -3,10 +3,20 @@ Record a := { ; proj2 : Type }. +Notation "A -> B" := (forall (_ : A), B) (at level 99, B at level 200). Inductive foo := A | B : a -> foo. +Inductive aba := C. + Inductive eh1 := Ah1 : eh2 -> eh1 -with eh2 := Bh1 : eh1 -> eh2. +with eh2 := Bh1 : eh1 -> eh2. + +Definition mu := forall (x : Type), x. + +Inductive False := . + +Inductive nat := O | S : nat -> nat. +Inductive bool := true | false. Variable (j : nat). @@ -42,4 +52,4 @@ Module Bar. Theorem not : False. Qed. -End Bar. \ No newline at end of file +End Bar.