From b26437a7cad136f5a15f133409094b15457baaec Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 27 Sep 2024 00:43:19 +0200 Subject: [PATCH] [js] Build working filesystem for findlib-based worker. We hook `loadfile` to use precompiled `.cma.js` files, using our copy of findlib. The build is very rustical, but works. We also tweak the VM options so they are correct. --- .github/workflows/build.yml | 23 +++++-- Makefile | 50 ++++++++++++++- compiler/driver.ml | 3 +- controller-js/README.md | 70 ++++++++++++++++++++- controller-js/coq_lsp_worker.ml | 104 ++++++++++++++++++-------------- controller-js/dune | 40 +++++++++--- controller-js/js_stub/unix.js | 5 +- controller-js/my_dynload.ml | 42 +++++++++++++ controller-js/my_dynload.mli | 2 + controller/coq_lsp.ml | 3 +- coq/init.ml | 7 ++- coq/init.mli | 2 + coq/protect.ml | 3 +- etc/META.threads | 37 ++++++++++++ petanque/json_shell/shell.ml | 3 +- 15 files changed, 328 insertions(+), 66 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..40bcfc98 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -116,21 +116,34 @@ 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: 🦏🧱🦏 Build coq-lsp VSCode extension 🦏🦏🦏 + uses: actions/setup-node@v4 + with: + node-version: 22 + 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/syntaxes + editor/code/out/ + editor/code/coq.configuration.json + compression-level: 9 build-opam: name: Opam dev install strategy: @@ -195,7 +208,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..baf2d468 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 + +OPAMROOT=$(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 $(OPAMROOT) -wholename '*/str/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/seq/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/uri/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/base/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/unix/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/zarith/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/yojson/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/findlib/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/dynlink/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/parsexp/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/sexplib/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/sexplib0/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/bigarray/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/cmdliner/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/ppx_hash/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/angstrom/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/stringext/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/ppx_compare/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/ppx_deriving/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/ppx_sexp_conv/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/memprof-limits/META' -printf "%p:/static/lib/%P ") \ + $$(find $(OPAMROOT) -wholename '*/ppx_deriving_yojson/META' -printf "%p:/static/lib/%P ") + # These libs are actually linked, so no cma is needed. + # $$(find $(OPAMROOT) -wholename '*/zarith/*.cma' -printf "%p:/static/lib/%P " -or -wholename '*/zarith/META' -printf "%p:/static/lib/%P ") + cp _build/install/default/lib/coq-fs-core.js controller-js + +# Serlib plugins require: +# ppx_compare.runtime-lib +# ppx_deriving.runtime +# ppx_deriving_yojson.runtime +# ppx_hash.runtime-lib +# ppx_sexp_conv.runtime-lib diff --git a/compiler/driver.ml b/compiler/driver.ml index 08bd8e18..fb2da9de 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -2,7 +2,8 @@ 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 vm, warnings = (true, None) in + Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings }) let replace_test_path exp message = let home_re = Str.regexp (exp ^ ".*$") in 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 13c7c80f..b341ee45 100644 --- a/controller-js/coq_lsp_worker.ml +++ b/controller-js/coq_lsp_worker.ml @@ -14,27 +14,6 @@ module LSP = Lsp.Base open Js_of_ocaml open Controller -let verb = true - -let _coq_cma_link ~file_path = - let open Format in - (* Coq doesn't append the extension anymore when submitting this *) - let cmo_file = file_path ^ ".cma" in - if verb then eprintf "bytecode file %s requested\n%!" cmo_file; - try - let js_code = Sys_js.read_file ~name:(cmo_file ^ ".js") in - let js_code = - if String.sub js_code 0 1 = "(" then js_code - else "(" ^ js_code ^ ")" (* jsoo < 4.0 *) - in - (* When eval'ed, the js_code will return a closure waiting for the jsoo - global object to link the plugin. *) - Ok Js.Unsafe.((eval_string js_code : < .. > Js.t -> unit) global) - with Sys_error _ -> - eprintf "!! bytecode file %s{,.js} not found in path. DYNLINK FAILED\n%!" - cmo_file; - Error cmo_file - let rec obj_to_json (cobj : < .. > Js.t) : Yojson.Safe.t = let open Js in let open Js.Unsafe in @@ -71,25 +50,16 @@ let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t = | `Tuple t -> Array.(Js.array @@ map ofresh (of_list t)) | `Variant (_, _) -> pure_js_expr "undefined" -let findlib_conf = "\ndestdir=\"/lib\"path=\"/lib\"" - -let lib_fs ~prefix:_ ~path = - match path with - | "findlib.conf" -> Some findlib_conf - | _ -> None +let findlib_conf = "\ndestdir=\"/static/lib\"path=\"/static/lib\"" let setup_pseudo_fs () = (* '/static' is the default working directory of jsoo *) - (* Sys_js.unmount ~path:"/static"; *) - Sys_js.mount ~path:"/lib/" lib_fs; + Sys_js.create_file ~name:"/static/lib/findlib.conf" ~content:findlib_conf; () let setup_std_printers () = - (* XXX Convert to logTrace? *) - (* Sys_js.set_channel_flusher stdout (fun msg -> post_answer (Log (Notice, - Pp.str @@ "stdout: " ^ msg))); *) - (* Sys_js.set_channel_flusher stderr (fun msg -> post_answer (Log (Notice, - Pp.str @@ "stderr: " ^ msg))); *) + Sys_js.set_channel_flusher stdout (Fleche.Io.Log.trace "stdout" "%s"); + Sys_js.set_channel_flusher stderr (Fleche.Io.Log.trace "stderr" "%s"); () let post_message (msg : Lsp.Base.Message.t) = @@ -156,10 +126,34 @@ 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 - Coq.Init.(coq_init { debug; load_module; load_plugin }) + 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 }) external coq_vm_trap : unit -> unit = "coq_vm_trap" @@ -181,24 +175,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 = + (* Needs overriding as otherwise will use the setting of the + compilation context, see if /static/findlib.conf is right *) + let ocamlpath = Some "/static/lib" in + let coqlib = "/static/coqlib" in + let vo_load_path = List.map (fun f -> f coqlib) [ stdlib; user_contrib ] in Coq.Workspace.CmdLine. - { coqlib = "/static/coq" - ; coqcorelib = "/static/coq" - ; ocamlpath = Some "/lib" - ; vo_load_path = [ stdlib ] + { coqlib + ; coqcorelib = "/static/lib/coq-core" (* deprecated upstream *) + ; 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..50600199 100644 --- a/controller-js/js_stub/unix.js +++ b/controller-js/js_stub/unix.js @@ -383,7 +383,10 @@ 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 +// Provides: unix_realpath +// Requires: unix_ll +function unix_realpath() { unix_ll("unix_realpath", arguments); } +// Provides: unix_recvfrom // Requires: unix_ll function unix_recv() { unix_ll("unix_recv", arguments); } // Provides: unix_recvfrom 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/controller/coq_lsp.ml b/controller/coq_lsp.ml index fe410bd2..63a09e46 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -63,7 +63,8 @@ let concise_cb ofn = 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 vm, warnings = (true, None) in + Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings }) let exit_notification = Lsp.Base.Message.(Notification { method_ = "exit"; params = [] }) diff --git a/coq/init.ml b/coq/init.ml index b91c47c1..3eaeaf4f 100644 --- a/coq/init.ml +++ b/coq/init.ml @@ -23,6 +23,8 @@ type coq_opts = ; load_plugin : Mltop.PluginSpec.t -> unit (** callback to load findlib packages *) ; debug : bool (** Enable Coq Debug mode *) + ; vm : bool (** Enable Coq's VM *) + ; warnings : string option (** Coq's Warnings *) } let coq_lvl_to_severity (lvl : Feedback.level) = @@ -46,7 +48,7 @@ let mk_fb_handler q Feedback.{ contents; _ } = let coq_init opts = (* Core Coq initialization *) Lib.init (); - Global.set_impredicative_set false; + Global.set_VM opts.vm; Global.set_native_compiler false; if opts.debug then CDebug.set_flags "backtrace"; @@ -70,6 +72,9 @@ let coq_init opts = in Mltop.set_top ser_mltop; + (* Maybe set warnings *) + Option.iter CWarnings.set_flags opts.warnings; + (* This should go away in Coq itself *) Safe_typing.allow_delayed_constants := true; diff --git a/coq/init.mli b/coq/init.mli index a0720aea..e9822255 100644 --- a/coq/init.mli +++ b/coq/init.mli @@ -23,6 +23,8 @@ type coq_opts = ; load_plugin : Mltop.PluginSpec.t -> unit (** callback to load findlib packages *) ; debug : bool (** Enable Coq Debug mode *) + ; vm : bool (** Enable Coq's VM *) + ; warnings : string option (** Coq's Warnings *) } val coq_init : coq_opts -> State.t diff --git a/coq/protect.ml b/coq/protect.ml index c768e1e9..d345edb5 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -36,7 +36,8 @@ end let eval_exn ~token ~f x = match Limits.limit ~token ~f x with | Ok res -> R.Completed (Ok res) - | Error _ -> + (* Useful in the JS worker, but beware... *) + | (exception Stack_overflow) | Error _ -> Vernacstate.Interp.invalidate_cache (); R.Interrupted | exception exn -> 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]" +) + diff --git a/petanque/json_shell/shell.ml b/petanque/json_shell/shell.ml index 3d4324b4..b7097be0 100644 --- a/petanque/json_shell/shell.ml +++ b/petanque/json_shell/shell.ml @@ -1,7 +1,8 @@ let init_coq ~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 vm, warnings = (true, None) in + Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings }) let cmdline : Coq.Workspace.CmdLine.t = { coqlib = Coq_config.coqlib