diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 643dfac6..6e2ab363 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -60,7 +60,7 @@ jobs: steps: - name: 🔭 Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: submodules: recursive @@ -83,6 +83,69 @@ 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-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 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/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 Install strategy: @@ -90,7 +153,7 @@ jobs: runs-on: ubuntu-latest steps: - name: 🔭 Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: submodules: recursive @@ -121,11 +184,11 @@ jobs: working-directory: ./editor/code steps: - name: 🔭 Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: 🚀 Setup node - uses: actions/setup-node@v3 + uses: actions/setup-node@v4 with: - node-version: 18 + node-version: 22 - run: npm ci - run: npx --yes @vscode/vsce ls @@ -134,7 +197,7 @@ jobs: runs-on: ubuntu-latest steps: - name: 🔭 Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: submodules: recursive - name: ❄️ Setup Nix 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/ diff --git a/CHANGES.md b/CHANGES.md index bcc7ad96..de4884e1 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,40 @@ +# unreleased +------------ + + - [deps] Bump toolchain so minimal `ppxlib` is 0.26, in order to fix + some `ppx_import` oddities. This means our lower bound for the Jane + Street packages is now `v0.15`, which should be fine for the + foreseeable future (@ejgallego, #813) + - [workspace] [coq] Support _CoqProject arguments `-type-in-type` and + `-allow-rewrite-rules` (for 8.20) (@ejgallego, #819) + - [serlib] Support for ltac2_ltac1 plugin (@ejgallego, #820) + - [serlib] Fix Ltac2 AST piercing bug, add test case that should help + in the future (@ejgallego, @jim-portegies, #821) + - [fleche] [8.20] understand rewrite rules and symbols on document + outline (@ejgallego, @Alizter, #825, fixes #824) + - [fleche] [coq] support `Restart` meta command (@ejgallego, + @Alizter, #828, fixes #827) + - [fleche] [plugins] New plugin example `explain_errors`, that will + print all errors on a file, with their goal context (@ejgallego, + #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) + - [hover] Fix universe and level printing in hover (#839, fixes #835 + , @ejgallego , @Alizter) + - [fleche] New immediate request serving mode. In this mode, requests + are served with whatever document state we have. This is very + useful when we are not in continuous mode, and we don't have a good + reference as to what to build, for example in + `documentSymbols`. The mode actually works pretty well in practice + as often language requests will come after goals requests, so the + info that is needed is at hand. It could also be tried to set the + build target for immediate requests to the view hint, but we should + see some motivation for that (@ejgallego, #841) + # coq-lsp 0.2.0: From Green to Blue ----------------------------------- 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 b6a968ae..26f6e481 100644 --- a/Makefile +++ b/Makefile @@ -1,3 +1,5 @@ +SHELL := /usr/bin/env bash + COQ_BUILD_CONTEXT=../_build/default/coq PKG_SET= coq-lsp.install @@ -44,6 +46,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 @@ -52,6 +56,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 @@ -69,6 +74,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 --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 coq_boot: # We do nothing for released versions @@ -132,3 +144,54 @@ make-fmt: build fmt opam-update-and-reinstall: git pull 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 + +_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/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/compiler/fcc.ml b/compiler/fcc.ml index dd990ad3..55c77d4b 100644 --- a/compiler/fcc.ml +++ b/compiler/fcc.ml @@ -3,14 +3,15 @@ open Cmdliner open Fcc_lib let fcc_main int_backend roots display debug plugins files coqlib coqcorelib - ocamlpath rload_path load_path require_libraries no_vo max_errors - coq_diags_level = + findlib_config ocamlpath rload_path load_path require_libraries no_vo + max_errors coq_diags_level = let vo_load_path = rload_path @ load_path in let ml_include_path = [] in let args = [] in let cmdline = { Coq.Workspace.CmdLine.coqlib ; coqcorelib + ; findlib_config ; ocamlpath ; vo_load_path ; ml_include_path @@ -100,8 +101,8 @@ let fcc_cmd : int Cmd.t = let open Coq.Args in Term.( const fcc_main $ int_backend $ roots $ display $ debug $ plugins $ file - $ coqlib $ coqcorelib $ ocamlpath $ rload_paths $ qload_paths $ ri_from - $ no_vo $ max_errors $ coq_diags_level) + $ coqlib $ coqcorelib $ findlib_config $ ocamlpath $ rload_paths + $ qload_paths $ ri_from $ no_vo $ max_errors $ coq_diags_level) in let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term) diff --git a/controller-js/README.md b/controller-js/README.md new file mode 100644 index 00000000..244cc00c --- /dev/null +++ b/controller-js/README.md @@ -0,0 +1,84 @@ +## coq-lsp Web Worker README + +This directory contains the implementation of our LSP-compliant web +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 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. + +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 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 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. + +## 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 new file mode 100644 index 00000000..57d82577 --- /dev/null +++ b/controller-js/coq_lsp_worker.ml @@ -0,0 +1,220 @@ +(* 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 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 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" + +(* 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 coqlib = + let unix_path = Filename.concat coqlib "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 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 + ; coqcorelib = "/static/lib/coq-core" (* deprecated upstream *) + ; findlib_config + ; ocamlpath + ; vo_load_path + ; ml_include_path = [] + ; require_libraries = [ (None, "Coq.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); + () + +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..123b03de --- /dev/null +++ b/controller-js/dune @@ -0,0 +1,85 @@ +(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 + coq-fs-core.js + coq-fs.js + marshal-arch.js) + (flags + :standard + --linkall + --dynlink + ; --toplevel + (:include .extraflags) + ; +toplevel.js + ; --enable + ; with-js-error + ; --enable + ; debuginfo + ; --no-inline + ; --debug-info + ; --source-map + ; --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 + ; js_of_ocaml-toplevel + ; js_of_ocaml-compiler.dynlink + ; js_of_ocaml-compiler.findlib-support + )) + +(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}))) + +(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) + +(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..07dbbb7c --- /dev/null +++ b/controller-js/js_stub/unix.js @@ -0,0 +1,505 @@ +//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_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); } +// 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-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 3d7746cb..aeaebb46 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -60,42 +60,11 @@ let concise_cb ofn = } (* Main loop *) -module CB (O : sig - val ofn : Lsp.Base.Notification.t -> unit -end) = -struct - let ofn = O.ofn - let trace _hdr ?extra message = Lsp.Io.logTrace ~message ~extra - let message ~lvl ~message = Lsp.Io.logMessage ~lvl ~message - - let diagnostics ~uri ~version diags = - Lsp.Core.mk_diagnostics ~uri ~version diags |> ofn - - let fileProgress ~uri ~version progress = - Lsp.JFleche.mk_progress ~uri ~version progress |> ofn - - let perfData ~uri ~version perf = - Lsp.JFleche.mk_perf ~uri ~version perf |> ofn - - let serverVersion vi = Lsp.JFleche.mk_serverVersion vi |> ofn - let serverStatus st = Lsp.JFleche.mk_serverStatus st |> ofn - - let cb = - Fleche.Io.CallBack. - { trace - ; message - ; diagnostics - ; fileProgress - ; perfData - ; serverVersion - ; serverStatus - } -end - 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 = [] }) @@ -112,8 +81,8 @@ let rec lsp_init_loop ~io ~ifn ~ofn ~cmdline ~debug = L.trace "read_request" "error: %s" err; lsp_init_loop ~io ~ifn ~ofn ~cmdline ~debug -let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path - require_libraries delay int_backend = +let lsp_main bt coqcorelib coqlib findlib_config ocamlpath vo_load_path + ml_include_path require_libraries delay int_backend = Coq.Limits.select_best int_backend; Coq.Limits.start (); @@ -130,7 +99,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path Lsp.Io.set_log_fn ofn_ntn; - let module CB = CB (struct + let module CB = Lsp_core.CB (struct let ofn = ofn_ntn end) in let io = CB.cb in @@ -145,6 +114,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path let cmdline = { Coq.Workspace.CmdLine.coqcorelib ; coqlib + ; findlib_config ; ocamlpath ; vo_load_path ; ml_include_path @@ -231,8 +201,8 @@ let lsp_cmd : unit Cmd.t = v (Cmd.info "coq-lsp" ~version:Fleche.Version.server ~doc ~man) Term.( - const lsp_main $ bt $ coqcorelib $ coqlib $ ocamlpath $ vo_load_path - $ ml_include_path $ ri_from $ delay $ int_backend)) + const lsp_main $ bt $ coqcorelib $ coqlib $ findlib_config $ ocamlpath + $ vo_load_path $ ml_include_path $ ri_from $ delay $ int_backend)) let main () = let ecode = Cmd.eval lsp_cmd in diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 62963a07..eb33483e 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 list_field name dict = U.to_list (field name dict) let string_field name dict = U.to_string (field name dict) @@ -398,7 +402,16 @@ let do_document_request_maybe ~params ~handler = let postpone = not !Fleche.Config.v.check_only_on_request in do_document_request ~postpone ~params ~handler -let do_symbols = do_document_request_maybe ~handler:Rq_symbols.symbols +let do_immediate ~params ~handler = + let uri = Helpers.get_uri params in + Rq.Action.Data (Request.Data.Immediate { uri; handler }) + +(* new immediate mode, cc: #816 *) +let do_symbols ~params = + let handler = Rq_symbols.symbols in + if !Fleche.Config.v.check_only_on_request then do_immediate ~params ~handler + else do_document_request ~postpone:true ~params ~handler + let do_document = do_document_request_maybe ~handler:Rq_document.request let do_save_vo = do_document_request_maybe ~handler:Rq_save.request let do_lens = do_document_request_maybe ~handler:Rq_lens.request @@ -710,3 +723,35 @@ let enqueue_message (com : LSP.Message.t) = general, to perform queue optimizations *) LspQueue.push_and_optimize com; set_current_token () + +module CB (O : sig + val ofn : Lsp.Base.Notification.t -> unit +end) = +struct + let ofn = O.ofn + let trace _hdr ?extra message = Lsp.Io.logTrace ~message ~extra + let message ~lvl ~message = Lsp.Io.logMessage ~lvl ~message + + let diagnostics ~uri ~version diags = + Lsp.Core.mk_diagnostics ~uri ~version diags |> ofn + + let fileProgress ~uri ~version progress = + Lsp.JFleche.mk_progress ~uri ~version progress |> ofn + + let perfData ~uri ~version perf = + Lsp.JFleche.mk_perf ~uri ~version perf |> ofn + + let serverVersion vi = Lsp.JFleche.mk_serverVersion vi |> ofn + let serverStatus st = Lsp.JFleche.mk_serverStatus st |> ofn + + let cb = + Fleche.Io.CallBack. + { trace + ; message + ; diagnostics + ; fileProgress + ; perfData + ; serverVersion + ; serverStatus + } +end diff --git a/controller/lsp_core.mli b/controller/lsp_core.mli index 0b9368a3..eb3aac4b 100644 --- a/controller/lsp_core.mli +++ b/controller/lsp_core.mli @@ -63,3 +63,10 @@ val dispatch_or_resume_check : (** Add a message to the queue *) val enqueue_message : Lsp.Base.Message.t -> unit + +(** Generic output handler *) +module CB (O : sig + val ofn : Lsp.Base.Notification.t -> unit +end) : sig + val cb : Fleche.Io.CallBack.t +end diff --git a/controller/request.ml b/controller/request.ml index f2acdb11..3ea2fac4 100644 --- a/controller/request.ml +++ b/controller/request.ml @@ -48,6 +48,10 @@ type position = (** Requests that require data access *) module Data = struct type t = + | Immediate of + { uri : Lang.LUri.File.t + ; handler : document + } | DocRequest of { uri : Lang.LUri.File.t ; postpone : bool @@ -63,6 +67,7 @@ module Data = struct (* Debug printing *) let data fmt = function + | Immediate { uri = _; handler = _ } -> Format.fprintf fmt "{k:imm }" | DocRequest { uri = _; postpone; handler = _ } -> Format.fprintf fmt "{k:doc | p: %B}" postpone | PosRequest { uri = _; point; version; postpone; handler = _ } -> @@ -73,6 +78,8 @@ module Data = struct let dm_request pr = match pr with + | Immediate { uri; handler = _ } -> + (uri, false, Fleche.Theory.Request.Immediate) | DocRequest { uri; postpone; handler = _ } -> (uri, postpone, Fleche.Theory.Request.FullDoc) | PosRequest { uri; point; version; postpone; handler = _ } -> @@ -80,6 +87,7 @@ module Data = struct let serve ~token ~doc pr = match pr with + | Immediate { uri = _; handler } -> handler ~token ~doc | DocRequest { uri = _; postpone = _; handler } -> handler ~token ~doc | PosRequest { uri = _; point; version = _; postpone = _; handler } -> handler ~token ~point ~doc diff --git a/controller/request.mli b/controller/request.mli index da4f5b41..d760381d 100644 --- a/controller/request.mli +++ b/controller/request.mli @@ -35,6 +35,10 @@ type position = (** Requests that require data access *) module Data : sig type t = + | Immediate of + { uri : Lang.LUri.File.t + ; handler : document + } | DocRequest of { uri : Lang.LUri.File.t ; postpone : bool diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index cc2ae3af..a1b062dc 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -12,10 +12,28 @@ let build_ind_type mip = Inductive.type_of_inductive mip type id_info = | Notation of Pp.t - | Def of (Pp.t * Names.Constant.t option * string option) - -let info_of_ind env sigma ((sp, i) : Names.Ind.t) = + | Def of + { typ : Pp.t (** type of the ide *) + ; params : Pp.t (** params that need display next to the name *) + ; full_path : Pp.t option + (** full path of the constant, if any, for example + [Stdlib.Lists.map] *) + ; source : string option (** filename where the constant is located *) + } + +let print_params env sigma params = + if CList.is_empty params then Pp.mt () + else Pp.(spc () ++ Printer.pr_rel_context env sigma params ++ brk (1, 2)) + +let info_of_ind env ((sp, i) : Names.Ind.t) = + let udecl = None in let mib = Environ.lookup_mind sp env in + let bl = + Printer.universe_binders_with_opt_names + (Declareops.inductive_polymorphic_context mib) + udecl + in + let sigma = Evd.from_ctx (UState.of_names bl) in let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in @@ -37,26 +55,56 @@ let info_of_ind env sigma ((sp, i) : Names.Ind.t) = (Impargs.implicits_of_global (Names.GlobRef.IndRef (sp, i))) in let impargs = List.map Impargs.binding_kind_of_status impargs in - Def (Printer.pr_ltype_env ~impargs env_params sigma arity, None, None) + let inst = + if Declareops.inductive_is_polymorphic mib then + Printer.pr_universe_instance sigma u + else Pp.mt () + in + let params = EConstr.Unsafe.to_rel_context params in + let typ = Printer.pr_ltype_env ~impargs env_params sigma arity in + let params = Pp.(inst ++ print_params env sigma params) in + let full_path = Some (Names.MutInd.print sp) in + let source = + let dp = Names.MutInd.modpath sp |> Names.ModPath.dp in + Coq.Module.(make dp |> Result.to_option |> Option.map source) + in + Def { typ; params; full_path; source } let type_of_constant cb = cb.Declarations.const_type -let info_of_const env sigma cr = +let info_of_const env cr = + let udecl = None in let cdef = Environ.lookup_constant cr env in + let bl = + Printer.universe_binders_with_opt_names + (Environ.constant_context env cr) + udecl + in + let sigma = Evd.from_ctx (UState.of_names bl) in (* This prints the definition *) (* let cb = Environ.lookup_constant cr env in *) (* Option.cata (fun (cb,_univs,_uctx) -> Some cb ) None *) (* (Global.body_of_constant_body Library.indirect_accessor cb), *) let typ = type_of_constant cdef in + let univs = Declareops.constant_polymorphic_context cdef in + let inst = Univ.make_abstract_instance univs in let impargs = Impargs.select_stronger_impargs (Impargs.implicits_of_global (Names.GlobRef.ConstRef cr)) in let impargs = List.map Impargs.binding_kind_of_status impargs in let typ = Printer.pr_ltype_env env sigma ~impargs typ in - let dp = Names.Constant.modpath cr |> Names.ModPath.dp in - let source = Coq.Module.(make dp |> Result.to_option |> Option.map source) in - Def (typ, Some cr, source) + let inst = + if Environ.polymorphic_constant cr env then + Printer.pr_universe_instance sigma inst + else Pp.mt () + in + let full_path = Some (Names.Constant.print cr) in + let source = + let dp = Names.Constant.modpath cr |> Names.ModPath.dp in + Coq.Module.(make dp |> Result.to_option |> Option.map source) + in + Def { typ; params = inst; full_path; source } let info_of_var env vr = let vdef = Environ.lookup_named vr env in @@ -73,7 +121,13 @@ let info_of_constructor env cr = in ctype -let print_type env sigma x = Def (Printer.pr_ltype_env env sigma x, None, None) +let print_type env sigma x = + Def + { typ = Printer.pr_ltype_env env sigma x + ; params = Pp.mt () + ; full_path = None + ; source = None + } let info_of_id env sigma id = let qid = Libnames.qualid_of_string id in @@ -89,8 +143,8 @@ let info_of_id env sigma id = let open Names.GlobRef in (match lid with | VarRef vr -> info_of_var env vr |> print_type env sigma - | ConstRef cr -> info_of_const env sigma cr - | IndRef ir -> info_of_ind env sigma ir + | ConstRef cr -> info_of_const env cr + | IndRef ir -> info_of_ind env ir | ConstructRef cr -> info_of_constructor env cr |> print_type env sigma) |> fun x -> Some x | Abbrev kn -> Some (Notation (Prettyp.print_abbreviation env kn)) @@ -115,20 +169,19 @@ let info_of_id_at_point ~token ~node id = let pp_cr fmt = function | None -> () - | Some cr -> - Format.fprintf fmt " - **full path**: `%a`@\n" Pp.pp_with - (Names.Constant.print cr) + | Some cr -> Format.fprintf fmt " - **full path**: `%a`@\n" Pp.pp_with cr let pp_file fmt = function | None -> () | Some file -> Format.fprintf fmt " - **in file**: `%s`" file let pp_typ id = function - | Def (typ, cr, file) -> + | Def { typ; params; full_path; source } -> let typ = Pp.string_of_ppcmds typ in + let param = Pp.string_of_ppcmds params in Format.( - asprintf "@[```coq\n%s : %s@\n```@\n@[%a@]@[%a@]@]" id typ pp_cr cr - pp_file file) + asprintf "@[```coq\n%s%s: %s@\n```@\n@[%a@]@[%a@]@]" id param typ pp_cr + full_path pp_file source) | Notation nt -> let nt = Pp.string_of_ppcmds nt in Format.(asprintf "```coq\n%s\n```" nt) @@ -170,8 +223,10 @@ let info_notation ~point (ast : Fleche.Doc.Node.Ast.t) = Some (ntn_key_info key) | _ -> None +(* Disabled until it is more useful and doesn't pre-empt other stuff. *) let info_notation ~token:_ ~contents:_ ~point ~node : string option = - Option.bind node.Fleche.Doc.Node.ast (info_notation ~point) + if false then Option.bind node.Fleche.Doc.Node.ast (info_notation ~point) + else None open Fleche diff --git a/coq-lsp.opam b/coq-lsp.opam index 7817134e..cc5158a4 100644 --- a/coq-lsp.opam +++ b/coq-lsp.opam @@ -33,26 +33,26 @@ depends: [ "menhir" { >= "20220210" } # unit testing - "ppx_inline_test" { >= "0.14.1" } + "ppx_inline_test" { >= "v0.15.0" } # Uncomment this for releases "coq" { >= "8.18" < "8.19" } # coq deps: remove this for releases - "ocamlfind" {>= "1.8.1"} - "zarith" {>= "1.11"} + "ocamlfind" {>= "1.9.1"} + "zarith" {>= "1.13"} # result dep, fixed in main, but kept for older releases "result" { >= "1.5" } # serlib deps: see what we need to keep for release - "ppx_deriving" { >= "4.2.1" } - "ppx_deriving_yojson" { >= "3.4" } - "ppx_import" { >= "1.5-3" } - "sexplib" { >= "v0.13.0" & < "v0.18" } - "ppx_sexp_conv" { >= "v0.13.0" & < "v0.18" } - "ppx_compare" { >= "v0.13.0" & < "v0.18" } - "ppx_hash" { >= "v0.13.0" & < "v0.18" } + "ppx_deriving" { >= "5.2" } + "ppx_deriving_yojson" { >= "3.7.0" } + "ppx_import" { >= "1.11.0" } + "sexplib" { >= "v0.15.0" & < "v0.18" } + "ppx_sexp_conv" { >= "v0.15.0" & < "v0.18" } + "ppx_compare" { >= "v0.15.0" & < "v0.18" } + "ppx_hash" { >= "v0.15.0" & < "v0.18" } ] depopts: ["lwt" "logs"] diff --git a/coq/args.ml b/coq/args.ml index 0d7ddd99..d118ef13 100644 --- a/coq/args.ml +++ b/coq/args.ml @@ -24,10 +24,17 @@ let coqcorelib = & opt string (Filename.concat Coq_config.coqlib "../coq-core/") & info [ "coqcorelib" ] ~docv:"COQCORELIB" ~doc) +let findlib_config = + let doc = "Override findlib's config file" in + Arg.( + value + & opt (some string) None + & info [ "findlib_config" ] ~docv:"OCAMLFIND_CONF" ~doc) + let ocamlpath = - let doc = "Path to OCaml's lib" in + let doc = "Extra Paths to OCaml's libraries" in Arg.( - value & opt (some string) None & info [ "ocamlpath" ] ~docv:"OCAMLPATH" ~doc) + value & opt (list string) [] & info [ "ocamlpath" ] ~docv:"OCAMLPATH" ~doc) let coq_lp_conv ~implicit (unix_path, lp) = { Loadpath.coq_path = Libnames.dirpath_of_string lp diff --git a/coq/args.mli b/coq/args.mli index 0181d2e8..821148ab 100644 --- a/coq/args.mli +++ b/coq/args.mli @@ -9,7 +9,8 @@ open Cmdliner val coqlib : String.t Term.t val coqcorelib : String.t Term.t -val ocamlpath : String.t option Term.t +val findlib_config : String.t option Term.t +val ocamlpath : String.t list Term.t val rload_paths : Loadpath.vo_path List.t Term.t val qload_paths : Loadpath.vo_path List.t Term.t val debug : Bool.t Term.t diff --git a/coq/ast.ml b/coq/ast.ml index cc9c9569..52bba40d 100644 --- a/coq/ast.ml +++ b/coq/ast.ml @@ -74,12 +74,13 @@ module Meta = struct module Command = struct type t = + | AbortAll | Back of int - | ResetName of Names.lident | ResetInitial - | AbortAll - (* Not supported, but actually easy if we want | VernacRestart | VernacUndo - _ | VernacUndoTo _ *) + | ResetName of Names.lident + | Restart + (* Not supported, but actually easy if we want | VernacUndo _ | VernacUndoTo + _ *) [@@deriving hash, compare] end @@ -104,6 +105,9 @@ module Meta = struct | { expr = VernacSynPure VernacResetInitial; control; attrs } -> let command = Command.ResetInitial in Some { command; loc; attrs; control } + | { expr = VernacSynPure VernacRestart; control; attrs } -> + let command = Command.Restart in + Some { command; loc; attrs; control } | { expr = VernacSynPure (VernacBack num); control; attrs } -> let command = Command.Back num in Some { command; loc; attrs; control } @@ -309,4 +313,11 @@ let make_info ~st:_ ~lines CAst.{ loc; v } : Lang.Ast.Info.t list option = let kind = Kinds.method_ in let detail = "Instance" in Some [ Lang.Ast.Info.make ~range ~name ~kind ~detail () ] + (* | VernacSynPure (VernacSymbol slist) -> *) + (* Some (List.concat_map (symbol_info ~lines ~range) slist) *) + (* | VernacSynPure (VernacAddRewRule (name, _)) -> *) + (* let name = mk_id ~lines name in *) + (* let kind = Kinds.method_ in *) + (* let detail = "Rewrite Rule" in *) + (* Some [ Lang.Ast.Info.make ~range ~name ~kind ~detail () ] *) | _ -> None) diff --git a/coq/ast.mli b/coq/ast.mli index f2562507..d59515ab 100644 --- a/coq/ast.mli +++ b/coq/ast.mli @@ -37,10 +37,11 @@ module Meta : sig module Command : sig type t = + | AbortAll | Back of int - | ResetName of Names.lident | ResetInitial - | AbortAll + | ResetName of Names.lident + | Restart end type t = diff --git a/coq/init.ml b/coq/init.ml index 95b3e357..c14b7cb2 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 84a5bd61..1946cb78 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/loader.ml b/coq/loader.ml index 134c9fb8..6ac4ec19 100644 --- a/coq/loader.ml +++ b/coq/loader.ml @@ -48,6 +48,7 @@ let map_serlib fl_pkg = | "coq-core.plugins.funind" (* funind *) | "coq-core.plugins.ltac" (* ltac *) | "coq-core.plugins.ltac2" (* ltac2 *) + | "coq-core.plugins.ltac2_ltac1" (* ltac2_ltac1 *) | "coq-core.plugins.micromega" (* micromega *) | "coq-core.plugins.micromega_core" (* micromega_core *) | "coq-core.plugins.ring" (* ring *) diff --git a/coq/print.ml b/coq/print.ml index 01f09273..9430200a 100644 --- a/coq/print.ml +++ b/coq/print.ml @@ -4,3 +4,11 @@ let pr_letype_env ~goal_concl_style env sigma x = let pr_letype_env ~token ~goal_concl_style env sigma x = let f = pr_letype_env ~goal_concl_style env sigma in Protect.eval ~token ~f x + +let pr_goals ~token ~proof = + let proof = + State.Proof.to_coq proof |> Vernacstate.LemmaStack.get_top + |> Declare.Proof.get + in + let f = Printer.pr_open_subgoals in + Protect.eval ~token ~f proof diff --git a/coq/print.mli b/coq/print.mli index e6a4dda4..98d18d10 100644 --- a/coq/print.mli +++ b/coq/print.mli @@ -5,3 +5,6 @@ val pr_letype_env : -> Evd.evar_map -> EConstr.t -> (Pp.t, Loc.t) Protect.E.t + +val pr_goals : + token:Limits.Token.t -> proof:State.Proof.t -> (Pp.t, Loc.t) Protect.E.t diff --git a/coq/workspace.ml b/coq/workspace.ml index 27fc1373..4aa7e7dd 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -19,15 +19,27 @@ module Flags_ = Flags module Flags = struct type t = - { indices_matter : bool - ; impredicative_set : bool + { impredicative_set : bool + ; indices_matter : bool + ; type_in_type : bool + ; rewrite_rules : bool } - let default = { indices_matter = false; impredicative_set = false } + let default = + { impredicative_set = false + ; indices_matter = false + ; type_in_type = false + ; rewrite_rules = false + } - let apply { indices_matter; impredicative_set } = + let apply + { impredicative_set; indices_matter; type_in_type; rewrite_rules = _ } = + Global.set_impredicative_set impredicative_set; Global.set_indices_matter indices_matter; - Global.set_impredicative_set impredicative_set + Global.set_check_universes (not type_in_type); + () + (* V8.20-only *) + (* Global.set_rewrite_rules_allowed rewrite_rules *) end module Warning : sig @@ -59,7 +71,8 @@ end type t = { coqlib : string ; coqcorelib : string - ; ocamlpath : string option + ; findlib_config : string option + ; ocamlpath : string list ; vo_load_path : Loadpath.vo_path list ; ml_include_path : string list ; require_libs : Require.t list @@ -95,10 +108,14 @@ let rec parse_args args init boot libs f w = | [] -> (init, boot, List.rev libs, f, List.rev w) | "-rifrom" :: from :: lib :: rest -> parse_args rest init boot ((Some from, lib) :: libs) f w - | "-indices-matter" :: rest -> - parse_args rest init boot libs { f with Flags.indices_matter = true } w | "-impredicative-set" :: rest -> parse_args rest init boot libs { f with Flags.impredicative_set = true } w + | "-indices-matter" :: rest -> + parse_args rest init boot libs { f with Flags.indices_matter = true } w + | "-type-in-type" :: rest -> + parse_args rest init boot libs { f with Flags.type_in_type = true } w + | "-allow-rewrite-rules" :: rest -> + parse_args rest init boot libs { f with Flags.rewrite_rules = true } w | "-noinit" :: rest -> parse_args rest false boot libs f w | "-boot" :: rest -> parse_args rest init true libs f w | "-w" :: warn :: rest -> @@ -112,7 +129,8 @@ module CmdLine = struct type t = { coqlib : string ; coqcorelib : string - ; ocamlpath : string option + ; findlib_config : string option + ; ocamlpath : string list ; vo_load_path : Loadpath.vo_path list ; ml_include_path : string list ; args : string list @@ -127,6 +145,7 @@ let mk_require_from (from, library) = let make ~cmdline ~implicit ~kind ~debug = let { CmdLine.coqcorelib ; coqlib + ; findlib_config ; ocamlpath ; args ; ml_include_path @@ -165,6 +184,7 @@ let make ~cmdline ~implicit ~kind ~debug = let ml_include_path = dft_ml_include_path @ ml_include_path in { coqlib ; coqcorelib + ; findlib_config ; ocamlpath ; vo_load_path ; ml_include_path @@ -183,12 +203,8 @@ let pp_load_path fmt (* This is a bit messy upstream, as -I both extends Coq loadpath and OCAMLPATH loadpath *) -let findlib_init ~ml_include_path ~ocamlpath = - let config, ocamlpath = - match ocamlpath with - | None -> (None, []) - | Some dir -> (Some (Filename.concat dir "findlib.conf"), [ dir ]) - in +let findlib_init ~ml_include_path ?findlib_config ~ocamlpath () = + let config = findlib_config in let env_ocamlpath = try [ Sys.getenv "OCAMLPATH" ] with Not_found -> [] in let env_ocamlpath = ml_include_path @ env_ocamlpath @ ocamlpath in let ocamlpathsep = if Sys.unix then ":" else ";" in @@ -198,6 +214,7 @@ let findlib_init ~ml_include_path ~ocamlpath = let describe { coqlib ; coqcorelib + ; findlib_config ; ocamlpath ; kind ; vo_load_path @@ -213,14 +230,10 @@ let describe in let n_vo = List.length vo_load_path in let n_ml = List.length ml_include_path in - let ocamlpath_msg = - Option.cata - (fun op -> "was overrident to " ^ op) - "wasn't overriden" ocamlpath - in + let ocamlpath_msg = "added paths: [" ^ String.concat "|" ocamlpath ^ "]" in (* We need to do this in order for the calls to Findlib to make sense, but really need to modify this *) - findlib_init ~ml_include_path ~ocamlpath; + findlib_init ~ml_include_path ?findlib_config ~ocamlpath (); let fl_packages = Findlib.list_packages' () in let fl_config = Findlib.config_file () in let fl_location = Findlib.default_location () in @@ -298,6 +311,7 @@ let dirpath_of_uri ~uri = let apply ~intern ~uri { coqlib = _ ; coqcorelib = _ + ; findlib_config ; ocamlpath ; vo_load_path ; ml_include_path @@ -311,7 +325,7 @@ let apply ~intern ~uri Flags.apply flags; Warning.apply warnings; List.iter Mltop.add_ml_dir ml_include_path; - findlib_init ~ml_include_path ~ocamlpath; + findlib_init ~ml_include_path ?findlib_config ~ocamlpath (); List.iter Loadpath.add_vo_path vo_load_path; Declaremods.start_library (dirpath_of_uri ~uri); load_objs ~intern require_libs diff --git a/coq/workspace.mli b/coq/workspace.mli index a5ed7c2e..2a46e7cf 100644 --- a/coq/workspace.mli +++ b/coq/workspace.mli @@ -17,8 +17,10 @@ module Flags : sig type t = private - { indices_matter : bool - ; impredicative_set : bool + { impredicative_set : bool + ; indices_matter : bool + ; type_in_type : bool + ; rewrite_rules : bool } end @@ -40,10 +42,14 @@ module Require : sig } end +(* Generated from a _CoqProject, dune (in the future) or command line args *) type t = private { coqlib : string ; coqcorelib : string - ; ocamlpath : string option + ; findlib_config : + string option (* Path to findlib config file, if [None], default *) + ; ocamlpath : + string list (* extra ocamlpath paths, for example for local plugins *) ; vo_load_path : Loadpath.vo_path list (** List of -R / -Q flags passed to Coq, usually theories we depend on *) ; ml_include_path : string list @@ -75,7 +81,8 @@ module CmdLine : sig type t = { coqlib : string ; coqcorelib : string - ; ocamlpath : string option + ; findlib_config : string option + ; ocamlpath : string list ; vo_load_path : Loadpath.vo_path list ; ml_include_path : string list ; args : string list diff --git a/dune b/dune index 966a3aa4..243438e7 100644 --- a/dune +++ b/dune @@ -1,3 +1,3 @@ -(dirs :standard \ serlib serlib_8_19) +(dirs :standard \ serlib serlib_8_20 serlib_8_19) (vendored_dirs vendor) 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/editor/code/src/goals.ts b/editor/code/src/goals.ts index 87aec4db..bb6cd544 100644 --- a/editor/code/src/goals.ts +++ b/editor/code/src/goals.ts @@ -1,12 +1,4 @@ -import { - Uri, - WebviewPanel, - window, - ViewColumn, - extensions, - commands, - TextDocument, -} from "vscode"; +import { Uri, WebviewPanel, window, ViewColumn } from "vscode"; import { BaseLanguageClient, RequestType, 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 + 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/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index e802371d..a9d3322b 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -15,66 +15,142 @@ See also the upstream LSP issue on generic support for Proof Assistants https://github.com/microsoft/language-server-protocol/issues/1414 +### coq-lsp basic operating model + +`coq-lsp` is a bit different from other servers in that checking the +file is often very expensive, so the continuous LSP model can be too +heavy. The philosophy of `coq-lsp` is to treat a Coq document as a +build task, and then check the document under user-request. + +Thus, for example when the user requests goals at a given point, +`coq-lsp` will check if the goals are known, otherwise try to check +the required document parts to return answers to the user ASAP. + +`coq-lsp` has three main functioning modes (controlled by a regular +parameter): + +- _continuous mode_: in this mode, `coq-lsp` will try to complete + checking of all open files when idle. This mode has shown to be very + useful in many contexts, for example educational, as it provides + very low latency. + +- _on-demand mode_: in this mode, `coq-lsp` will do nothing when + idle. This mode for example can be used to simulate the traditional + "step-based" Coq interaction mode, just have your client request + goals as the desired step position, `coq-lsp` will execute the + document up to that point. + +- _on-demand mode, with viewport hints_: in this mode, inspired by + Isabelle, the `coq-lsp` client will inform the server about the + user's viewport. This mode provides a comfortable compromise between + latency and CPU usage. + +Note that on-demand mode often implies that some requests that require +the full document to be checked, like `documentSymbols`, will return +less complete information. + +Also note that it has been hard for us to design an interaction mode +that would fit well all client editors; for example VSCode doesn't +implement progress on some requests that would be very useful for us. + +However, the underlying checking engine (`Flèche`) is very flexible, +so don't hesitate to contact with us if your client would want things +in a different way. + +### coq-lsp workspace configuration + +See the manual for the exact details, but indeed, coq-lsp will try to +auto-configure Coq projects looking for `_CoqProject` files in the LSP +workspace folders sent by the client. + +### A minimal client implementation: + +In order to implement a minimal, but working `coq-lsp` client, you need to: + +- setup a regular LSP client on your side, +- setup the right parameters for `initializationOptions` on `initialize`, +- implement the `coq/goals` request + +And that should be it! We recommend next supporting the +`coq/serverStatus` notification, and maybe `coq/viewport` too. + ## Language server protocol support table If a feature doesn't appear here it usually means it is not planned in the short term: -| Method | Support | Notes | -|---------------------------------------|---------|---------------------------------------------------------------| -| `initialize` | Partial | We don't obey the advertised client capabilities | -| `client/registerCapability` | No | Not planned ATM | -| `$/setTrace` | Yes | | -| `$/logTrace` | Yes | | -| `window/logMessage` | Yes | | -|---------------------------------------|---------|---------------------------------------------------------------| -| `textDocument/didOpen` | Yes | We can't reuse Memo tables yet | -| `textDocument/didChange` | Yes | We only support `TextDocumentSyncKind.Full` for now | -| `textDocument/didClose` | Partial | We'd likely want to save a `.vo` file on close if possible | -| `textDocument/didSave` | Partial | Undergoing behavior refinement | -|---------------------------------------|---------|---------------------------------------------------------------| -| `notebookDocument/didOpen` | No | Planned | -|---------------------------------------|---------|---------------------------------------------------------------| -| `textDocument/declaration` | No | Planned, blocked on upstream issues | -| `textDocument/definition` | Yes (*) | Uses .glob information which is often incomplete | -| `textDocument/references` | No | Planned, blocked on upstream issues | -| `textDocument/hover` | Yes | Shows stats and type info of identifiers at point, extensible | -| `textDocument/codeLens` | No | | -| `textDocument/foldingRange` | No | | -| `textDocument/documentSymbol` | Yes | Sections and modules missing (#322) | -| `textDocument/semanticTokens` | No | Planned | -| `textDocument/inlineValue` | No | Planned | -| `textDocument/inlayHint` | No | Planned | -| `textDocument/completion` | Partial | Needs more work locally and upstream (#50) | -| `textDocument/publishDiagnostics` | Yes | | -| `textDocument/diagnostic` | No | Planned, issue #49 | -| `textDocument/codeAction` | No | Planned | -| `textDocument/selectionRange` | Partial | Selection for a point is its span; no parents | -|---------------------------------------|---------|---------------------------------------------------------------| -| `workspace/workspaceFolders` | Yes | Each folder should have a `_CoqProject` file at the root. | -| `workspace/didChangeWorkspaceFolders` | Yes | | -| `workspace/didChangeConfiguration` | Yes (*) | We still do a client -> server push, instead of pull | -|---------------------------------------|---------|---------------------------------------------------------------| +| Method | Support | Notes | +|---------------------------------------|---------|--------------------------------------------------------------------------| +| `initialize` | Partial | We don't obey the advertised client capabilities | +| `client/registerCapability` | No | Not planned ATM | +| `$/setTrace` | Yes | | +| `$/logTrace` | Yes | | +| `window/logMessage` | Yes | | +|---------------------------------------|---------|--------------------------------------------------------------------------| +| `textDocument/didOpen` | Yes | We can't reuse Memo tables yet | +| `textDocument/didChange` | Yes | We only support `TextDocumentSyncKind.Full` for now | +| `textDocument/didClose` | Partial | We'd likely want to save a `.vo` file on close if possible | +| `textDocument/didSave` | Partial | Undergoing behavior refinement | +|---------------------------------------|---------|--------------------------------------------------------------------------| +| `notebookDocument/didOpen` | No | Planned | +|---------------------------------------|---------|--------------------------------------------------------------------------| +| `textDocument/declaration` | No | Planned, blocked on upstream issues | +| `textDocument/definition` | Yes (*) | Uses .glob information which is often incomplete | +| `textDocument/references` | No | Planned, blocked on upstream issues | +| `textDocument/hover` | Yes | Shows stats, type info, and location of identifiers at point, extensible | +| `textDocument/codeLens` | No | | +| `textDocument/foldingRange` | No | | +| `textDocument/documentSymbol` | Yes | Sections and modules missing (#322) | +| `textDocument/semanticTokens` | No | Planned | +| `textDocument/inlineValue` | No | Planned | +| `textDocument/inlayHint` | No | Planned | +| `textDocument/completion` | Partial | Needs more work locally and upstream (#50) | +| `textDocument/publishDiagnostics` | Yes | | +| `textDocument/diagnostic` | No | Planned, issue #49 | +| `textDocument/codeAction` | No | Planned | +| `textDocument/selectionRange` | Partial | Selection for a point is its span; no parents | +|---------------------------------------|---------|--------------------------------------------------------------------------| +| `workspace/diagnostic` | No | Planned | +| `workspace/workspaceFolders` | Yes | Each folder should have a `_CoqProject` file at the root. | +| `workspace/didChangeWorkspaceFolders` | Yes | | +| `workspace/didChangeConfiguration` | Yes (*) | We still do a client -> server push, instead of pull | +|---------------------------------------|---------|--------------------------------------------------------------------------| ### URIs accepted by coq-lsp -`coq-lsp` only accepts `file:///` URIs; moreover, the URIs sent to the -server must be able to be mapped back to a Coq library name, so a -fully-checked file can be saved to a `.vo` for example. +The `coq-lsp` server only accepts `file:///` URIs; moreover, the URIs +sent to the server must be able to be mapped back to a Coq library +name, so a fully-checked file can be saved to a `.vo` for example. Don't hesitate to open an issue if you need support for different kind -of URIs in your application / client. +of URIs in your application / client. The client does support +`vsls:///` URIs. Additionally, `coq-lsp` will use the extension of the file in the URI to determine the content type. Supported extensions are: - `.v`: File will be interpreted as a regular Coq vernacular file, -- `.mv`: File will be interpreted as a markdown file, and code +- `.mv`: File will be interpreted as a markdown file. Code snippets between `coq` markdown code blocks will be interpreted as Coq code. +- `.v.tex` or `.lv`: File will be interpreted as a LaTeX file. Code + snippets between `\begin{coq}/\end{coq}` LaTeX environments will be + interpreted as Coq code. ## Extensions to the LSP specification -As of today, `coq-lsp` implements two extensions to the LSP spec. Note -that none of them are stable yet: +As of today, `coq-lsp` implements several extensions to the LSP +spec. Note that none of them are stable yet. + +- [Extra diagnostics data](#extra-diagnostics-data) +- [Goal display](#goal-display) +- [File checking progress](#file-checking-progress) +- [Document Ast](#document-ast-request) +- [.vo file saving](#vo-file-saving) +- [Performance data notification](#performance-data-notification) +- [Trim cache notification](#trim-cache-notification) +- [Viewport notification](#viewport-notification) +- [Server configuration parameters](#did-change-configuration-and-server-configuration-parameters) +- [Server version notification](#server-version-notification) +- [Server status notification](#server-status-notification) ### Extra diagnostics data diff --git a/examples/ItHolds.v b/examples/ItHolds.v new file mode 100644 index 00000000..e9c32a78 --- /dev/null +++ b/examples/ItHolds.v @@ -0,0 +1,233 @@ +(******************************************************************************) +(* This file is part of Waterproof-lib. *) +(* *) +(* Waterproof-lib is free software: you can redistribute it and/or modify *) +(* it under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 3 of the License, or *) +(* (at your option) any later version. *) +(* *) +(* Waterproof-lib is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU General Public License for more details. *) +(* *) +(* You should have received a copy of the GNU General Public License *) +(* along with Waterproof-lib. If not, see . *) +(* *) +(******************************************************************************) + +Require Import Ltac2.Ltac2. +Require Import Ltac2.Message. +Local Ltac2 concat_list (ls : message list) : message := + List.fold_right concat ls (of_string ""). + +(** Tries to make the assertion [True] with label [label]. + Throws an error if this fails, i.e. if the label is already used + for another one of the hypotheses. + + This check was separated out from the 'assert'-tactics below because the + '[label] is already used error' would otherwise be caught in + the code meant to catch [AutomationFailure] errors. *) + +Local Ltac2 try_out_label (label : ident) := + match Control.case (fun () => + assert True as $label by exact I) + with + | Err exn => Control.zero exn + | Val _ => clear $label + end. + +(* For making tests independent of WaterProof *) +Ltac2 warn : message -> unit := fun _ => (). +Ltac2 throw : message -> unit := fun _ => (). +Ltac2 waterprove (_depth: int) (_shield: bool) (_db_type: 'a) := (). +Ltac2 rwaterprove (_depth: int) (_shield: bool) (_db_type: 'a) (_ : constr) := (). +Ltac2 suggest_how_to_use (_x : constr) (_label : ident option) := (). +Ltac2 Type exn ::= [ FailedToProve(constr) ]. +Ltac2 correct_type_by_wrapping (t: constr): constr := t. +Ltac2 wrapper_core_by_tactic (_by_tactic : constr -> unit) (_xtr_lemma : constr) := (). +Ltac2 panic_if_goal_wrapped () := (). +Ltac2 since_framework (_by_tactic : constr -> unit) (_claimed_cause : constr) := (). + +(** Attempts to assert that [claim] holds, if succesful [claim] is added to the local + hypotheses. If [label] is specified [claim] is given [label] as its identifier, otherwise an + identifier starting with '_H' is generated. + + Additionally, if argument [postpone] is [true], actually proving the claim is postponed. + The claim is asserted and the proof is shelved using an evar. + *) +Local Ltac2 wp_assert (claim : constr) (label : ident option) (postpone : bool):= + let err_msg (g : constr) := concat_list + [of_string "Could not verify that "; of_constr g; of_string "."] in + let id := + match label with + | None => Fresh.in_goal @_H + | Some label => try_out_label label; label + end + in + let claim := claim in + if postpone + then + (* Assert claim and proof using shelved evar *) + (* (using 'admit' would have shown a confusing warning message) *) + assert $claim as $id; + Control.focus 1 1 (fun () => + let evar_id := Fresh.in_goal @_Hpostpone in + ltac1:(id claim |- evar (id : claim)) (Ltac1.of_ident evar_id) (Ltac1.of_constr claim); + let evar := Control.hyp evar_id in + exact $evar + ); + warn (concat_list [of_string "Please come back later to provide an actual proof of "; + of_constr claim; of_string "."]) + + else + (* Assert claim and attempt to prove automatically *) + match Control.case (fun () => + assert $claim as $id by + (waterprove 5 true 99)) + with + | Val _ => () + | Err (FailedToProve g) => throw (err_msg g) + | Err exn => Control.zero exn + end; + (* Print suggestion on how to use new statement. *) + suggest_how_to_use claim label. + +(** Attempts to assert that [claim] holds, if succesful [claim] is added to the local + hypotheses. If [label] is specified [claim] is given [label] as its identifier, otherwise an + identifier starting with '_H' is generated. + [xtr_lemma] has to be used in the proof that [claim] holds. + *) +Local Ltac2 core_wp_assert_by (claim : constr) (label : ident option) (xtr_lemma : constr) := + let err_msg (g : constr) := concat_list + [of_string "Could not verify that "; of_constr g; of_string "."] in + let id := + match label with + | None => Fresh.in_goal @_H + | Some label => try_out_label label; label + end + in + let claim := correct_type_by_wrapping claim in + match Control.case (fun () => + assert $claim as $id by + (rwaterprove 5 true 19 xtr_lemma)) + with + | Val _ => () + | Err (FailedToProve g) => throw (err_msg g) + | Err exn => Control.zero exn (* includes FailedToUse error *) + end. + +(** Adaptation of [core_wp_assert_by] that turns the [FailedToUse] errors + which might be thrown into user readable errors. *) +Local Ltac2 wp_assert_by (claim : constr) (label : ident option) (xtr_lemma : constr) := + wrapper_core_by_tactic (core_wp_assert_by claim label) xtr_lemma; + (* Print suggestion on how to use new statement. *) + suggest_how_to_use claim label. + +(** Adaptation of [core_wp_assert_by] that allows user to use mathematical statements themselves + instead of references to them as extra information for the automation system. + Uses the code in [Since.v]. *) +Local Ltac2 wp_assert_since (claim : constr) (label : ident option) (xtr_claim : constr) := + since_framework (core_wp_assert_by claim label) xtr_claim; + (* Print suggestion on how to use new statement. *) + suggest_how_to_use claim label. + + +(** + Attempts to assert a claim and proves it automatically using a specified lemma, + this lemma has to be used. + + Arguments: + - [xtr_lemma: constr], reference to a lemma used to prove the claim (via [rwaterprove]). + - [label: ident option], optional name for the claim. + If the proof succeeds, it will become a hypothesis (bearing [label] as name). + - [claim: constr], the actual content of the claim to prove. + + Raises exception: + - (fatal) if [rwaterprove] fails to prove the claim using the specified lemma. + - [[label] is already used], if there is already another hypothesis with identifier [label]. +*) +Ltac2 Notation "By" xtr_lemma(constr) "it" "holds" "that" claim(constr) label(opt(seq("(", ident, ")"))) := + panic_if_goal_wrapped (); + wp_assert_by claim label xtr_lemma. + +Ltac2 Notation "Since" xtr_claim(constr) "it" "holds" "that" claim(constr) label(opt(seq("(", ident, ")"))) := + panic_if_goal_wrapped (); + wp_assert_since claim label xtr_claim. + + +(** * It holds that ... (...) + Attempts to assert a claim and proves it automatically. + Removes [StateHyp.Wrapper] wrapper from the goal (proving claim by automation not necessary). + + Arguments: + - [label: ident option], optional name for the claim. + If the proof succeeds, it will become a hypothesis (bearing [label] as name). + - [claim: constr], the actual content of the claim to prove. + + Raises exception: + - (fatal) if [rwaterprove] fails to prove the claim using the specified lemma. + - [[label] is already used], if there is already another hypothesis with identifier [label]. + - (fatal) If goal is wrapped in [StateHyp.Wrapper] and the wrong statement is specified. +*) +Inductive Wrapper (A : Type) (h : A) (G : Type) : Type := + | wrap : G -> Wrapper A h G. +Ltac2 check_constr_equal (_a: constr) (_b: constr) := false. + +Local Ltac2 wp_assert_with_unwrap (claim : constr) (label : ident option) := + (* Try out label first. + Code results in wrong error if done inside repeated match.. *) + match label with | None => () | Some label => try_out_label label end; + + match! goal with + | [h : ?s |- Wrapper ?s ?h_spec _] => + let h_constr := Control.hyp h in + (* sanity check "h = h_spec" *) + if check_constr_equal h_constr h_spec + then () + else fail; + let w := match label with + | None => Fresh.fresh (Fresh.Free.of_goal ()) @_H + | Some label => label + end in + if check_constr_equal s claim + then + match Control.case (fun () => assert $claim as $w by exact $h_constr) with + | Val _ => (* If claims are definitionally equal, go with the + version that is supplied as argument to "It holds that ..." *) + apply (wrap $s); + Std.clear [h] + | Err exn => print (of_string "Exception occurred"); print (of_exn exn) + end + else throw (of_string "Wrong statement specified.") + (* rename ident generated in specialize with user-specified label*) + (* match label with + | None => () + | Some label => Std.rename [(w, label)] + end *) + | [|- _] => + panic_if_goal_wrapped (); + wp_assert claim label false + end. + +Ltac2 Notation "It" "holds" "that" claim(constr) label(opt(seq("(", ident, ")"))) := + wp_assert_with_unwrap claim label. + + +(** * By magic it holds that ... (...) + Asserts a claim and proves it using a shelved evar. + + Arguments: + - [label: ident option], optional name for the claim. + - [claim: constr], the actual content of the claim to prove. + + Raises exception: + - [[label] is already used], if there is already another hypothesis with identifier [label]. + + Raises warning: + - [Please come back later to provide an actual proof of [claim].], always. +*) + +Ltac2 Notation "By" "magic" "it" "holds" "that" claim(constr) label(opt(seq("(", ident, ")"))) := + panic_if_goal_wrapped (); + wp_assert claim label true. \ No newline at end of file diff --git a/examples/MetaCommands.v b/examples/MetaCommands.v index a352ed8c..d56da43f 100644 --- a/examples/MetaCommands.v +++ b/examples/MetaCommands.v @@ -42,5 +42,12 @@ Lemma foo : True. now auto. Qed. Print foo. +(* testing restart *) +Goal nat -> nat. +intro x. +Restart. +intros x. exact x. +Qed. + diff --git a/examples/documentSymbol.v b/examples/documentSymbol.v index 06cf6e4f..78044a02 100644 --- a/examples/documentSymbol.v +++ b/examples/documentSymbol.v @@ -8,7 +8,7 @@ Inductive foo := A | B : a -> foo. Inductive eh1 := Ah1 : eh2 -> eh1 with eh2 := Bh1 : eh1 -> eh2. -Variable (j : nat). +Axiom (j : nat). Axiom test : False. @@ -34,7 +34,7 @@ End Moo. Module Bar. - Variable (u : nat). + Parameter (u : nat). Parameter (v : nat). @@ -42,4 +42,4 @@ Module Bar. Theorem not : False. Qed. -End Bar. \ No newline at end of file +End Bar. diff --git a/examples/print_univs.v b/examples/print_univs.v new file mode 100644 index 00000000..f6a24025 --- /dev/null +++ b/examples/print_univs.v @@ -0,0 +1,14 @@ +From Coq Require Import Prelude. +Set Printing Universes. +Set Universe Polymorphism. + +Definition arr (S: Type) : Type := S. + +Print arr. + +Inductive foo (M : Type) : Type -> Type := + bar : M -> Type -> foo M nat. + +Print foo. + +About foo. diff --git a/examples/rewrite/_CoqProject b/examples/rewrite/_CoqProject new file mode 100644 index 00000000..bc0bb094 --- /dev/null +++ b/examples/rewrite/_CoqProject @@ -0,0 +1,3 @@ +-arg -allow-rewrite-rules + +simple.v diff --git a/examples/rewrite/alis.v b/examples/rewrite/alis.v new file mode 100644 index 00000000..1398856f --- /dev/null +++ b/examples/rewrite/alis.v @@ -0,0 +1,53 @@ +From Coq Require Import Prelude. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Symbol Interval : Set. +Symbol i0 : Interval. +Symbol i1 : Interval. +Symbol seg : i0 = i1. + +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y + := match p with idpath _ => u end. + + +Unset Universe Polymorphism. +Symbol ap@{u v} : forall {A : Type@{u}}{B : Type@{v}} (f : A -> B) {x y : A} + (p : x = y), f x = f y. +Rewrite Rule ap_comp := +| @ap ?A ?P ?f _ _ (@idpath@{u} _ ?a) => @idpath ?P (?f ?a). +Symbol apD@{u v} : forall {A : Type@{u}} {P : A -> Type@{v}} + (f : forall x, P x) {x y : A} (p : x = y), transport P p (f x) = f y. +Rewrite Rule apD_comp := +| @apD ?A ?P ?f _ _ (@idpath _ ?a) => @idpath (?P ?a) (?f ?a). +Set Universe Polymorphism. + +Symbol Interval_ind + : forall (P : Interval -> Type) + (a : P i0) (b : P i1) (p : transport P seg a = b), + forall x, P x. + +Symbol Interval_rec : forall (P : Type) (a b : P) (p : a = b), Interval -> P. + +Rewrite Rule interval_rewrite := +| Interval_ind ?P ?a ?b ?p i0 => ?a +| Interval_ind ?P ?a ?b ?p i1 => ?b +| apD (Interval_ind ?P ?a ?b ?p) seg => ?p +| ap (Interval_rec ?P ?a ?b ?p) seg => ?p +. + +Definition funext {A : Type} {P : A -> Type} {f g : forall x, P x} + : (forall x, f x = g x) -> f = g. +Proof. + intros p. + simple refine (let r := _ in _). + 1: exact (Interval -> forall x, P x). + { intros i x; revert i. + exact (Interval_rec _ (f x) (g x) (p x)). } + (* Coq can't rewrite under eta :'( *) + Fail exact (ap r seg). +Abort. diff --git a/examples/rewrite/simple.v b/examples/rewrite/simple.v new file mode 100644 index 00000000..b22831cb --- /dev/null +++ b/examples/rewrite/simple.v @@ -0,0 +1,25 @@ +(* test for *) + +Symbols + (pplus : nat -> nat -> nat) + (pmul : nat -> nat -> nat). + +Notation "a ++ b" := (pplus a b). +Notation "a ** b" := (pmul a b) (at level 50). + +Rewrite Rules pplus_rewrite := +| ?n ++ 0 => ?n +| ?n ++ S ?m => S (?n ++ ?m) +| 0 ++ ?n => ?n +| S ?n ++ ?m => S (?n ++ ?m) +| ?n ++ (?m ++ ?o) => (?n ++ ?m) ++ ?o. + +Rewrite Rules pmul_rewrite := +| 0 ** ?n => 0 +| ?n ** 0 => 0 +| S ?n ** ?m => ?n ++ (?n ** ?m) +| ?n ** S ?m => ?m ++ (?n ** ?m) +| ?n ** (?m ** ?o) => (?n ** ?m) ** ?o. + +Lemma foo n m : S n ** m ++ 0 = n ++ n ** m. +Proof. now reflexivity. Qed. diff --git a/flake.lock b/flake.lock index 4d6681c3..54efa01d 100644 --- a/flake.lock +++ b/flake.lock @@ -21,11 +21,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1712014858, - "narHash": "sha256-sB4SWl2lX95bExY2gMFG5HIzvva5AVMJd4Igm+GpZNw=", + "lastModified": 1725024810, + "narHash": "sha256-ODYRm8zHfLTH3soTFWE452ydPYz2iTvr9T8ftDMUQ3E=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "9126214d0a59633752a136528f5f3b9aa8565b7d", + "rev": "af510d4a62d071ea13925ce41c95e3dec816c01d", "type": "github" }, "original": { @@ -57,11 +57,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1703102458, - "narHash": "sha256-3pOV731qi34Q2G8e2SqjUXqnftuFrbcq+NdagEZXISo=", + "lastModified": 1717929455, + "narHash": "sha256-BiI5xWygriOJuNISnGAeL0KYxrEMnjgpg+7wDskVBhI=", "owner": "nix-community", "repo": "napalm", - "rev": "edcb26c266ca37c9521f6a97f33234633cbec186", + "rev": "e1babff744cd278b56abe8478008b4a9e23036cf", "type": "github" }, "original": { @@ -88,29 +88,23 @@ }, "nixpkgs-lib": { "locked": { - "dir": "lib", - "lastModified": 1711703276, - "narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "d8fe5e6c92d0d190646fb9f1056741a229980089", - "type": "github" + "lastModified": 1722555339, + "narHash": "sha256-uFf2QeW7eAHlYXuDktm9c25OxOyCoUOQmh5SZ9amE5Q=", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/a5d394176e64ab29c852d03346c1fc9b0b7d33eb.tar.gz" }, "original": { - "dir": "lib", - "owner": "NixOS", - "ref": "nixos-unstable", - "repo": "nixpkgs", - "type": "github" + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/a5d394176e64ab29c852d03346c1fc9b0b7d33eb.tar.gz" } }, "nixpkgs_2": { "locked": { - "lastModified": 1714058985, - "narHash": "sha256-gD/Ya/oXic+vbQGvmqxm8qaWmOx3HnrKHQtSL6oRW0E=", + "lastModified": 1724999960, + "narHash": "sha256-LB3jqSGW5u1ZcUcX6vO/qBOq5oXHlmOCxsTXGMEitp4=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "bf182c39d9439811484aad0d241ea89619b44bc7", + "rev": "b96f849e725333eb2b1c7f1cb84ff102062468ba", "type": "github" }, "original": { @@ -122,11 +116,11 @@ }, "nixpkgs_3": { "locked": { - "lastModified": 1708475490, - "narHash": "sha256-g1v0TsWBQPX97ziznfJdWhgMyMGtoBFs102xSYO4syU=", + "lastModified": 1723637854, + "narHash": "sha256-med8+5DSWa2UnOqtdICndjDAEjxr5D7zaIiK4pn0Q7c=", "owner": "nixos", "repo": "nixpkgs", - "rev": "0e74ca98a74bc7270d28838369593635a5db3260", + "rev": "c3aa7b8938b17aebd2deecf7be0636000d62a2b9", "type": "github" }, "original": { @@ -165,11 +159,11 @@ "nixpkgs": "nixpkgs_3" }, "locked": { - "lastModified": 1714058656, - "narHash": "sha256-Qv4RBm4LKuO4fNOfx9wl40W2rBbv5u5m+whxRYUMiaA=", + "lastModified": 1724833132, + "narHash": "sha256-F4djBvyNRAXGusJiNYInqR6zIMI3rvlp6WiKwsRISos=", "owner": "numtide", "repo": "treefmt-nix", - "rev": "c6aaf729f34a36c445618580a9f95a48f5e4e03f", + "rev": "3ffd842a5f50f435d3e603312eefa4790db46af5", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 6783a2d6..5e130af7 100644 --- a/flake.nix +++ b/flake.nix @@ -30,18 +30,17 @@ ... }: let l = lib // builtins; - coqpkg = pkgs.coqPackages_8_18; + coqpkg = pkgs.coqPackages_8_20; coqPackages = coqpkg.coqPackages; ocamlPackages = coqpkg.coq.ocamlPackages; in { packages.default = config.packages.coq-lsp; - # NOTE(2023-06-02): Nix does not support top-level self submodules (yet) packages.coq-lsp = ocamlPackages.buildDunePackage { duneVersion = "3"; pname = "coq-lsp"; - version = "${self.lastModifiedDate}+8.18-rc1"; + version = "${self.lastModifiedDate}+8.20-rc1"; src = self.outPath; @@ -76,7 +75,7 @@ flakeFormatter = true; - settings.global.excludes = ["./vendor/**"]; + settings.global.excludes = ["./vendor/**" "controller-js/js_stub/**"]; programs.alejandra.enable = true; programs.ocamlformat = { diff --git a/fleche/doc.ml b/fleche/doc.ml index 76d9c836..7a26f434 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -318,15 +318,17 @@ let init_fname ~uri = let init_loc ~uri = Loc.initial (init_fname ~uri) (* default range for the node that contains the init feedback errors *) -let drange = +let drange ~lines = let open Lang in + let llen = if Array.length lines > 0 then String.length lines.(0) else 1 in let start = Point.{ line = 0; character = 0; offset = 0 } in - let end_ = Point.{ line = 0; character = 1; offset = 1 } in + let end_ = Point.{ line = 0; character = llen; offset = llen } in Range.{ start; end_ } let process_init_feedback ~lines ~stats ~global_stats state feedback = let messages = List.map (Node.Message.feedback_to_message ~lines) feedback in if not (CList.is_empty messages) then + let drange = drange ~lines in let diags, messages = Diags.of_messages ~drange messages in let parsing_time = 0.0 in let info = Node.Info.make ~parsing_time ?stats ~global_stats () in @@ -552,6 +554,13 @@ end (* This is not in its own module because we don't want to move the definition of [Node.t] out (yet) *) module Recovery : sig + (** [find_proof_start nodes] returns [Some (node, pnode)] where [node] is the + node that contains the start of the proof, and [pnode] is the previous + node, if exists. [nodes] is the list of document nodes, in _reverse + order_. *) + val find_proof_start : Node.t list -> (Node.t * Node.t option) option + (* This is useful in meta-commands, and other plugins actually! *) + val handle : token:Coq.Limits.Token.t -> context:Recovery_context.t @@ -672,6 +681,11 @@ let search_node ~command ~doc ~st = in (Coq.Protect.E.error message, nstats None) | Some node -> (Coq.Protect.E.ok node.state, nstats (Some node))) + | Restart -> ( + match Recovery.find_proof_start doc.nodes with + | None -> + (Coq.Protect.E.error Pp.(str "no proof to restart"), Memo.Stats.zero) + | Some (node, _) -> (Coq.Protect.E.ok node.state, nstats None)) | ResetName id -> ( let toc = doc.toc in let id = Names.Id.to_string id.v in diff --git a/fleche/theory.ml b/fleche/theory.ml index d4234974..9c4f710a 100644 --- a/fleche/theory.ml +++ b/fleche/theory.ml @@ -341,6 +341,7 @@ let close ~uri = module Request = struct type request = + | Immediate | FullDoc | PosInDoc of { point : int * int @@ -379,6 +380,7 @@ module Request = struct let default () = Cancel in (* should be Cancelled? *) match request with + | Immediate -> Handle.with_doc ~kind ~default ~uri ~f:(fun _ doc -> Now doc) | FullDoc -> Handle.with_doc ~kind ~default ~uri ~f:(fun _ doc -> match (Doc.Completion.is_completed doc.completed, postpone) with @@ -402,6 +404,7 @@ module Request = struct (** Removes the request from the list of things to wake up *) let remove { id; uri; postpone = _; request } = match request with + | Immediate -> () | FullDoc -> Handle.remove_cp_request ~uri ~id | PosInDoc { point; _ } -> Handle.remove_pt_request ~uri ~id ~point end diff --git a/fleche/theory.mli b/fleche/theory.mli index e20c2cf7..1703875f 100644 --- a/fleche/theory.mli +++ b/fleche/theory.mli @@ -49,6 +49,7 @@ val close : uri:Lang.LUri.File.t -> unit module Request : sig type request = + | Immediate | FullDoc | PosInDoc of { point : int * int diff --git a/lsp/jLang.ml b/lsp/jLang.ml index 7df98eb9..e5490703 100644 --- a/lsp/jLang.ml +++ b/lsp/jLang.ml @@ -88,3 +88,26 @@ module Diagnostic = struct let message = Pp.to_string message in _t_to_yojson { range; severity; message; data } end + +module Stdlib = JStdlib + +module With_range = struct + type 'a t = [%import: ('a Lang.With_range.t[@with Lang.Range.t := Range.t])] + [@@deriving yojson] +end + +module Ast = struct + module Name = struct + type t = [%import: Lang.Ast.Name.t] [@@deriving yojson] + end + + module Info = struct + type t = + [%import: + (Lang.Ast.Info.t + [@with + Lang.Range.t := Range.t; + Lang.With_range.t := With_range.t])] + [@@deriving yojson] + end +end diff --git a/lsp/jLang.mli b/lsp/jLang.mli index 3aba7f17..2b59f7b8 100644 --- a/lsp/jLang.mli +++ b/lsp/jLang.mli @@ -38,3 +38,9 @@ module Diagnostic : sig [@@deriving yojson] end end + +module Ast : sig + module Info : sig + type t = Lang.Ast.Info.t [@@deriving yojson] + end +end diff --git a/lsp/jStdlib.ml b/lsp/jStdlib.ml new file mode 100644 index 00000000..5995cbaf --- /dev/null +++ b/lsp/jStdlib.ml @@ -0,0 +1,5 @@ +module Result = struct + include Stdlib.Result + + type ('a, 'e) t = [%import: ('a, 'e) Stdlib.Result.t] [@@deriving yojson] +end diff --git a/petanque/README.md b/petanque/README.md index cdb47056..e3f40fd0 100644 --- a/petanque/README.md +++ b/petanque/README.md @@ -14,6 +14,7 @@ an OCaml API (`agent.mli`) which is then exposed via some form of RPC. - Guilaume Baudart (Inria) - Emilio J. Gallego Arias (Inria) +- Marc Lelarge (Inria) - Laetitia Teodorescu (Inria) ## Acknowledgments diff --git a/petanque/json/jAgent.ml b/petanque/json/jAgent.ml index dac37aa8..58c39789 100644 --- a/petanque/json/jAgent.ml +++ b/petanque/json/jAgent.ml @@ -8,22 +8,6 @@ module Inspect = struct end (* The typical protocol dance *) - -(* What a mess result stuff is, we need this in case result is installed, as - then the types below will be referenced as plain result ... *) -module Stdlib = struct - module Result = struct - include Stdlib.Result - - type ('a, 'e) t = [%import: ('a, 'e) Stdlib.Result.t] [@@deriving yojson] - end -end - -module Result = Stdlib.Result - -(* ppx_import < 1.10 hack, for some reason it gets confused with the aliases. *) -module Result_ = Stdlib.Result - module Error = struct type t = [%import: Petanque.Agent.Error.t] [@@deriving yojson] end @@ -36,57 +20,24 @@ module Run_result = struct type 'a t = [%import: 'a Petanque.Agent.Run_result.t] [@@deriving yojson] end +(* Both are needed as of today *) +module Stdlib = Lsp.JStdlib +module Result = Stdlib.Result + module R = struct - type 'a t = - [%import: - ('a Petanque.Agent.R.t - [@with - Stdlib.Result.t := Result_.t; - Result.t := Result_.t])] - [@@deriving yojson] + type 'a t = [%import: 'a Petanque.Agent.R.t] [@@deriving yojson] end module Goals = struct type t = string Lsp.JCoq.Goals.reified_pp option [@@deriving yojson] end -module Lang = struct - module Range = struct - type t = Lsp.JLang.Range.t [@@deriving yojson] - end - - module With_range = struct - type 'a t = [%import: ('a Lang.With_range.t[@with Lang.Range.t := Range.t])] - [@@deriving yojson] - end - - module Ast = struct - module Name = struct - type t = [%import: Lang.Ast.Name.t] [@@deriving yojson] - end - - module Info = struct - type t = - [%import: - (Lang.Ast.Info.t - [@with - Lang.Range.t := Range.t; - Lang.With_range.t := With_range.t])] - [@@deriving yojson] - end - end -end +module Lang = Lsp.JLang module Premise = struct module Info = struct type t = [%import: Petanque.Agent.Premise.Info.t] [@@deriving yojson] end - type t = - [%import: - (Petanque.Agent.Premise.t - [@with - Stdlib.Result.t := Result_.t; - Result.t := Result_.t])] - [@@deriving yojson] + type t = [%import: Petanque.Agent.Premise.t] [@@deriving yojson] end diff --git a/petanque/json_shell/protocol_shell.ml b/petanque/json_shell/protocol_shell.ml index 4f4bb4d7..12acda71 100644 --- a/petanque/json_shell/protocol_shell.ml +++ b/petanque/json_shell/protocol_shell.ml @@ -6,7 +6,6 @@ (************************************************************************) open Petanque_json -open JAgent (** [set_workspace { debug; root }] sets the current workspace to the directory specified in [root] *) @@ -47,7 +46,8 @@ module TableOfContents = struct end module Response = struct - type t = (string * Lang.Ast.Info.t list option) list [@@deriving yojson] + type t = (string * Lsp.JLang.Ast.Info.t list option) list + [@@deriving yojson] end module Handler = struct diff --git a/petanque/json_shell/shell.ml b/petanque/json_shell/shell.ml index 3d4324b4..a9dccdb4 100644 --- a/petanque/json_shell/shell.ml +++ b/petanque/json_shell/shell.ml @@ -1,12 +1,14 @@ 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 ; coqcorelib = Filename.concat Coq_config.coqlib "../coq-core" - ; ocamlpath = None + ; findlib_config = None + ; ocamlpath = [] ; vo_load_path = [] ; ml_include_path = [] ; args = [] diff --git a/plugins/explain_errors/dune b/plugins/explain_errors/dune new file mode 100644 index 00000000..4f4fc5f2 --- /dev/null +++ b/plugins/explain_errors/dune @@ -0,0 +1,4 @@ +(library + (name Explain_errors) + (public_name coq-lsp.plugin.explain_errors) + (libraries coq-lsp.fleche)) diff --git a/plugins/explain_errors/main.ml b/plugins/explain_errors/main.ml new file mode 100644 index 00000000..599a856e --- /dev/null +++ b/plugins/explain_errors/main.ml @@ -0,0 +1,58 @@ +(* Example plugin to print errors with goals *) +(* c.f. https://github.com/coq/coq/issues/19601 *) +open Fleche + +let msg_info ~io = Io.(Report.msg ~io ~lvl:Info) + +let pp_goals ~token ~st = + match Coq.State.lemmas ~st with + | None -> Pp.str "no goals" + | Some proof -> ( + match Coq.Print.pr_goals ~token ~proof with + | { Coq.Protect.E.r = Completed (Ok goals); _ } -> goals + | { Coq.Protect.E.r = Completed (Error (User msg | Anomaly msg)); _ } -> + Pp.(str "error when printing goals: " ++ snd msg) + | { Coq.Protect.E.r = Interrupted; _ } -> + Pp.str "goal printing was interrupted") + +module Error_info = struct + type t = + { error : Pp.t + ; command : string + ; goals : Pp.t + } + + let print ~io { error; command; goals } = + msg_info ~io + "[explain errors plugin]@\n\ + Error:@\n\ + \ @[%a@]@\n\ + @\n\ + when trying to apply@\n\ + @\n\ + \ @[%s@]@\n\ + for goals:@\n\ + \ @[%a@]" Pp.pp_with error command Pp.pp_with goals +end + +let extract_errors ~token ~root ~contents (node : Doc.Node.t) = + let errors = List.filter Lang.Diagnostic.is_error node.diags in + let st = Option.cata Doc.Node.state root node.prev in + let command = Contents.extract_raw ~contents ~range:node.range in + let goals = pp_goals ~token ~st in + List.map + (fun { Lang.Diagnostic.message; _ } -> + { Error_info.error = message; command; goals }) + errors + +let explain_error ~io ~token ~(doc : Doc.t) = + let root = doc.root in + let contents = doc.contents in + let errors = + List.(map (extract_errors ~token ~root ~contents) doc.nodes |> concat) + in + msg_info ~io "[explain errors plugin] we got %d errors" (List.length errors); + List.iter (Error_info.print ~io) errors + +let main () = Theory.Register.Completed.add explain_error +let () = main () diff --git a/plugins/explain_errors/main.mli b/plugins/explain_errors/main.mli new file mode 100644 index 00000000..948db8fa --- /dev/null +++ b/plugins/explain_errors/main.mli @@ -0,0 +1 @@ +(* *) diff --git a/serlib/plugins/ltac2/ser_tac2expr.ml b/serlib/plugins/ltac2/ser_tac2expr.ml index 65eb5a41..dd25268c 100644 --- a/serlib/plugins/ltac2/ser_tac2expr.ml +++ b/serlib/plugins/ltac2/ser_tac2expr.ml @@ -169,7 +169,7 @@ module T2ESpec = struct | CTacFun of raw_patexpr list * raw_tacexpr | CTacApp of raw_tacexpr * raw_tacexpr list | CTacSyn of (Names.lname * raw_tacexpr) list * Names.KerName.t - | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * Names.KerName.t + | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr | CTacCnv of raw_tacexpr * raw_typexpr | CTacSeq of raw_tacexpr * raw_tacexpr | CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr diff --git a/serlib/plugins/ltac2_ltac1/dune b/serlib/plugins/ltac2_ltac1/dune new file mode 100644 index 00000000..58952247 --- /dev/null +++ b/serlib/plugins/ltac2_ltac1/dune @@ -0,0 +1,12 @@ +(library + (name serlib_ltac2_ltac1) + (public_name coq-lsp.serlib.ltac2_ltac1) + (synopsis "Serialization Library for Coq Ltac2_ltac1 Plugin") + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) + (libraries coq-core.plugins.ltac2_ltac1 serlib sexplib)) diff --git a/serlib/plugins/ltac2_ltac1/ser_tac2quote_ltac1.ml b/serlib/plugins/ltac2_ltac1/ser_tac2quote_ltac1.ml new file mode 100644 index 00000000..d0eb012f --- /dev/null +++ b/serlib/plugins/ltac2_ltac1/ser_tac2quote_ltac1.ml @@ -0,0 +1 @@ +(* empty until we support Ltac2 genargs *) diff --git a/serlib_8_18/serlib/dune b/serlib_8_18/serlib/dune index 70b49ecd..8d1620e4 100644 --- a/serlib_8_18/serlib/dune +++ b/serlib_8_18/serlib/dune @@ -2,6 +2,11 @@ (name serlib) (public_name coq-lsp.serlib) (synopsis "Serialization Library for Coq") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare ppx_deriving_yojson)) + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_hash + ppx_compare + ppx_deriving_yojson)) (libraries result coq-core.stm sexplib)) - diff --git a/serlib_8_18/serlib/plugins/cc/dune b/serlib_8_18/serlib/plugins/cc/dune index 9a15cc2e..28ca0e2d 100644 --- a/serlib_8_18/serlib/plugins/cc/dune +++ b/serlib_8_18/serlib/plugins/cc/dune @@ -2,5 +2,11 @@ (name serlib_cc) (public_name coq-lsp.serlib.cc) (synopsis "Serialization Library for Coq Congruence Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) (libraries coq-core.plugins.cc serlib sexplib)) diff --git a/serlib_8_18/serlib/plugins/extraction/dune b/serlib_8_18/serlib/plugins/extraction/dune index ff31030a..01de14be 100644 --- a/serlib_8_18/serlib/plugins/extraction/dune +++ b/serlib_8_18/serlib/plugins/extraction/dune @@ -2,5 +2,6 @@ (name serlib_extraction) (public_name coq-lsp.serlib.extraction) (synopsis "Serialization Library for Coq Fundind Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv)) + (preprocess + (staged_pps ppx_import ppx_sexp_conv)) (libraries coq-core.plugins.extraction serlib)) diff --git a/serlib_8_18/serlib/plugins/firstorder/dune b/serlib_8_18/serlib/plugins/firstorder/dune index d97e959b..ee351fc9 100644 --- a/serlib_8_18/serlib/plugins/firstorder/dune +++ b/serlib_8_18/serlib/plugins/firstorder/dune @@ -2,5 +2,6 @@ (name serlib_firstorder) (public_name coq-lsp.serlib.firstorder) (synopsis "Serialization Library for Coq Firstorder Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare)) + (preprocess + (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare)) (libraries coq-core.plugins.firstorder serlib sexplib)) diff --git a/serlib_8_18/serlib/plugins/funind/dune b/serlib_8_18/serlib/plugins/funind/dune index 24868223..591c0571 100644 --- a/serlib_8_18/serlib/plugins/funind/dune +++ b/serlib_8_18/serlib/plugins/funind/dune @@ -2,5 +2,6 @@ (name serlib_funind) (public_name coq-lsp.serlib.funind) (synopsis "Serialization Library for Coq Fundind Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare)) + (preprocess + (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare)) (libraries coq-core.plugins.funind serlib serlib_ltac sexplib)) diff --git a/serlib_8_18/serlib/plugins/ltac/dune b/serlib_8_18/serlib/plugins/ltac/dune index a0a27370..b2668504 100644 --- a/serlib_8_18/serlib/plugins/ltac/dune +++ b/serlib_8_18/serlib/plugins/ltac/dune @@ -2,5 +2,11 @@ (name serlib_ltac) (public_name coq-lsp.serlib.ltac) (synopsis "Serialization Library for Coq [LTAC plugin]") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) (libraries coq-core.plugins.ltac serlib sexplib)) diff --git a/serlib_8_18/serlib/plugins/ltac2/dune b/serlib_8_18/serlib/plugins/ltac2/dune index cdf4769d..fe468ad6 100644 --- a/serlib_8_18/serlib/plugins/ltac2/dune +++ b/serlib_8_18/serlib/plugins/ltac2/dune @@ -2,5 +2,11 @@ (name serlib_ltac2) (public_name coq-lsp.serlib.ltac2) (synopsis "Serialization Library for Coq [LTAC2 plugin]") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) (libraries coq-core.plugins.ltac2 serlib sexplib)) diff --git a/serlib_8_18/serlib/plugins/micromega/dune b/serlib_8_18/serlib/plugins/micromega/dune index 41e8e947..9f0296e9 100644 --- a/serlib_8_18/serlib/plugins/micromega/dune +++ b/serlib_8_18/serlib/plugins/micromega/dune @@ -2,5 +2,11 @@ (name serlib_micromega) (public_name coq-lsp.serlib.micromega) (synopsis "Serialization Library for Coq Congruence Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) (libraries coq-core.plugins.micromega serlib sexplib)) diff --git a/serlib_8_18/serlib/plugins/ring/dune b/serlib_8_18/serlib/plugins/ring/dune index dd456ffb..6b7b8e47 100644 --- a/serlib_8_18/serlib/plugins/ring/dune +++ b/serlib_8_18/serlib/plugins/ring/dune @@ -2,5 +2,6 @@ (name serlib_ring) (public_name coq-lsp.serlib.ring) (synopsis "Serialization Library for Coq Setoid Newring Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare)) + (preprocess + (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare)) (libraries coq-core.plugins.ring serlib serlib_ltac sexplib)) diff --git a/serlib_8_18/serlib/plugins/ssr/dune b/serlib_8_18/serlib/plugins/ssr/dune index 96810811..277917c8 100644 --- a/serlib_8_18/serlib/plugins/ssr/dune +++ b/serlib_8_18/serlib/plugins/ssr/dune @@ -2,5 +2,16 @@ (name serlib_ssr) (public_name coq-lsp.serlib.ssreflect) (synopsis "Serialization Library for Coq [SSR plugin]") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) - (libraries coq-core.plugins.ssreflect serlib serlib_ltac serlib_ssrmatching sexplib)) + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) + (libraries + coq-core.plugins.ssreflect + serlib + serlib_ltac + serlib_ssrmatching + sexplib)) diff --git a/serlib_8_18/serlib/plugins/ssrmatching/dune b/serlib_8_18/serlib/plugins/ssrmatching/dune index 8fa026ab..f4192e2d 100644 --- a/serlib_8_18/serlib/plugins/ssrmatching/dune +++ b/serlib_8_18/serlib/plugins/ssrmatching/dune @@ -2,5 +2,11 @@ (name serlib_ssrmatching) (public_name coq-lsp.serlib.ssrmatching) (synopsis "Serialization Library for Coq [SSR Matching plugin]") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) (libraries coq-core.plugins.ssrmatching serlib serlib_ltac sexplib)) diff --git a/serlib_8_18/serlib/plugins/syntax/dune b/serlib_8_18/serlib/plugins/syntax/dune index a6fe47e6..aea4ef0a 100644 --- a/serlib_8_18/serlib/plugins/syntax/dune +++ b/serlib_8_18/serlib/plugins/syntax/dune @@ -2,5 +2,11 @@ (name serlib_number_string_notation_plugin) (public_name coq-lsp.serlib.number_string_notation) (synopsis "Serialization Library for Coq Number and String Syntax Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) (libraries coq-core.plugins.number_string_notation serlib sexplib)) diff --git a/serlib_8_18/serlib/plugins/tauto/dune b/serlib_8_18/serlib/plugins/tauto/dune index e055cd3e..9170dbc0 100644 --- a/serlib_8_18/serlib/plugins/tauto/dune +++ b/serlib_8_18/serlib/plugins/tauto/dune @@ -2,5 +2,11 @@ (name serlib_tauto) (public_name coq-lsp.serlib.tauto) (synopsis "Serialization Library for Coq Tauto Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) (libraries coq-core.plugins.tauto serlib sexplib)) diff --git a/serlib_8_18/serlib/plugins/zify/dune b/serlib_8_18/serlib/plugins/zify/dune index 89f41f8a..96332e6a 100644 --- a/serlib_8_18/serlib/plugins/zify/dune +++ b/serlib_8_18/serlib/plugins/zify/dune @@ -2,5 +2,11 @@ (name serlib_zify) (public_name coq-lsp.serlib.zify) (synopsis "Serialization Library for Coq Congruence Plugin") - (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_hash ppx_compare)) + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) (libraries coq-core.plugins.zify serlib sexplib)) diff --git a/serlib_8_20/plugins/ltac2_ltac1/dune b/serlib_8_20/plugins/ltac2_ltac1/dune new file mode 100644 index 00000000..58952247 --- /dev/null +++ b/serlib_8_20/plugins/ltac2_ltac1/dune @@ -0,0 +1,12 @@ +(library + (name serlib_ltac2_ltac1) + (public_name coq-lsp.serlib.ltac2_ltac1) + (synopsis "Serialization Library for Coq Ltac2_ltac1 Plugin") + (preprocess + (staged_pps + ppx_import + ppx_sexp_conv + ppx_deriving_yojson + ppx_hash + ppx_compare)) + (libraries coq-core.plugins.ltac2_ltac1 serlib sexplib)) diff --git a/serlib_8_20/plugins/ltac2_ltac1/ser_tac2quote_ltac1.ml b/serlib_8_20/plugins/ltac2_ltac1/ser_tac2quote_ltac1.ml new file mode 100644 index 00000000..d0eb012f --- /dev/null +++ b/serlib_8_20/plugins/ltac2_ltac1/ser_tac2quote_ltac1.ml @@ -0,0 +1 @@ +(* empty until we support Ltac2 genargs *) diff --git a/test/CoqProject/_CoqProject b/test/CoqProject/_CoqProject index 3bf09db5..73b8c6f8 100644 --- a/test/CoqProject/_CoqProject +++ b/test/CoqProject/_CoqProject @@ -3,6 +3,6 @@ -arg -w -arg -local-declaration -arg -w -arg +non-primitive-record --arg -rifrom -arg Coq.Lists -arg List +-arg -rifrom -arg Stdlib.Lists -arg List test.v diff --git a/test/compiler/basic/run.t b/test/compiler/basic/run.t index 94ea7aa1..a5af49a8 100644 --- a/test/compiler/basic/run.t +++ b/test/compiler/basic/run.t @@ -8,7 +8,7 @@ Describe the project + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] @@ -19,7 +19,7 @@ Compile a single file, don't generate a `.vo` file: + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/a.v @@ -35,7 +35,7 @@ Compile a single file, generate a .vo file + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/a.v @@ -55,7 +55,7 @@ Compile a dependent file + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/b.v @@ -75,14 +75,11 @@ Compile both files + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/a.v [message] compiling file proj1/b.v -<<<<<<< HEAD -======= ->>>>>>> main $ ls proj1 a.diags a.v @@ -99,13 +96,10 @@ Compile a dependent file without the dep being built + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/b.v -<<<<<<< HEAD -======= ->>>>>>> main $ ls proj1 a.diags a.v @@ -139,7 +133,7 @@ Compile a file with all messages: + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/a.v @@ -150,7 +144,7 @@ Compile a file with all messages: + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/a.v @@ -180,7 +174,7 @@ Use two workspaces + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] Configuration loaded from Command-line arguments @@ -188,7 +182,7 @@ Use two workspaces + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/a.v @@ -197,12 +191,6 @@ Use two workspaces Sys_error("proj2/b.v: No such file or directory") [125] -<<<<<<< HEAD -======= ->>>>>>> main -<<<<<<< HEAD -======= ->>>>>>> main Load the example plugin $ fcc --plugin=coq-lsp.plugin.example --root proj1 proj1/a.v @@ -211,14 +199,11 @@ Load the example plugin + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/a.v [message] [example plugin] file checking for proj1/a.v was completed -<<<<<<< HEAD -======= ->>>>>>> main Load the astdump plugin $ fcc --plugin=coq-lsp.plugin.astdump --root proj1 proj1/a.v @@ -227,15 +212,12 @@ Load the astdump plugin + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/a.v [message] [ast plugin] dumping ast for proj1/a.v ... [message] [ast plugin] dumping ast for proj1/a.v was completed! -<<<<<<< HEAD -======= ->>>>>>> main EJGA: I'd be nice to check the checksum of files here, however `md5sum` is not avilable on all of our CI platforms yet. `ls -l` @@ -255,7 +237,7 @@ We do the same for the goaldump plugin: + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file proj1/a.v diff --git a/test/compiler/exit_code/run.t b/test/compiler/exit_code/run.t index 3d2af0e4..0ca22ebe 100644 --- a/test/compiler/exit_code/run.t +++ b/test/compiler/exit_code/run.t @@ -9,7 +9,7 @@ Describe the environment: + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 3 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] diff --git a/test/compiler/long_file/run.t b/test/compiler/long_file/run.t index 86fcb14a..e5939c37 100644 --- a/test/compiler/long_file/run.t +++ b/test/compiler/long_file/run.t @@ -12,7 +12,7 @@ We now compile the challenging file: + coqcorelib is at: [TEST_PATH] - Modules [Coq.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope - - ocamlpath wasn't overriden + - ocamlpath added paths: [] + findlib config: [TEST_PATH] + findlib default location: [TEST_PATH] [message] compiling file ./test.v diff --git a/test/serlib/genarg/ItHolds.v b/test/serlib/genarg/ItHolds.v new file mode 100644 index 00000000..e9c32a78 --- /dev/null +++ b/test/serlib/genarg/ItHolds.v @@ -0,0 +1,233 @@ +(******************************************************************************) +(* This file is part of Waterproof-lib. *) +(* *) +(* Waterproof-lib is free software: you can redistribute it and/or modify *) +(* it under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 3 of the License, or *) +(* (at your option) any later version. *) +(* *) +(* Waterproof-lib is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU General Public License for more details. *) +(* *) +(* You should have received a copy of the GNU General Public License *) +(* along with Waterproof-lib. If not, see . *) +(* *) +(******************************************************************************) + +Require Import Ltac2.Ltac2. +Require Import Ltac2.Message. +Local Ltac2 concat_list (ls : message list) : message := + List.fold_right concat ls (of_string ""). + +(** Tries to make the assertion [True] with label [label]. + Throws an error if this fails, i.e. if the label is already used + for another one of the hypotheses. + + This check was separated out from the 'assert'-tactics below because the + '[label] is already used error' would otherwise be caught in + the code meant to catch [AutomationFailure] errors. *) + +Local Ltac2 try_out_label (label : ident) := + match Control.case (fun () => + assert True as $label by exact I) + with + | Err exn => Control.zero exn + | Val _ => clear $label + end. + +(* For making tests independent of WaterProof *) +Ltac2 warn : message -> unit := fun _ => (). +Ltac2 throw : message -> unit := fun _ => (). +Ltac2 waterprove (_depth: int) (_shield: bool) (_db_type: 'a) := (). +Ltac2 rwaterprove (_depth: int) (_shield: bool) (_db_type: 'a) (_ : constr) := (). +Ltac2 suggest_how_to_use (_x : constr) (_label : ident option) := (). +Ltac2 Type exn ::= [ FailedToProve(constr) ]. +Ltac2 correct_type_by_wrapping (t: constr): constr := t. +Ltac2 wrapper_core_by_tactic (_by_tactic : constr -> unit) (_xtr_lemma : constr) := (). +Ltac2 panic_if_goal_wrapped () := (). +Ltac2 since_framework (_by_tactic : constr -> unit) (_claimed_cause : constr) := (). + +(** Attempts to assert that [claim] holds, if succesful [claim] is added to the local + hypotheses. If [label] is specified [claim] is given [label] as its identifier, otherwise an + identifier starting with '_H' is generated. + + Additionally, if argument [postpone] is [true], actually proving the claim is postponed. + The claim is asserted and the proof is shelved using an evar. + *) +Local Ltac2 wp_assert (claim : constr) (label : ident option) (postpone : bool):= + let err_msg (g : constr) := concat_list + [of_string "Could not verify that "; of_constr g; of_string "."] in + let id := + match label with + | None => Fresh.in_goal @_H + | Some label => try_out_label label; label + end + in + let claim := claim in + if postpone + then + (* Assert claim and proof using shelved evar *) + (* (using 'admit' would have shown a confusing warning message) *) + assert $claim as $id; + Control.focus 1 1 (fun () => + let evar_id := Fresh.in_goal @_Hpostpone in + ltac1:(id claim |- evar (id : claim)) (Ltac1.of_ident evar_id) (Ltac1.of_constr claim); + let evar := Control.hyp evar_id in + exact $evar + ); + warn (concat_list [of_string "Please come back later to provide an actual proof of "; + of_constr claim; of_string "."]) + + else + (* Assert claim and attempt to prove automatically *) + match Control.case (fun () => + assert $claim as $id by + (waterprove 5 true 99)) + with + | Val _ => () + | Err (FailedToProve g) => throw (err_msg g) + | Err exn => Control.zero exn + end; + (* Print suggestion on how to use new statement. *) + suggest_how_to_use claim label. + +(** Attempts to assert that [claim] holds, if succesful [claim] is added to the local + hypotheses. If [label] is specified [claim] is given [label] as its identifier, otherwise an + identifier starting with '_H' is generated. + [xtr_lemma] has to be used in the proof that [claim] holds. + *) +Local Ltac2 core_wp_assert_by (claim : constr) (label : ident option) (xtr_lemma : constr) := + let err_msg (g : constr) := concat_list + [of_string "Could not verify that "; of_constr g; of_string "."] in + let id := + match label with + | None => Fresh.in_goal @_H + | Some label => try_out_label label; label + end + in + let claim := correct_type_by_wrapping claim in + match Control.case (fun () => + assert $claim as $id by + (rwaterprove 5 true 19 xtr_lemma)) + with + | Val _ => () + | Err (FailedToProve g) => throw (err_msg g) + | Err exn => Control.zero exn (* includes FailedToUse error *) + end. + +(** Adaptation of [core_wp_assert_by] that turns the [FailedToUse] errors + which might be thrown into user readable errors. *) +Local Ltac2 wp_assert_by (claim : constr) (label : ident option) (xtr_lemma : constr) := + wrapper_core_by_tactic (core_wp_assert_by claim label) xtr_lemma; + (* Print suggestion on how to use new statement. *) + suggest_how_to_use claim label. + +(** Adaptation of [core_wp_assert_by] that allows user to use mathematical statements themselves + instead of references to them as extra information for the automation system. + Uses the code in [Since.v]. *) +Local Ltac2 wp_assert_since (claim : constr) (label : ident option) (xtr_claim : constr) := + since_framework (core_wp_assert_by claim label) xtr_claim; + (* Print suggestion on how to use new statement. *) + suggest_how_to_use claim label. + + +(** + Attempts to assert a claim and proves it automatically using a specified lemma, + this lemma has to be used. + + Arguments: + - [xtr_lemma: constr], reference to a lemma used to prove the claim (via [rwaterprove]). + - [label: ident option], optional name for the claim. + If the proof succeeds, it will become a hypothesis (bearing [label] as name). + - [claim: constr], the actual content of the claim to prove. + + Raises exception: + - (fatal) if [rwaterprove] fails to prove the claim using the specified lemma. + - [[label] is already used], if there is already another hypothesis with identifier [label]. +*) +Ltac2 Notation "By" xtr_lemma(constr) "it" "holds" "that" claim(constr) label(opt(seq("(", ident, ")"))) := + panic_if_goal_wrapped (); + wp_assert_by claim label xtr_lemma. + +Ltac2 Notation "Since" xtr_claim(constr) "it" "holds" "that" claim(constr) label(opt(seq("(", ident, ")"))) := + panic_if_goal_wrapped (); + wp_assert_since claim label xtr_claim. + + +(** * It holds that ... (...) + Attempts to assert a claim and proves it automatically. + Removes [StateHyp.Wrapper] wrapper from the goal (proving claim by automation not necessary). + + Arguments: + - [label: ident option], optional name for the claim. + If the proof succeeds, it will become a hypothesis (bearing [label] as name). + - [claim: constr], the actual content of the claim to prove. + + Raises exception: + - (fatal) if [rwaterprove] fails to prove the claim using the specified lemma. + - [[label] is already used], if there is already another hypothesis with identifier [label]. + - (fatal) If goal is wrapped in [StateHyp.Wrapper] and the wrong statement is specified. +*) +Inductive Wrapper (A : Type) (h : A) (G : Type) : Type := + | wrap : G -> Wrapper A h G. +Ltac2 check_constr_equal (_a: constr) (_b: constr) := false. + +Local Ltac2 wp_assert_with_unwrap (claim : constr) (label : ident option) := + (* Try out label first. + Code results in wrong error if done inside repeated match.. *) + match label with | None => () | Some label => try_out_label label end; + + match! goal with + | [h : ?s |- Wrapper ?s ?h_spec _] => + let h_constr := Control.hyp h in + (* sanity check "h = h_spec" *) + if check_constr_equal h_constr h_spec + then () + else fail; + let w := match label with + | None => Fresh.fresh (Fresh.Free.of_goal ()) @_H + | Some label => label + end in + if check_constr_equal s claim + then + match Control.case (fun () => assert $claim as $w by exact $h_constr) with + | Val _ => (* If claims are definitionally equal, go with the + version that is supplied as argument to "It holds that ..." *) + apply (wrap $s); + Std.clear [h] + | Err exn => print (of_string "Exception occurred"); print (of_exn exn) + end + else throw (of_string "Wrong statement specified.") + (* rename ident generated in specialize with user-specified label*) + (* match label with + | None => () + | Some label => Std.rename [(w, label)] + end *) + | [|- _] => + panic_if_goal_wrapped (); + wp_assert claim label false + end. + +Ltac2 Notation "It" "holds" "that" claim(constr) label(opt(seq("(", ident, ")"))) := + wp_assert_with_unwrap claim label. + + +(** * By magic it holds that ... (...) + Asserts a claim and proves it using a shelved evar. + + Arguments: + - [label: ident option], optional name for the claim. + - [claim: constr], the actual content of the claim to prove. + + Raises exception: + - [[label] is already used], if there is already another hypothesis with identifier [label]. + + Raises warning: + - [Please come back later to provide an actual proof of [claim].], always. +*) + +Ltac2 Notation "By" "magic" "it" "holds" "that" claim(constr) label(opt(seq("(", ident, ")"))) := + panic_if_goal_wrapped (); + wp_assert claim label true. \ No newline at end of file diff --git a/test/serlib/genarg/dune b/test/serlib/genarg/dune index 7291a34f..23a1cebe 100644 --- a/test/serlib/genarg/dune +++ b/test/serlib/genarg/dune @@ -143,6 +143,14 @@ (action (bash "./%{script} %{input}"))) +(rule + (alias runtest) + (deps + (:script test_roundtrip) + (:input ItHolds.v)) + (action + (bash "./%{script} %{input}"))) + (rule (alias runtest) (deps diff --git a/test/serlib/genarg/extraction.v b/test/serlib/genarg/extraction.v index ec92c845..a771e714 100644 --- a/test/serlib/genarg/extraction.v +++ b/test/serlib/genarg/extraction.v @@ -1,4 +1,4 @@ -Require Coq.extraction.Extraction. +Require Stdlib.extraction.Extraction. Extraction Language Haskell. diff --git a/test/serlib/genarg/libTactics.v b/test/serlib/genarg/libTactics.v index 451a77ad..d909a7e8 100644 --- a/test/serlib/genarg/libTactics.v +++ b/test/serlib/genarg/libTactics.v @@ -370,7 +370,7 @@ Ltac fast_rm_inside E := Note: the tactic [number_to_nat] is extended in [LibInt] to take into account the [int] type, alias for [Z]. *) -Require Coq.Numbers.BinNums Coq.ZArith.BinInt. +Require Stdlib.Numbers.BinNums Stdlib.ZArith.BinInt. Definition ltac_int_to_nat (x:BinInt.Z) : nat := match x with @@ -2519,7 +2519,7 @@ Tactic Notation "subst_eq" constr(E) := (* ---------------------------------------------------------------------- *) (** ** Tactics to work with proof irrelevance *) -Require Import Coq.Logic.ProofIrrelevance. +Require Import Stdlib.Logic.ProofIrrelevance. (** [pi_rewrite E] replaces [E] of type [Prop] with a fresh unification variable, and is thus a practical way to @@ -3098,7 +3098,7 @@ Tactic Notation "cases_if'" := [inductions E gen X1 .. XN] is a shorthand for [dependent induction E generalizing X1 .. XN]. *) -Require Import Coq.Program.Equality. +Require Import Stdlib.Program.Equality. Ltac inductions_post := unfold eq' in *. @@ -3189,7 +3189,7 @@ Tactic Notation "induction_wf" ":" constr(E) ident(X) := judgment that includes a counter for the maximal height (see LibTacticsDemos for an example) *) -Require Import Coq.Arith.Compare_dec. +Require Import Stdlib.Arith.Compare_dec. Require Import Lia. Lemma induct_height_max2 : forall n1 n2 : nat, @@ -4166,7 +4166,7 @@ Tactic Notation "exists" "~" constr(T1) "," constr(T2) "," constr(T3) "," same as for light automation. Exception: use [subs*] instead of [subst*] if you - import the library [Coq.Classes.Equivalence]. *) + import the library [Stdlib.Classes.Equivalence]. *) Tactic Notation "equates" "*" constr(E) := equates E; auto_star. @@ -5007,7 +5007,7 @@ Open Scope nat_scope. (** [exists T1 ... TN, P] is a shorthand for [exists T1, ..., exists TN, P]. Note that - [Coq.Program.Syntax] already defines exists + [Stdlib.Program.Syntax] already defines exists for arity up to 4. *) Notation "'exists' x1 ',' P" :=