From d3b77acb7ce752b893639cb94698f7d89e25d130 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 30 Aug 2024 17:15:34 +0200 Subject: [PATCH 01/31] [petanque] Update README --- petanque/README.md | 1 + 1 file changed, 1 insertion(+) 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 From c1236756609f30c9f8b83b0cc10da65eab7f53ec Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 30 Aug 2024 21:23:20 +0200 Subject: [PATCH 02/31] [nix] [build] Update flake to more modern ppx packages. --- .github/workflows/build.yml | 4 ++-- flake.lock | 48 ++++++++++++++++--------------------- flake.nix | 5 ++-- 3 files changed, 25 insertions(+), 32 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 7faca7df..e45be040 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -133,10 +133,10 @@ jobs: submodules: recursive - name: ❄️ Setup Nix - uses: cachix/install-nix-action@v22 + uses: cachix/install-nix-action@v27 - name: 🧱 Build coq-lsp - run: nix build .?submodules=1 + run: nix build '.?submodules=1#' client-compile: runs-on: ubuntu-latest 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..0b4f98d6 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; From 6219d342d5026634f101f2339ee254d08f295181 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Aug 2024 18:17:11 +0200 Subject: [PATCH 03/31] [build] [deps] Bump ppxlib toolchain to 0.26.0. It is time to clean up this old compat setup once that #698 has been completed; old `ppx_import` is giving us too much trouble with `petanque`. --- CHANGES.md | 8 ++++ coq-lsp.opam | 20 ++++----- lsp/jLang.ml | 23 ++++++++++ lsp/jLang.mli | 6 +++ lsp/jStdlib.ml | 5 +++ petanque/json/jAgent.ml | 63 +++------------------------ petanque/json_shell/protocol_shell.ml | 4 +- 7 files changed, 61 insertions(+), 68 deletions(-) create mode 100644 lsp/jStdlib.ml diff --git a/CHANGES.md b/CHANGES.md index bcc7ad96..dacded90 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,11 @@ +# 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) + # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/coq-lsp.opam b/coq-lsp.opam index cf4ddd26..950f6166 100644 --- a/coq-lsp.opam +++ b/coq-lsp.opam @@ -34,23 +34,23 @@ depends: [ "menhir" { >= "20220210" } # unit testing - "ppx_inline_test" { >= "0.14.1" } + "ppx_inline_test" { >= "v0.15.0" } # Uncomment this for releases # "coq" { >= "8.17" < "8.18" } # coq deps: remove this for releases - "ocamlfind" {>= "1.8.1"} - "zarith" {>= "1.11"} + "ocamlfind" {>= "1.9.1"} + "zarith" {>= "1.13"} # 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/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/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 From 2180402e4af0096b1a3419f1d7783bea7ec9d43f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 19 Jul 2024 09:59:27 +0200 Subject: [PATCH 04/31] [coq] Adapt to https://github.com/coq/coq/pull/19310 --- coq/workspace.ml | 2 +- test/CoqProject/_CoqProject | 2 +- test/compiler/basic/run.t | 26 +++++++++++++------------- test/compiler/exit_code/run.t | 2 +- test/compiler/long_file/run.t | 2 +- test/serlib/genarg/extraction.v | 2 +- test/serlib/genarg/libTactics.v | 14 +++++++------- vendor/coq | 2 +- 8 files changed, 26 insertions(+), 26 deletions(-) diff --git a/coq/workspace.ml b/coq/workspace.ml index 175550e4..585f577a 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -156,7 +156,7 @@ let make ~cmdline ~implicit ~kind ~debug = in let require_libs = let rq_list = - if init then ((None, "Coq.Init.Prelude") :: require_libraries) @ libs + if init then ((None, "Stdlib.Init.Prelude") :: require_libraries) @ libs else require_libraries @ libs in List.map mk_require_from rq_list 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 92387815..7f39aa5c 100644 --- a/test/compiler/basic/run.t +++ b/test/compiler/basic/run.t @@ -6,7 +6,7 @@ Describe the project [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -17,7 +17,7 @@ Compile a single file, don't generate a `.vo` file: [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -33,7 +33,7 @@ Compile a single file, generate a .vo file [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -53,7 +53,7 @@ Compile a dependent file [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -73,7 +73,7 @@ Compile both files [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -94,7 +94,7 @@ Compile a dependent file without the dep being built [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -131,7 +131,7 @@ Compile a file with all messages: [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -142,7 +142,7 @@ Compile a file with all messages: [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -172,7 +172,7 @@ Use two workspaces [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -180,7 +180,7 @@ Use two workspaces [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -197,7 +197,7 @@ Load the example plugin [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -210,7 +210,7 @@ Load the astdump plugin [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] @@ -235,7 +235,7 @@ We do the same for the goaldump plugin: [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] diff --git a/test/compiler/exit_code/run.t b/test/compiler/exit_code/run.t index c7127987..d27c7722 100644 --- a/test/compiler/exit_code/run.t +++ b/test/compiler/exit_code/run.t @@ -7,7 +7,7 @@ Describe the environment: [message] Configuration loaded from ./_CoqProject - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 3 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] diff --git a/test/compiler/long_file/run.t b/test/compiler/long_file/run.t index f94b793b..83302ca7 100644 --- a/test/compiler/long_file/run.t +++ b/test/compiler/long_file/run.t @@ -10,7 +10,7 @@ We now compile the challenging file: [message] Configuration loaded from Command-line arguments - coqlib is at: [TEST_PATH] + coqcorelib is at: [TEST_PATH] - - Modules [Coq.Init.Prelude] will be loaded by default + - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope - ocamlpath wasn't overriden + findlib config: [TEST_PATH] 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..5f895f69 100644 --- a/test/serlib/genarg/libTactics.v +++ b/test/serlib/genarg/libTactics.v @@ -44,7 +44,7 @@ Set Implicit Arguments. -Require Import Coq.Lists.List. +Require Import Stdlib.Lists.List. (* ********************************************************************** *) @@ -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" := diff --git a/vendor/coq b/vendor/coq index 6a2431e6..7fec4bd9 160000 --- a/vendor/coq +++ b/vendor/coq @@ -1 +1 @@ -Subproject commit 6a2431e6fa1f4a0bbee6d98c3b709aca781061d5 +Subproject commit 7fec4bd91f2873f98541b5ecf640e83369768c99 From 22935b62e13bde0c4cb0fb271ce9021f3cce3ddb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Sep 2024 15:27:44 +0200 Subject: [PATCH 05/31] [workspace] [coq] Support _CoqProject arguments `-type-in-type` and `-allow-rewrite-rules` (for 8.20) --- CHANGES.md | 2 ++ coq/workspace.ml | 27 ++++++++++++++++++++------- coq/workspace.mli | 6 ++++-- 3 files changed, 26 insertions(+), 9 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index dacded90..5450502d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -5,6 +5,8 @@ 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, #) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/coq/workspace.ml b/coq/workspace.ml index 585f577a..3aa2b62a 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -19,15 +19,24 @@ 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); + Global.set_rewrite_rules_allowed rewrite_rules end module Warning : sig @@ -95,10 +104,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 -> diff --git a/coq/workspace.mli b/coq/workspace.mli index fb5b461f..74670083 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 From 1130aabeb326be81104dc5c3bb7587d44a32617a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Sep 2024 22:26:51 +0200 Subject: [PATCH 06/31] [serlib] Support for ltac2_ltac1 plugin --- CHANGES.md | 3 ++- coq/loader.ml | 1 + serlib/plugins/ltac2_ltac1/dune | 12 ++++++++++++ serlib/plugins/ltac2_ltac1/ser_tac2quote_ltac1.ml | 1 + 4 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 serlib/plugins/ltac2_ltac1/dune create mode 100644 serlib/plugins/ltac2_ltac1/ser_tac2quote_ltac1.ml diff --git a/CHANGES.md b/CHANGES.md index 5450502d..9b7570bb 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -6,7 +6,8 @@ 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, #) + `-allow-rewrite-rules` (for 8.20) (@ejgallego, #819) + - [serlib] Support for ltac2_ltac1 plugin (@ejgallego, #820) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- 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/serlib/plugins/ltac2_ltac1/dune b/serlib/plugins/ltac2_ltac1/dune new file mode 100644 index 00000000..151da43d --- /dev/null +++ b/serlib/plugins/ltac2_ltac1/dune @@ -0,0 +1,12 @@ +(library + (name serlib_btauto) + (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 *) From a9e38e0a20ae210b07fafbd5edb2bc54d02a09c0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Sep 2024 22:30:50 +0200 Subject: [PATCH 07/31] [serlib] Fix wrong piercing of Ltac2 AST + test case Thanks to Jim Portegies for testing, report, and test case. --- CHANGES.md | 2 + examples/ItHolds.v | 233 +++++++++++++++++++++++++++ serlib/plugins/ltac2/ser_tac2expr.ml | 2 +- test/serlib/genarg/ItHolds.v | 233 +++++++++++++++++++++++++++ test/serlib/genarg/dune | 8 + 5 files changed, 477 insertions(+), 1 deletion(-) create mode 100644 examples/ItHolds.v create mode 100644 test/serlib/genarg/ItHolds.v diff --git a/CHANGES.md b/CHANGES.md index 9b7570bb..fe00cd85 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -8,6 +8,8 @@ - [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) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- 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/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/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 d4a74cda..dab2a151 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 From fe6ce0ebb3c531e25ab036bcfcf12ae6402681ac Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Sep 2024 18:55:39 +0200 Subject: [PATCH 08/31] [serlib] Fix wrong pack name for ltac2_ltac1 plugin. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bug introduced in #820 Co-authored-by: GaΓ«tan Gilbert --- serlib/plugins/ltac2_ltac1/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/serlib/plugins/ltac2_ltac1/dune b/serlib/plugins/ltac2_ltac1/dune index 151da43d..58952247 100644 --- a/serlib/plugins/ltac2_ltac1/dune +++ b/serlib/plugins/ltac2_ltac1/dune @@ -1,5 +1,5 @@ (library - (name serlib_btauto) + (name serlib_ltac2_ltac1) (public_name coq-lsp.serlib.ltac2_ltac1) (synopsis "Serialization Library for Coq Ltac2_ltac1 Plugin") (preprocess From af3b722f0e7506b0c2a36072df96d9f3f74d1052 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 22 Sep 2024 13:13:36 +0200 Subject: [PATCH 09/31] [coq] Understand rewrite rules and symbols on document outline Fixes: #824 --- CHANGES.md | 2 ++ coq/ast.ml | 19 ++++++++++++++++++- examples/rewrite/_CoqProject | 3 +++ examples/rewrite/simple.v | 26 ++++++++++++++++++++++++++ 4 files changed, 49 insertions(+), 1 deletion(-) create mode 100644 examples/rewrite/_CoqProject create mode 100644 examples/rewrite/simple.v diff --git a/CHANGES.md b/CHANGES.md index fe00cd85..ad0f8e96 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -10,6 +10,8 @@ - [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, #82x, fixes: #824) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/coq/ast.ml b/coq/ast.ml index e260ccd3..9ff98c97 100644 --- a/coq/ast.ml +++ b/coq/ast.ml @@ -128,7 +128,7 @@ module Kinds = struct let _interface = 11 let function_ = 12 let variable = 13 - let _constant = 14 + let constant = 14 let _string = 15 let _number = 16 let _boolean = 17 @@ -278,6 +278,16 @@ let fixpoint_info ~lines ~range { fname; _ } = let detail = "Fixpoint" in Lang.Ast.Info.make ~range ~name ~detail ~kind:Kinds.function_ () +let symbol_info ~lines ~range + ((_, (idents, _typs)) : + (Constrexpr.ident_decl list * Constrexpr.constr_expr) with_coercion) = + let detail = "Rewrite Symbol" in + let mk_info (id, _) = + let name = mk_id ~lines id in + Lang.Ast.Info.make ~range ~name ~detail ~kind:Kinds.constant () + in + List.map mk_info idents + let make_info ~st:_ ~lines CAst.{ loc; v } : Lang.Ast.Info.t list option = let open Vernacexpr in match loc with @@ -310,4 +320,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/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/simple.v b/examples/rewrite/simple.v new file mode 100644 index 00000000..db670c91 --- /dev/null +++ b/examples/rewrite/simple.v @@ -0,0 +1,26 @@ +(* 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 30). + +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. + From 0d9954ab06dffd3c678e421d0e78d3a534cee6e4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 22 Sep 2024 16:12:52 +0200 Subject: [PATCH 10/31] [examples] [rewrite] Add example from Ali, tweak the simple one. --- examples/rewrite/alis.v | 53 +++++++++++++++++++++++++++++++++++++++ examples/rewrite/simple.v | 5 ++-- 2 files changed, 55 insertions(+), 3 deletions(-) create mode 100644 examples/rewrite/alis.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 index db670c91..b22831cb 100644 --- a/examples/rewrite/simple.v +++ b/examples/rewrite/simple.v @@ -5,7 +5,7 @@ Symbols (pmul : nat -> nat -> nat). Notation "a ++ b" := (pplus a b). -Notation "a ** b" := (pmul a b) (at level 30). +Notation "a ** b" := (pmul a b) (at level 50). Rewrite Rules pplus_rewrite := | ?n ++ 0 => ?n @@ -21,6 +21,5 @@ Rewrite Rules pmul_rewrite := | ?n ** S ?m => ?m ++ (?n ** ?m) | ?n ** (?m ** ?o) => (?n ** ?m) ** ?o. -Lemma foo n m : S n ** m ++ 0 = n ++ (n ** m). +Lemma foo n m : S n ** m ++ 0 = n ++ n ** m. Proof. now reflexivity. Qed. - From 32d3cbe29b8c80e853b5f932da1a90e0a53dcf6f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Sep 2024 16:42:09 +0200 Subject: [PATCH 11/31] [coq] [fleche] Support `Restart` command. Thanks to Ali for pointing this out. Fixes #827 --- CHANGES.md | 4 +++- coq/ast.ml | 12 ++++++++---- coq/ast.mli | 5 +++-- examples/MetaCommands.v | 7 +++++++ fleche/doc.ml | 12 ++++++++++++ 5 files changed, 33 insertions(+), 7 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index ad0f8e96..a5f2ba03 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -11,7 +11,9 @@ - [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, #82x, fixes: #824) + outline (@ejgallego, @Alizter, #825, fixes: #824) + - [fleche] [coq] support `Restart` meta command (@ejgallego, + @Alizter, #829, fixes #828) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/coq/ast.ml b/coq/ast.ml index 9ff98c97..8f0692c7 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 } diff --git a/coq/ast.mli b/coq/ast.mli index 950afeb1..e68be82a 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/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/fleche/doc.ml b/fleche/doc.ml index 9a01c900..21c58f39 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -552,6 +552,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 +679,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 From 472fc108b7158dcb9e59289d5428fd9836ca6ab9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Sep 2024 15:59:58 +0200 Subject: [PATCH 12/31] [vendor] [deps] bump Coq --- vendor/coq | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vendor/coq b/vendor/coq index 7fec4bd9..b6805232 160000 --- a/vendor/coq +++ b/vendor/coq @@ -1 +1 @@ -Subproject commit 7fec4bd91f2873f98541b5ecf640e83369768c99 +Subproject commit b68052328b65a3e85cd48a4718713fdd0c24f08d From 040aca3910ce9a26cec7119d52441d3e577d677b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Sep 2024 17:55:32 +0200 Subject: [PATCH 13/31] [nits] Minor refactorings and tweaks from the JS branch. --- controller/coq_lsp.ml | 34 +--------------------------------- controller/lsp_core.ml | 38 +++++++++++++++++++++++++++++++++++++- controller/lsp_core.mli | 7 +++++++ coq/workspace.mli | 1 + editor/code/src/goals.ts | 10 +--------- examples/documentSymbol.v | 4 ++-- 6 files changed, 49 insertions(+), 45 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 3d7746cb..fe410bd2 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -60,38 +60,6 @@ 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 @@ -130,7 +98,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 diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 62963a07..102afbf9 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) @@ -710,3 +714,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/coq/workspace.mli b/coq/workspace.mli index 74670083..fe66abbc 100644 --- a/coq/workspace.mli +++ b/coq/workspace.mli @@ -42,6 +42,7 @@ module Require : sig } end +(* Generated from a _CoqProject, dune (in the future) or command line args *) type t = private { coqlib : string ; coqcorelib : string 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/examples/documentSymbol.v b/examples/documentSymbol.v index 06cf6e4f..a0149e94 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). From 0afa5fb3c7db7ac17ee254350202b894143f609f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Sep 2024 15:07:29 +0200 Subject: [PATCH 14/31] [plugins] Example for error explaining plugin. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Inspired from the comments on Coq's issue 19601. For example, for this file: ```coq Definition a := 3. Lemma foo (n : nat) (f : nat -> nat) : True = False. Proof. now reflexivity. set (g := 3). Qed. ``` ẁe get: ``` Error: In environment n : nat f : nat -> nat Unable to unify "False" with "True". when trying to apply now reflexivity. for goals: 1 goal n : nat f : nat -> nat ============================ True = False [message] [explain errors plugin] Error: (in proof foo): Attempt to save an incomplete proof (there are remaining open goals). when trying to apply Qed. for goals: 1 goal n : nat f : nat -> nat g := 3 : nat ============================ True = False ``` --- CHANGES.md | 7 ++-- coq/print.ml | 8 +++++ coq/print.mli | 3 ++ plugins/explain_errors/dune | 4 +++ plugins/explain_errors/main.ml | 58 +++++++++++++++++++++++++++++++++ plugins/explain_errors/main.mli | 1 + 6 files changed, 79 insertions(+), 2 deletions(-) create mode 100644 plugins/explain_errors/dune create mode 100644 plugins/explain_errors/main.ml create mode 100644 plugins/explain_errors/main.mli diff --git a/CHANGES.md b/CHANGES.md index a5f2ba03..87b0133b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -9,11 +9,14 @@ `-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) + 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, #829, fixes #828) + @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) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- 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/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 @@ +(* *) From 010da4970b9eeca45036e11dd4c6500a717c5de3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 10 Jun 2024 01:13:03 +0200 Subject: [PATCH 15/31] [doc] Some tweaks to PROTOCOL.md documentation. --- etc/doc/PROTOCOL.md | 160 ++++++++++++++++++++++++++++++++------------ 1 file changed, 118 insertions(+), 42 deletions(-) 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 From e9e9f800e378854419569e1186562c1f44722dfe Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Sep 2024 21:24:19 +0200 Subject: [PATCH 16/31] [ci] Bump some actions to remove CI warnings. --- .github/workflows/build.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index e45be040..21416bab 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -58,7 +58,7 @@ jobs: steps: - name: πŸ”­ Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: submodules: recursive @@ -92,7 +92,7 @@ jobs: runs-on: ubuntu-latest steps: - name: πŸ”­ Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: submodules: recursive @@ -128,7 +128,7 @@ jobs: steps: - name: πŸ”­ Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: submodules: recursive @@ -145,9 +145,9 @@ 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 - run: npm ci @@ -158,7 +158,7 @@ jobs: runs-on: ubuntu-latest steps: - name: πŸ”­ Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: submodules: recursive - name: ❄️ Setup Nix From 87997c30f5440ff4354062dc91eabb4ab1083694 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 27 Sep 2024 13:06:18 +0200 Subject: [PATCH 17/31] [fleche] Highlight the full first line of the document on initialization error. --- CHANGES.md | 2 ++ fleche/doc.ml | 6 ++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 87b0133b..a3cb25b6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -17,6 +17,8 @@ - [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) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/fleche/doc.ml b/fleche/doc.ml index 21c58f39..fbde2b1e 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 From ae232f84368a286ae9a59b5817554b99fd58092f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 27 Sep 2024 16:03:13 +0200 Subject: [PATCH 18/31] [coq] Utils.with_control use VernacControl (adapt to coq/coq#19517 adding a control flag) --- coq/utils.ml | 55 ++++++++++++---------------------------------------- 1 file changed, 12 insertions(+), 43 deletions(-) diff --git a/coq/utils.ml b/coq/utils.ml index 0e6aa7eb..624d4352 100644 --- a/coq/utils.ml +++ b/coq/utils.ml @@ -45,47 +45,16 @@ let to_range ~lines (p : Loc.t) : Lang.Range.t = let to_orange ~lines = Option.map (to_range ~lines) -(* Separation of parsing and execution made upstream API hard to use for us - :/ *) -let pmeasure (measure, print) fn = - match measure fn () with - | Ok _ as r -> Feedback.msg_notice @@ print r - | Error (exn, _) as r -> - Feedback.msg_notice @@ print r; - Exninfo.iraise exn - -let with_fail fn = - try - fn (); - CErrors.user_err (Pp.str "The command has not failed!") - with exn when CErrors.noncritical exn -> - let exn = Exninfo.capture exn in - let msg = CErrors.iprint exn in - Feedback.msg_notice ?loc:None - Pp.(str "The command has indeed failed with message:" ++ fnl () ++ msg) - -let with_ctrl ctrl ~st ~fn = - let st = State.to_coq st in - match ctrl with - | Vernacexpr.ControlTime -> - pmeasure System.(measure_duration, fmt_transaction_result) fn - | Vernacexpr.ControlInstructions -> - pmeasure System.(count_instructions, fmt_instructions_result) fn - | Vernacexpr.ControlTimeout n -> ( - match Control.timeout (float_of_int n) fn () with - | None -> Exninfo.iraise (Exninfo.capture CErrors.Timeout) - | Some x -> x) - (* fail and succeed *) - | Vernacexpr.ControlFail -> - with_fail fn; - Vernacstate.Interp.invalidate_cache (); - Vernacstate.unfreeze_full_state st - | Vernacexpr.ControlSucceed -> - fn (); - Vernacstate.Interp.invalidate_cache (); - Vernacstate.unfreeze_full_state st - (* Unsupported by coq-lsp, maybe deprecate upstream *) - | Vernacexpr.ControlRedirect _ -> fn () - let with_control ~fn ~control ~st = - List.fold_right (fun ctrl fn () -> with_ctrl ctrl ~st ~fn) control fn () + let open VernacControl in + let control = from_syntax control in + let control, () = + under_control ~loc:None ~with_local_state:trivial_state control ~noop:() fn + in + let noop = after_last_phase ~loc:None control in + let () = + if noop then ( + Vernacstate.Interp.invalidate_cache (); + Vernacstate.unfreeze_full_state (State.to_coq st)) + in + () From 0143f792c5bce821f501f494753dd807f4f76ed3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Sep 2024 16:21:53 +0200 Subject: [PATCH 19/31] [args] [coq] Allow to set ocamlpath and findlib init file separately. This is needed for example in the JS case, likely this will help with the Coq Platform Windows Installer. --- compiler/fcc.ml | 9 +++++---- controller/coq_lsp.ml | 9 +++++---- coq/args.ml | 11 +++++++++-- coq/args.mli | 3 ++- coq/workspace.ml | 28 +++++++++++++--------------- coq/workspace.mli | 8 ++++++-- petanque/json_shell/shell.ml | 3 ++- test/compiler/basic/run.t | 26 +++++++++++++------------- test/compiler/exit_code/run.t | 2 +- test/compiler/long_file/run.t | 2 +- 10 files changed, 57 insertions(+), 44 deletions(-) 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/coq_lsp.ml b/controller/coq_lsp.ml index fe410bd2..6f2909ab 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -80,8 +80,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 (); @@ -113,6 +113,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 @@ -199,8 +200,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/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/workspace.ml b/coq/workspace.ml index 3aa2b62a..365e29d7 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -68,7 +68,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 @@ -125,7 +126,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 @@ -140,6 +142,7 @@ let mk_require_from (from, library) = let make ~cmdline ~implicit ~kind ~debug = let { CmdLine.coqcorelib ; coqlib + ; findlib_config ; ocamlpath ; args ; ml_include_path @@ -178,6 +181,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 @@ -196,12 +200,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 @@ -211,6 +211,7 @@ let findlib_init ~ml_include_path ~ocamlpath = let describe { coqlib ; coqcorelib + ; findlib_config ; ocamlpath ; kind ; vo_load_path @@ -226,14 +227,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 @@ -311,6 +308,7 @@ let dirpath_of_uri ~uri = let apply ~intern ~uri { coqlib = _ ; coqcorelib = _ + ; findlib_config ; ocamlpath ; vo_load_path ; ml_include_path @@ -324,7 +322,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 fe66abbc..4495ff07 100644 --- a/coq/workspace.mli +++ b/coq/workspace.mli @@ -46,7 +46,10 @@ end 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 @@ -78,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/petanque/json_shell/shell.ml b/petanque/json_shell/shell.ml index 3d4324b4..eb9f71b5 100644 --- a/petanque/json_shell/shell.ml +++ b/petanque/json_shell/shell.ml @@ -6,7 +6,8 @@ let init_coq ~debug = 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/test/compiler/basic/run.t b/test/compiler/basic/run.t index 7f39aa5c..53db111d 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 [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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,7 +75,7 @@ Compile both files + coqcorelib is at: [TEST_PATH] - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 @@ -96,7 +96,7 @@ Compile a dependent file without the dep being built + coqcorelib is at: [TEST_PATH] - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 @@ -133,7 +133,7 @@ Compile a file with all messages: + coqcorelib is at: [TEST_PATH] - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 @@ -144,7 +144,7 @@ Compile a file with all messages: + coqcorelib is at: [TEST_PATH] - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 @@ -174,7 +174,7 @@ Use two workspaces + coqcorelib is at: [TEST_PATH] - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 @@ -182,7 +182,7 @@ Use two workspaces + coqcorelib is at: [TEST_PATH] - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 @@ -199,7 +199,7 @@ Load the example plugin + coqcorelib is at: [TEST_PATH] - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 @@ -212,7 +212,7 @@ Load the astdump plugin + coqcorelib is at: [TEST_PATH] - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 @@ -237,7 +237,7 @@ We do the same for the goaldump plugin: + coqcorelib is at: [TEST_PATH] - Modules [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 d27c7722..1c4fd420 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 [Stdlib.Init.Prelude] will be loaded by default - 3 Coq path directory bindings in scope; 27 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 83302ca7..d7e0a468 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 [Stdlib.Init.Prelude] will be loaded by default - 2 Coq path directory bindings in scope; 27 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 From 97602487f1c56ccc95c8e2c5d0aa056f8dfbb1d3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 27 Sep 2024 00:43:19 +0200 Subject: [PATCH 20/31] [coq] [init] Allow init to tweak VM mode and warnings. Taken from #433, it is very useful there to run with a disabled VM. --- compiler/driver.ml | 3 ++- controller/coq_lsp.ml | 3 ++- coq/init.ml | 7 ++++++- coq/init.mli | 2 ++ petanque/json_shell/shell.ml | 3 ++- 5 files changed, 14 insertions(+), 4 deletions(-) diff --git a/compiler/driver.ml b/compiler/driver.ml index 08bd8e18..fb2da9de 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -2,7 +2,8 @@ let coq_init ~debug = let load_module = Dynlink.loadfile in let load_plugin = Coq.Loader.plugin_handler None in - Coq.Init.(coq_init { debug; load_module; load_plugin }) + let vm, warnings = (true, None) in + Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings }) let replace_test_path exp message = let home_re = Str.regexp (exp ^ ".*$") in diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 6f2909ab..aeaebb46 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -63,7 +63,8 @@ let concise_cb ofn = let coq_init ~debug = let load_module = Dynlink.loadfile in let load_plugin = Coq.Loader.plugin_handler None in - Coq.Init.(coq_init { debug; load_module; load_plugin }) + let vm, warnings = (true, None) in + Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings }) let exit_notification = Lsp.Base.Message.(Notification { method_ = "exit"; params = [] }) diff --git a/coq/init.ml b/coq/init.ml index b91c47c1..3eaeaf4f 100644 --- a/coq/init.ml +++ b/coq/init.ml @@ -23,6 +23,8 @@ type coq_opts = ; load_plugin : Mltop.PluginSpec.t -> unit (** callback to load findlib packages *) ; debug : bool (** Enable Coq Debug mode *) + ; vm : bool (** Enable Coq's VM *) + ; warnings : string option (** Coq's Warnings *) } let coq_lvl_to_severity (lvl : Feedback.level) = @@ -46,7 +48,7 @@ let mk_fb_handler q Feedback.{ contents; _ } = let coq_init opts = (* Core Coq initialization *) Lib.init (); - Global.set_impredicative_set false; + Global.set_VM opts.vm; Global.set_native_compiler false; if opts.debug then CDebug.set_flags "backtrace"; @@ -70,6 +72,9 @@ let coq_init opts = in Mltop.set_top ser_mltop; + (* Maybe set warnings *) + Option.iter CWarnings.set_flags opts.warnings; + (* This should go away in Coq itself *) Safe_typing.allow_delayed_constants := true; diff --git a/coq/init.mli b/coq/init.mli index a0720aea..e9822255 100644 --- a/coq/init.mli +++ b/coq/init.mli @@ -23,6 +23,8 @@ type coq_opts = ; load_plugin : Mltop.PluginSpec.t -> unit (** callback to load findlib packages *) ; debug : bool (** Enable Coq Debug mode *) + ; vm : bool (** Enable Coq's VM *) + ; warnings : string option (** Coq's Warnings *) } val coq_init : coq_opts -> State.t diff --git a/petanque/json_shell/shell.ml b/petanque/json_shell/shell.ml index eb9f71b5..a9dccdb4 100644 --- a/petanque/json_shell/shell.ml +++ b/petanque/json_shell/shell.ml @@ -1,7 +1,8 @@ let init_coq ~debug = let load_module = Dynlink.loadfile in let load_plugin = Coq.Loader.plugin_handler None in - Coq.Init.(coq_init { debug; load_module; load_plugin }) + let vm, warnings = (true, None) in + Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings }) let cmdline : Coq.Workspace.CmdLine.t = { coqlib = Coq_config.coqlib From c9c974ed1dfc01890611dbdc7dcb19142df93871 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 31 Jan 2023 16:58:27 +0100 Subject: [PATCH 21/31] [controller] [js] Initial javascript JSSO coq-lsp controller Bootstrapped and working! DONE: - interrupt support - 32bit compilation without hacks - CI + artifact TODO: minimal package manager: + try to load .vo files + hand write dune files for cma and coq-pkg for the prelude + bind jszip or some other zip lib + fetch package prelude.coq-pkg, unzip and register TODOS: - WASM - Package manager (v3) - jsCoq SDK (v2) --- CONTRIBUTING.md | 5 + Makefile | 10 + controller-js/README.md | 10 + controller-js/coq_lsp_worker.ml | 181 +++++++++++ controller-js/coq_lsp_worker.mli | 0 controller-js/dune | 59 ++++ controller-js/js_stub/coq_perf.js | 17 + controller-js/js_stub/coq_vm.js | 296 +++++++++++++++++ controller-js/js_stub/interrupt.js | 27 ++ controller-js/js_stub/marshal32.js | 4 + controller-js/js_stub/marshal64.js | 206 ++++++++++++ controller-js/js_stub/mutex.js | 93 ++++++ controller-js/js_stub/unix.js | 502 +++++++++++++++++++++++++++++ editor/code/src/browser.ts | 72 ++++- examples/documentSymbol.v | 2 +- flake.nix | 2 +- 16 files changed, 1479 insertions(+), 7 deletions(-) create mode 100644 controller-js/README.md create mode 100644 controller-js/coq_lsp_worker.ml create mode 100644 controller-js/coq_lsp_worker.mli create mode 100644 controller-js/dune create mode 100644 controller-js/js_stub/coq_perf.js create mode 100644 controller-js/js_stub/coq_vm.js create mode 100644 controller-js/js_stub/interrupt.js create mode 100644 controller-js/js_stub/marshal32.js create mode 100644 controller-js/js_stub/marshal64.js create mode 100644 controller-js/js_stub/mutex.js create mode 100644 controller-js/js_stub/unix.js diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index d49232c5..8255adc7 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -255,6 +255,11 @@ ideal would be for LSP clients to catch up and allow UTF-8 encodings (so no conversion is needed, at least for Coq), but it seems that we will take a while to get to this point. +## Worker version (and debugging tips) + +See https://github.com/ocsigen/js_of_ocaml/issues/410 for debugging +tips with `js_of_ocaml`. + ## Client guide (VS Code Extension) The VS Code extension is setup as a standard `npm` Typescript + React package diff --git a/Makefile b/Makefile index 90201847..ec08903c 100644 --- a/Makefile +++ b/Makefile @@ -47,6 +47,8 @@ build-all: coq_boot vendor/coq: $(error Submodules not initialized, please do "make submodules-init") +COQVM=yes + # We set -libdir due to a Coq bug on win32, see # https://github.com/coq/coq/pull/17289 , this can be removed once we # drop support for Coq 8.16 @@ -55,6 +57,7 @@ vendor/coq/config/coq_config.ml: vendor/coq && cd vendor/coq \ && ./configure -no-ask -prefix "$$EPATH/_build/install/default/" \ -libdir "$$EPATH/_build/install/default/lib/coq" \ + -bytecode-compiler $(COQVM) \ -native-compiler no \ && cp theories/dune.disabled theories/dune \ && cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune @@ -72,6 +75,13 @@ winconfig: && cp theories/dune.disabled theories/dune \ && cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune + +.PHONY: js +js: COQVM = no +js: coq_boot + dune build --profile=release controller-js/coq_lsp_worker.bc.cjs + mkdir -p editor/code/out/ && cp -a controller-js/coq_lsp_worker.bc.cjs editor/code/out/coq_lsp_worker.bc.js + .PHONY: coq_boot coq_boot: vendor/coq/config/coq_config.ml diff --git a/controller-js/README.md b/controller-js/README.md new file mode 100644 index 00000000..6b2ec291 --- /dev/null +++ b/controller-js/README.md @@ -0,0 +1,10 @@ +## coq-lsp Web Worker README + +This directory contains the implementation of our LSP-compliant web +worker for Coq / coq-lsp. + +As you can see the implementation is minimal, thanks to proper +abstraction of the core of the controller. + +For now it is only safe to use the worker in 32bit OCaml mode. + diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml new file mode 100644 index 00000000..91e19577 --- /dev/null +++ b/controller-js/coq_lsp_worker.ml @@ -0,0 +1,181 @@ +(* Coq JavaScript API. + * + * Copyright (C) 2016-2019 Emilio J. Gallego Arias, Mines ParisTech, Paris. + * Copyright (C) 2018-2023 Shachar Itzhaky, Technion + * Copyright (C) 2019-2023 Emilio J. Gallego Arias, INRIA + * LICENSE: GPLv3+ + * + * We provide a message-based asynchronous API for communication with + * Coq. + *) + +module U = Yojson.Safe.Util +module LSP = Lsp.Base +open Js_of_ocaml +open Controller + +let rec obj_to_json (cobj : < .. > Js.t) : Yojson.Safe.t = + let open Js in + let open Js.Unsafe in + let typeof_cobj = to_string (typeof cobj) in + match typeof_cobj with + | "string" -> `String (to_string @@ coerce cobj) + | "boolean" -> `Bool (to_bool @@ coerce cobj) + | "number" -> `Int (int_of_float @@ float_of_number @@ coerce cobj) + | _ -> + if instanceof cobj array_empty then + `List Array.(to_list @@ map obj_to_json @@ to_array @@ coerce cobj) + else if instanceof cobj Typed_array.arrayBuffer then + `String (Typed_array.String.of_arrayBuffer @@ coerce cobj) + else if instanceof cobj Typed_array.uint8Array then + `String (Typed_array.String.of_uint8Array @@ coerce cobj) + else + let json_string = Js.to_string (Json.output cobj) in + Yojson.Safe.from_string json_string + +let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t = + let open Js.Unsafe in + let ofresh j = json_to_obj (obj [||]) j in + match json with + | `Bool b -> coerce @@ Js.bool b + | `Null -> pure_js_expr "null" + | `Assoc l -> + List.iter (fun (p, js) -> set cobj p (ofresh js)) l; + cobj + | `List l -> Array.(Js.array @@ map ofresh (of_list l)) + | `Float f -> coerce @@ Js.number_of_float f + | `String s -> coerce @@ Js.string s + | `Int m -> coerce @@ Js.number_of_float (float_of_int m) + | `Intlit s -> coerce @@ Js.number_of_float (float_of_string s) + | `Tuple t -> Array.(Js.array @@ map ofresh (of_list t)) + | `Variant (_, _) -> pure_js_expr "undefined" + +let findlib_conf = "\ndestdir=\"/static/lib\"path=\"/static/lib\"" +let findlib_path = "/static/lib/findlib.conf" + +let setup_pseudo_fs () = + (* '/static' is the default working directory of jsoo *) + Sys_js.create_file ~name:findlib_path ~content:findlib_conf; + () + +let setup_std_printers () = + Sys_js.set_channel_flusher stdout (Fleche.Io.Log.trace "stdout" "%s"); + Sys_js.set_channel_flusher stderr (Fleche.Io.Log.trace "stderr" "%s"); + () + +let post_message (msg : Lsp.Base.Message.t) = + let json = Lsp.Base.Message.to_yojson msg in + let js = json_to_obj (Js.Unsafe.obj [||]) json in + Worker.post_message js + +type opaque + +external interrupt_setup : opaque (* Uint32Array *) -> unit = "interrupt_setup" + +let interrupt_is_setup = ref false + +let parse_msg msg = + if Js.instanceof msg Js.array_length then ( + let _method_ = Js.array_get msg 0 in + let handle = Js.array_get msg 1 |> Obj.magic in + interrupt_setup handle; + interrupt_is_setup := true; + Error "processed interrupt_setup") + else obj_to_json msg |> Lsp.Base.Message.of_yojson + +let on_msg msg = + match parse_msg msg with + | Error _ -> + Lsp.Io.logMessage ~lvl:Lsp.Io.Lvl.Error + ~message:"Error in JSON RPC Message Parsing" + | Ok msg -> + (* Lsp.Io.trace "interrupt_setup" (string_of_bool !interrupt_is_setup); *) + Lsp_core.enqueue_message msg + +let setTimeout cb d = Dom_html.setTimeout cb d + +module CB = Controller.Lsp_core.CB (struct + let ofn n = Lsp.Base.Message.notification n |> post_message +end) + +let rec process_queue ~state () = + match + Lsp_core.dispatch_or_resume_check ~io:CB.cb ~ofn:post_message ~state + with + | None -> + Fleche.Io.Log.trace "proccess queue" "ended"; + () + | Some (Yield state) -> ignore (setTimeout (process_queue ~state) 0.1) + (* We need to yield so [on_msg] above has the chance to run and add the + command(s) to the queue. *) + | Some (Cont state) -> ignore (setTimeout (process_queue ~state) 0.) + +let on_init ~io ~root_state ~cmdline ~debug msg = + match parse_msg msg with + | Error _ -> () + | Ok msg -> ( + match + Lsp_core.lsp_init_process ~ofn:post_message ~io ~cmdline ~debug msg + with + | Lsp_core.Init_effect.Exit -> (* XXX: bind to worker.close () *) () + | Lsp_core.Init_effect.Loop -> () + | Lsp_core.Init_effect.Success workspaces -> + Worker.set_onmessage on_msg; + let default_workspace = Coq.Workspace.default ~debug ~cmdline in + let state = + { Lsp_core.State.root_state; cmdline; workspaces; default_workspace } + in + ignore (setTimeout (process_queue ~state) 0.1)) + +let coq_init ~debug = + let load_module = Dynlink.loadfile in + let load_plugin = Coq.Loader.plugin_handler None in + (* XXX: Fixme at some point? *) + let vm, warnings = (false, Some "-vm-compute-disabled") in + Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings }) + +external coq_vm_trap : unit -> unit = "coq_vm_trap" + +(* This code is executed on Worker initialization *) +let main () = + (* This is needed if dynlink is enabled in 4.03.0 *) + Sys.interactive := false; + + Coq.Limits.(select Coq); + Coq.Limits.start (); + + setup_pseudo_fs (); + setup_std_printers (); + + (* setup_interp (); *) + coq_vm_trap (); + + Lsp.Io.set_log_fn (fun n -> Lsp.Base.Message.notification n |> post_message); + let io = CB.cb in + Fleche.Io.CallBack.set io; + + let stdlib = + let unix_path = "/static/coq/theories/" in + let coq_path = Names.(DirPath.make [ Id.of_string "Coq" ]) in + Loadpath. + { unix_path; coq_path; implicit = true; has_ml = false; recursive = true } + in + + let cmdline = + Coq.Workspace.CmdLine. + { coqlib = "/static/coqlib" + ; coqcorelib = "/static/lib/coq-core" + ; findlib_config = Some findlib_path + ; ocamlpath = [] + ; vo_load_path = [ stdlib ] + ; ml_include_path = [] + ; require_libraries = [] + ; args = [ "-noinit" ] + } + in + let debug = true in + let root_state = coq_init ~debug in + Worker.set_onmessage (on_init ~io ~root_state ~cmdline ~debug); + () + +let () = main () diff --git a/controller-js/coq_lsp_worker.mli b/controller-js/coq_lsp_worker.mli new file mode 100644 index 00000000..e69de29b diff --git a/controller-js/dune b/controller-js/dune new file mode 100644 index 00000000..af7826f5 --- /dev/null +++ b/controller-js/dune @@ -0,0 +1,59 @@ +(executable + (name coq_lsp_worker) + (modes js) + (preprocess + (pps js_of_ocaml-ppx)) + (js_of_ocaml + (javascript_files + js_stub/mutex.js + js_stub/unix.js + js_stub/coq_vm.js + js_stub/coq_perf.js + js_stub/interrupt.js + marshal-arch.js) + (flags + :standard + --dynlink + +dynlink.js + ; (:include .extraflags) + ; +toplevel.js + ; --enable + ; with-js-error + ; --enable + ; debuginfo + ; --no-inline + ; --debug-info + ; --source-map + ; no coq-fs yet + ; --file=coq-fs + --setenv + PATH=/bin)) + (link_flags -linkall -no-check-prims) + ; The old makefile set: -noautolink -no-check-prims + (libraries zarith_stubs_js yojson controller)) + +(rule + (target coq_lsp_worker.bc.cjs) + (mode promote) + (action + (copy coq_lsp_worker.bc.js coq_lsp_worker.bc.cjs))) + +(rule + (targets marshal-arch.js) + ; This is to inject the dep of a FS on the executable if we want. + ; (deps coq-fs) + (action + (copy js_stub/marshal%{ocaml-config:word_size}.js %{targets}))) + +; Set debug flags if JSCOQ_DEBUG environment variable is set. +; (ugly, but there are no conditional expressions in Dune) + +(rule + (targets .extraflags) + (deps + (env_var JSCOQ_DEBUG)) + (action + (with-stdout-to + %{targets} + (bash + "echo '(' ${JSCOQ_DEBUG+ --pretty --noinline --disable shortvar --debug-info} ')'")))) diff --git a/controller-js/js_stub/coq_perf.js b/controller-js/js_stub/coq_perf.js new file mode 100644 index 00000000..41ba8c4c --- /dev/null +++ b/controller-js/js_stub/coq_perf.js @@ -0,0 +1,17 @@ +//Provides: CAML_init +function CAML_init() { + return; +} + +//Provides: CAML_peek +//Requires: caml_int64_of_int32 +function CAML_peek() { + return caml_int64_of_int32(0); +} + + +//Provides: CAML_drop +function CAML_drop() { + return; +} + diff --git a/controller-js/js_stub/coq_vm.js b/controller-js/js_stub/coq_vm.js new file mode 100644 index 00000000..cf86e905 --- /dev/null +++ b/controller-js/js_stub/coq_vm.js @@ -0,0 +1,296 @@ +// Provides: vm_ll +function vm_ll(s, args) { + if (vm_ll.log) joo_global_object.console.warn(s, args); + if (vm_ll.trap) throw new Error("vm trap: '"+ s + "' not implemented"); +} + +vm_ll.log = false; // whether to log calls +vm_ll.trap = false; // whether to halt on calls + +// Provides: init_coq_vm +// Requires: vm_ll +function init_coq_vm() { + vm_ll('init_coq_vm', arguments); + return; +} + +// EG: Coq VM's code is evil and performs static initialization... the +// best option would be to disable the VM code entirely as before. + +// Provides: coq_vm_trap +// Requires: vm_ll +function coq_vm_trap() { // will cause future calls to vm code to fault + vm_ll.log = vm_ll.trap = true; // (called after initialization) +} + +// Provides: accumulate_code +// Requires: vm_ll +function accumulate_code() { + // EG: Where the hell is that called from + vm_ll('accumulate_code', arguments); + return []; +} + +// Provides: coq_pushpop +// Requires: vm_ll +function coq_pushpop() { + vm_ll('coq_pushpop', arguments); + return []; +} + +// Provides: coq_closure_arity +// Requires: vm_ll +function coq_closure_arity() { + vm_ll('coq_closure_arity', arguments); + return []; +} + +// Provides: coq_eval_tcode +// Requires: vm_ll +function coq_eval_tcode() { + vm_ll('coq_eval_tcode', arguments); + return []; +} + +// Provides: coq_int_tcode +// Requires: vm_ll +function coq_int_tcode() { + vm_ll('coq_int_tcode', arguments); + return []; +} + +// Provides: coq_interprete_ml +// Requires: vm_ll +function coq_interprete_ml() { + vm_ll('coq_interprete_ml', arguments); + return []; +} + +// Provides: coq_is_accumulate_code +// Requires: vm_ll +function coq_is_accumulate_code() { + vm_ll('coq_is_accumulate_code', arguments); + return []; +} + +// Provides: coq_kind_of_closure +// Requires: vm_ll +function coq_kind_of_closure() { + vm_ll('coq_kind_of_closure', arguments); + return []; +} + +// Provides: coq_makeaccu +// Requires: vm_ll +function coq_makeaccu() { + vm_ll('coq_makeaccu', arguments); + return []; +} + +// Provides: coq_offset +// Requires: vm_ll +function coq_offset() { + vm_ll('coq_offset', arguments); + return []; +} + +// Provides: coq_offset_closure +// Requires: vm_ll +function coq_offset_closure() { + vm_ll('coq_offset_closure', arguments); + return []; +} + +// Provides: coq_offset_tcode +// Requires: vm_ll +function coq_offset_tcode() { + vm_ll('coq_offset_tcode', arguments); + return []; +} + +// Provides: coq_push_arguments +// Requires: vm_ll +function coq_push_arguments() { + vm_ll('coq_push_arguments', arguments); + return []; +} + +// Provides: coq_push_ra +// Requires: vm_ll +function coq_push_ra() { + vm_ll('coq_push_ra', arguments); + return []; +} + +// Provides: coq_push_val +// Requires: vm_ll +function coq_push_val() { + vm_ll('coq_push_val', arguments); + return []; +} + +// Provides: coq_push_vstack +// Requires: vm_ll +function coq_push_vstack() { + vm_ll('coq_push_vstack', arguments); + return []; +} + +// Provides: coq_set_transp_value +// Requires: vm_ll +function coq_set_transp_value() { + vm_ll('coq_set_transp_value', arguments); + return []; +} + +// Provides: coq_set_bytecode_field +// Requires: vm_ll +function coq_set_bytecode_field() { + vm_ll('coq_set_bytecode_field', arguments); + return [0]; +} + +// Provides: coq_tcode_of_code +// Requires: vm_ll +function coq_tcode_of_code() { + vm_ll('coq_tcode_of_code', arguments); + return []; +} + +// Provides: coq_accumulate +// Requires: vm_ll +function coq_accumulate() { + // This is called on init, so let's be more lenient + // vm_ll('coq_accumulate', arguments); + return []; +} + +// Provides: coq_obj_set_tag +// Requires: vm_ll +function coq_obj_set_tag() { + vm_ll('coq_obj_set_tag', arguments); + return []; +} + +// Provides: coq_uint63_to_float_byte +// Requires: vm_ll +function coq_uint63_to_float_byte() { + // First element of the array is the length! + vm_ll('coq_uint63_to_float_byte', arguments); + return [0]; +} + +// Provides: get_coq_atom_tbl +// Requires: vm_ll +function get_coq_atom_tbl() { + // First element of the array is the length! + vm_ll('get_coq_atom_tbl', arguments); + return [0]; +} + +// Provides: get_coq_global_data +// Requires: vm_ll +function get_coq_global_data() { + vm_ll('get_coq_global_data', arguments); + return []; +} + +// Provides: get_coq_transp_value +// Requires: vm_ll +function get_coq_transp_value() { + vm_ll('get_coq_transp_value', arguments); + return []; +} + +// Provides: realloc_coq_atom_tbl +// Requires: vm_ll +function realloc_coq_atom_tbl() { + vm_ll('realloc_coq_atom_tbl', arguments); + return; +} + +// Provides: realloc_coq_global_data +// Requires: vm_ll +function realloc_coq_global_data() { + vm_ll('realloc_coq_global_data', arguments); + return; +} + +// Provides: coq_interprete_byte +// Requires: vm_ll +function coq_interprete_byte() { vm_ll('coq_interprete_byte', arguments); } +// Provides: coq_set_drawinstr +// Requires: vm_ll +function coq_set_drawinstr() { vm_ll('coq_set_drawinstr', arguments); } +// Provides: coq_tcode_array +// Requires: vm_ll +function coq_tcode_array() { vm_ll('coq_tcode_array', arguments); } + +// Provides: coq_fadd_byte +function coq_fadd_byte(r1, r2) { + return r1 + r2; +} + +// Provides: coq_fsub_byte +function coq_fsub_byte(r1, r2) { + return r1 - r2; +} + +// Provides: coq_fmul_byte +function coq_fmul_byte(r1, r2) { + return r1 * r2; +} + +// Provides: coq_fdiv_byte +function coq_fdiv_byte(r1, r2) { + return r1 / r2; +} + +// Provides: coq_fsqrt_byte +// Requires: vm_ll +function coq_fsqrt_byte() { + vm_ll('coq_fsqrt_byte', arguments); + return; +} + +// Provides: coq_is_double +// Requires: vm_ll + function coq_is_double() { + vm_ll('coq_is_double', arguments); + return; +} + +// Provides: coq_next_down_byte +// Requires: vm_ll + function coq_next_down_byte() { + vm_ll('coq_next_down_byte', arguments); + return; +} + +// Provides: coq_next_up_byte +// Requires: vm_ll + function coq_next_up_byte() { + vm_ll('coq_next_up_byte', arguments); + return; +} + +// Provides: coq_current_fix +// Requires: vm_ll +function coq_current_fix() { + vm_ll('coq_current_fix', arguments); + return []; +} + +// Provides: coq_last_fix +// Requires: vm_ll +function coq_last_fix() { + vm_ll('coq_last_fix', arguments); + return []; +} + +// Provides: coq_shift_fix +// Requires: vm_ll +function coq_shift_fix() { + vm_ll('coq_shift_fix', arguments); + return []; +} diff --git a/controller-js/js_stub/interrupt.js b/controller-js/js_stub/interrupt.js new file mode 100644 index 00000000..6b14c1ce --- /dev/null +++ b/controller-js/js_stub/interrupt.js @@ -0,0 +1,27 @@ +// Provides: interrupt_setup +function interrupt_setup(shmem) { + var Int32Array = joo_global_object.Int32Array, + SharedArrayBuffer = joo_global_object.SharedArrayBuffer; + + if (Int32Array && SharedArrayBuffer) { + shmem = shmem || new Int32Array(new SharedArrayBuffer(4)); + interrupt_setup.vec = shmem; + interrupt_setup.checkpoint = 0; + return shmem; + } +} + +// Provides: interrupt_pending +// Requires: interrupt_setup +function interrupt_pending() { + var Atomics = joo_global_object.Atomics; + + if (Atomics && interrupt_setup.vec) { + var ld = Atomics.load(interrupt_setup.vec, 0); + if (ld > interrupt_setup.checkpoint) { + interrupt_setup.checkpoint = ld; + return true; + } + } + return false; +} diff --git a/controller-js/js_stub/marshal32.js b/controller-js/js_stub/marshal32.js new file mode 100644 index 00000000..93a769d0 --- /dev/null +++ b/controller-js/js_stub/marshal32.js @@ -0,0 +1,4 @@ +/* (Blank) + * For 64-bit compilation, marshal64.js is selected. + * For 32-bit compilation, nothing further is required. + */ diff --git a/controller-js/js_stub/marshal64.js b/controller-js/js_stub/marshal64.js new file mode 100644 index 00000000..90b368a1 --- /dev/null +++ b/controller-js/js_stub/marshal64.js @@ -0,0 +1,206 @@ +/** + * This is a hack to circumvent a discrepancy arising when Coq is compiled + * as a 64-bit library and then passed through js_of_ocaml, resulting in + * 32-bit JavaScript code. + * As a whole, the Coq codebase makes little use of integer arithmetic and + * does not create huge arrays of more than 2^31-1 elements. An exception + * to this is hash values calculated for storing various Coq types in maps + * and hash tables and to speed up comparisons. + * Though the values themselves are meaningless, they are unfortunately + * stored in .vo files through use of the Marshal module, and lead to files + * that cannot be read back via 32-bit code. + * + * As 32-bit support is declining (e.g. the following issue relating to + * macOS builds of OCaml: https://github.com/ocaml/ocaml/issues/6900), + * there may be no escape from building 64-bit Coq, both core and libraries. + * This requires a patch to jsoo's Marshal primitive that will not throw + * when encountering a 64-bit integer. The version below truncates such + * values. It may be extremely fragile, but so far, seems to work. + */ + + +//Provides: caml_input_value_from_reader mutable +//Requires: caml_failwith +//Requires: caml_float_of_bytes, caml_custom_ops + +/*** !!! This overrides the implementation from js_of_ocaml !!! ***/ + +function caml_input_value_from_reader(reader, ofs) { + var _magic = reader.read32u () + var _block_len = reader.read32u (); + var num_objects = reader.read32u (); + var _size_32 = reader.read32u (); + var _size_64 = reader.read32u (); + var stack = []; + var intern_obj_table = (num_objects > 0)?[]:null; + var obj_counter = 0; + function intern_rec () { + var code = reader.read8u (); + if (code >= 0x40 /*cst.PREFIX_SMALL_INT*/) { + if (code >= 0x80 /*cst.PREFIX_SMALL_BLOCK*/) { + var tag = code & 0xF; + var size = (code >> 4) & 0x7; + var v = [tag]; + if (size == 0) return v; + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + stack.push(v, size); + return v; + } else + return (code & 0x3F); + } else { + if (code >= 0x20/*cst.PREFIX_SMALL_STRING */) { + var len = code & 0x1F; + var v = reader.readstr (len); + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + } else { + switch(code) { + case 0x00: //cst.CODE_INT8: + return reader.read8s (); + case 0x01: //cst.CODE_INT16: + return reader.read16s (); + case 0x02: //cst.CODE_INT32: + return reader.read32s (); + case 0x03: //cst.CODE_INT64: + reader.read32s (); return reader.read32s (); // <------------ HERE + //caml_failwith("input_value: integer too large"); // (ouch) + break; + case 0x04: //cst.CODE_SHARED8: + var offset = reader.read8u (); + return intern_obj_table[obj_counter - offset]; + case 0x05: //cst.CODE_SHARED16: + var offset = reader.read16u (); + return intern_obj_table[obj_counter - offset]; + case 0x06: //cst.CODE_SHARED32: + var offset = reader.read32u (); + return intern_obj_table[obj_counter - offset]; + case 0x08: //cst.CODE_BLOCK32: + var header = reader.read32u (); + var tag = header & 0xFF; + var size = header >> 10; + var v = [tag]; + if (size == 0) return v; + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + stack.push(v, size); + return v; + case 0x13: //cst.CODE_BLOCK64: + caml_failwith ("input_value: data block too large"); + break; + case 0x09: //cst.CODE_STRING8: + var len = reader.read8u(); + var v = reader.readstr (len); + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + case 0x0A: //cst.CODE_STRING32: + var len = reader.read32u(); + var v = reader.readstr (len); + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + case 0x0C: //cst.CODE_DOUBLE_LITTLE: + var t = new Array(8);; + for (var i = 0;i < 8;i++) t[7 - i] = reader.read8u (); + var v = caml_float_of_bytes (t); + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + case 0x0B: //cst.CODE_DOUBLE_BIG: + var t = new Array(8);; + for (var i = 0;i < 8;i++) t[i] = reader.read8u (); + var v = caml_float_of_bytes (t); + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + case 0x0E: //cst.CODE_DOUBLE_ARRAY8_LITTLE: + var len = reader.read8u(); + var v = new Array(len+1); + v[0] = 254; + var t = new Array(8);; + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + for (var i = 1;i <= len;i++) { + for (var j = 0;j < 8;j++) t[7 - j] = reader.read8u(); + v[i] = caml_float_of_bytes (t); + } + return v; + case 0x0D: //cst.CODE_DOUBLE_ARRAY8_BIG: + var len = reader.read8u(); + var v = new Array(len+1); + v[0] = 254; + var t = new Array(8);; + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + for (var i = 1;i <= len;i++) { + for (var j = 0;j < 8;j++) t[j] = reader.read8u(); + v [i] = caml_float_of_bytes (t); + } + return v; + case 0x07: //cst.CODE_DOUBLE_ARRAY32_LITTLE: + var len = reader.read32u(); + var v = new Array(len+1); + v[0] = 254; + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + var t = new Array(8);; + for (var i = 1;i <= len;i++) { + for (var j = 0;j < 8;j++) t[7 - j] = reader.read8u(); + v[i] = caml_float_of_bytes (t); + } + return v; + case 0x0F: //cst.CODE_DOUBLE_ARRAY32_BIG: + var len = reader.read32u(); + var v = new Array(len+1); + v[0] = 254; + var t = new Array(8);; + for (var i = 1;i <= len;i++) { + for (var j = 0;j < 8;j++) t[j] = reader.read8u(); + v [i] = caml_float_of_bytes (t); + } + return v; + case 0x10: //cst.CODE_CODEPOINTER: + case 0x11: //cst.CODE_INFIXPOINTER: + caml_failwith ("input_value: code pointer"); + break; + case 0x12: //cst.CODE_CUSTOM: + case 0x18: //cst.CODE_CUSTOM_LEN: + case 0x19: //cst.CODE_CUSTOM_FIXED: + var c, s = ""; + while ((c = reader.read8u ()) != 0) s += String.fromCharCode (c); + var ops = caml_custom_ops[s]; + var expected_size; + if(!ops) + caml_failwith("input_value: unknown custom block identifier"); + switch(code){ + case 0x12: // cst.CODE_CUSTOM (deprecated) + break; + case 0x19: // cst.CODE_CUSTOM_FIXED + if(!ops.fixed_length) + caml_failwith("input_value: expected a fixed-size custom block"); + expected_size = ops.fixed_length; + break; + case 0x18: // cst.CODE_CUSTOM_LEN + expected_size = reader.read32u (); + // Skip size64 + reader.read32s(); reader.read32s(); + break; + } + var old_pos = reader.i; + var size = [0]; + var v = ops.deserialize(reader, size); + if(expected_size != undefined){ + if(expected_size != size[0]) + caml_failwith("input_value: incorrect length of serialized custom block"); + } + if (intern_obj_table) intern_obj_table[obj_counter++] = v; + return v; + default: + caml_failwith ("input_value: ill-formed message"); + } + } + } + } + var res = intern_rec (); + while (stack.length > 0) { + var size = stack.pop(); + var v = stack.pop(); + var d = v.length; + if (d < size) stack.push(v, size); + v[d] = intern_rec (); + } + if (typeof ofs!="number") ofs[0] = reader.i; + return res; +} diff --git a/controller-js/js_stub/mutex.js b/controller-js/js_stub/mutex.js new file mode 100644 index 00000000..d4a9acb6 --- /dev/null +++ b/controller-js/js_stub/mutex.js @@ -0,0 +1,93 @@ +// Whether to log. +var v_log = false; +function ll(s) { if (v_log) console.log(s); } + +//Provides: caml_condition_broadcast +function caml_condition_broadcast() { + // ll("***caml_condition_broadcast"); + return 0; +} + +//Provides: caml_condition_new +function caml_condition_new() { + // ll("***caml_condition_new"); + return 0; +} + +//Provides: caml_condition_signal +function caml_condition_signal() { + // ll("***caml_condition_signal"); + return 0; +} + +//Provides: caml_condition_wait +function caml_condition_wait() { + // ll("***caml_condition_wait"); + return 0; +} + +//Provides: caml_thread_initialize +function caml_thread_initialize() { + // ll("***caml_thread_initialize"); + return 0; +} + +//Provides: caml_thread_new +function caml_thread_new() { + // ll("***caml_thread_new"); + return 0; +} + +//Provides: caml_thread_self +function caml_thread_self() { + // ll("***caml_thread_self"); + return [0,0]; +} + +//Provides: caml_thread_uncaught_exception +function caml_thread_uncaught_exception() { + // ll("***caml_thread_uncaught_exception"); + return 0; +} + +//Provides: caml_thread_yield +function caml_thread_yield() { + // ll("***caml_thread_yield"); + return 0; +} + +//Provides: caml_mutex_lock +function caml_mutex_lock() { + // ll("***caml_mutex_lock"); + return 0; +} + +//Provides: caml_mutex_new +function caml_mutex_new() { + // ll("***caml_mutex_new"); + return 0; +} + +//Provides: caml_mutex_unlock +function caml_mutex_unlock() { + // ll("***caml_mutex_unlock"); + return 0; +} + +//Provides: caml_thread_cleanup +function caml_thread_cleanup() { + // ll("***caml_thread_cleanup"); + return 0; +} + +//Provides: caml_thread_exit +function caml_thread_exit() { + // ll("***caml_thread_exit"); + return 0; +} + +//Provides: caml_thread_id +function caml_thread_id() { + // ll("***caml_thread_id"); + return 0; +} diff --git a/controller-js/js_stub/unix.js b/controller-js/js_stub/unix.js new file mode 100644 index 00000000..a606d9bb --- /dev/null +++ b/controller-js/js_stub/unix.js @@ -0,0 +1,502 @@ +//Provides: unix_ll +function unix_ll(s, args) { + if (unix_ll.log) joo_global_object.console.warn(s, args); + if (unix_ll.trap) throw new Error("unix trap: '"+ s + "' not implemented"); +} +unix_ll.log = true; // whether to log calls +unix_ll.trap = false; // whether to halt on calls + +//Provides: caml_raise_unix_error +//Requires: caml_named_value, caml_raise_with_arg, caml_new_string +function caml_raise_unix_error(msg) { + var tag = caml_named_value("Unix.Unix_error"); + // var util = require('util'); + // console.log(util.inspect(chan, {showHidden: false, depth: null})); + caml_raise_with_arg (tag, caml_new_string (msg)); +} + +//Provides: unix_access +//Requires: unix_ll +function unix_access() { + unix_ll("unix_access", arguments); + return 0; +} + +//Provides: unix_alarm +//Requires: unix_ll +function unix_alarm() { + unix_ll("unix_alarm", arguments); + return 0; +} + +//Provides: unix_bind +//Requires: unix_ll +function unix_bind() { + unix_ll("unix_bind", arguments); + return 0; +} + +//Provides: unix_close +//Requires: unix_ll +function unix_close() { + unix_ll("unix_close", arguments); + return 0; +} + +//Provides: unix_connect +//Requires: unix_ll +function unix_connect() { + unix_ll("unix_connect", arguments); + return 0; +} + +//Provides: unix_dup +//Requires: unix_ll +function unix_dup() { + unix_ll("unix_dup", arguments); + return 0; +} + +//Provides: unix_dup2 +//Requires: unix_ll +function unix_dup2() { + unix_ll("unix_dup2", arguments); + return 0; +} + +//Provides: unix_environment +//Requires: unix_ll +function unix_environment() { + unix_ll("unix_environment", arguments); + return 0; +} + +//Provides: unix_error_message +//Requires: unix_ll +function unix_error_message() { + unix_ll("unix_error_message", arguments); + return 0; +} + +//Provides: unix_execve +//Requires: unix_ll +function unix_execve() { + unix_ll("unix_execve", arguments); + return 0; +} + +//Provides: unix_execvp +//Requires: unix_ll +function unix_execvp() { + unix_ll("unix_execvp", arguments); + return 0; +} + +//Provides: unix_execvpe +//Requires: unix_ll +function unix_execvpe() { + unix_ll("unix_execvpe", arguments); + return 0; +} + +//Provides: unix_getcwd +//Requires: unix_ll +function unix_getcwd() { + unix_ll("unix_getcwd", arguments); + return 0; +} + +//Provides: unix_fork +//Requires: unix_ll +function unix_fork() { + unix_ll("unix_fork", arguments); + return 0; +} + +//Provides: unix_getpid +//Requires: unix_ll +function unix_getpid() { + unix_ll("unix_getpid", arguments); + return 0; +} + +//Provides: unix_getpwnam +//Requires: unix_ll +function unix_getpwnam() { + unix_ll("unix_getpwnam", arguments); + return 0; +} + +//Provides: unix_getsockname +//Requires: unix_ll +function unix_getsockname() { + unix_ll("unix_getsockname", arguments); + return 0; +} + +//Provides: unix_kill +//Requires: unix_ll +function unix_kill() { + unix_ll("unix_kill", arguments); + return 0; +} + +//Provides: unix_listen +//Requires: unix_ll +function unix_listen() { + unix_ll("unix_listen", arguments); + return 0; +} + +//Provides: unix_pipe +//Requires: unix_ll +function unix_pipe() { + unix_ll("unix_pipe", arguments); + return 0; +} + +//Provides: unix_read +//Requires: unix_ll +function unix_read() { + unix_ll("unix_read", arguments); + return 0; +} + +//Provides: unix_opendir +//Requires: unix_ll +function unix_opendir(dir) { + unix_ll("unix_opendir", arguments); + + // caml_raise_unix_error("opendir", arguments); + return []; +} + +//Provides: unix_readdir +//Requires: unix_ll, caml_raise_constant, caml_global_data +function unix_readdir(dir) { + unix_ll("unix_readdir", arguments); + + // caml_raise_unix_error("readdir", arguments); + caml_raise_constant(caml_global_data.End_of_file); + return []; +} + +//Provides: unix_closedir +//Requires: unix_ll +function unix_closedir() { + unix_ll("unix_closedir", arguments); + return []; +} + +//Provides: unix_select +//Requires: unix_ll +function unix_select() { + unix_ll("unix_select", arguments); + return 0; +} + +//Provides: unix_set_close_on_exec +//Requires: unix_ll +function unix_set_close_on_exec() { + unix_ll("unix_set_close_on_exec", arguments); + return 0; +} + +//Provides: unix_set_nonblock +//Requires: unix_ll +function unix_set_nonblock() { + unix_ll("unix_set_nonblock", arguments); + return 0; +} + +//Provides: unix_sleep +//Requires: unix_ll +function unix_sleep() { + unix_ll("unix_sleep", arguments); + return 0; +} + +//Provides: unix_socket +//Requires: unix_ll +function unix_socket() { + unix_ll("unix_socket", arguments); + return 0; +} + +//Provides: unix_string_of_inet_addr +//Requires: unix_ll +function unix_string_of_inet_addr() { + unix_ll("unix_string_of_inet_addr", arguments); + return 0; +} + +//Provides: unix_times +//Requires: unix_ll +function unix_times() { + unix_ll("unix_times", arguments); + return 0; +} + +//Provides: unix_wait +//Requires: unix_ll +function unix_wait() { + unix_ll("unix_wait", arguments); + return 0; +} + +//Provides: unix_waitpid +//Requires: unix_ll +function unix_waitpid() { + unix_ll("unix_waitpid", arguments); + return 0; +} + +// Provides: unix_accept +// Requires: unix_ll +function unix_accept() { unix_ll("unix_accept", arguments); } +// Provides: unix_chdir +// Requires: unix_ll +function unix_chdir() { unix_ll("unix_chdir", arguments); } +// Provides: unix_chmod +// Requires: unix_ll +function unix_chmod() { unix_ll("unix_chmod", arguments); } +// Provides: unix_chown +// Requires: unix_ll +function unix_chown() { unix_ll("unix_chown", arguments); } +// Provides: unix_chroot +// Requires: unix_ll +function unix_chroot() { unix_ll("unix_chroot", arguments); } +// Provides: unix_clear_close_on_exec +// Requires: unix_ll +function unix_clear_close_on_exec() { unix_ll("unix_clear_close_on_exec", arguments); } +// Provides: unix_clear_nonblock +// Requires: unix_ll +function unix_clear_nonblock() { unix_ll("unix_clear_nonblock", arguments); } +// Provides: unix_environment_unsafe +// Requires: unix_ll +function unix_environment_unsafe() { unix_ll("unix_environment_unsafe", arguments); } +// Provides: unix_execv +// Requires: unix_ll +function unix_execv() { unix_ll("unix_execv", arguments); } +// Provides: unix_fchmod +// Requires: unix_ll +function unix_fchmod() { unix_ll("unix_fchmod", arguments); } +// Provides: unix_fchown +// Requires: unix_ll +function unix_fchown() { unix_ll("unix_fchown", arguments); } +// Provides: unix_fstat +// Requires: unix_ll +function unix_fstat() { unix_ll("unix_fstat", arguments); } +// Provides: unix_fstat_64 +// Requires: unix_ll +function unix_fstat_64() { unix_ll("unix_fstat_64", arguments); } +// Provides: unix_ftruncate +// Requires: unix_ll +function unix_ftruncate() { unix_ll("unix_ftruncate", arguments); } +// Provides: unix_ftruncate_64 +// Requires: unix_ll +function unix_ftruncate_64() { unix_ll("unix_ftruncate_64", arguments); } +// Provides: unix_getaddrinfo +// Requires: unix_ll +function unix_getaddrinfo() { unix_ll("unix_getaddrinfo", arguments); } +// Provides: unix_getegid +// Requires: unix_ll +function unix_getegid() { unix_ll("unix_getegid", arguments); } +// Provides: unix_geteuid +// Requires: unix_ll +function unix_geteuid() { unix_ll("unix_geteuid", arguments); } +// Provides: unix_getgid +// Requires: unix_ll +function unix_getgid() { unix_ll("unix_getgid", arguments); } +// Provides: unix_getgrgid +// Requires: unix_ll +function unix_getgrgid() { unix_ll("unix_getgrgid", arguments); } +// Provides: unix_getgrnam +// Requires: unix_ll +function unix_getgrnam() { unix_ll("unix_getgrnam", arguments); } +// Provides: unix_getgroups +// Requires: unix_ll +function unix_getgroups() { unix_ll("unix_getgroups", arguments); } +// Provides: unix_gethostbyaddr +// Requires: unix_ll +function unix_gethostbyaddr() { unix_ll("unix_gethostbyaddr", arguments); } +// Provides: unix_gethostbyname +// Requires: unix_ll +function unix_gethostbyname() { unix_ll("unix_gethostbyname", arguments); } +// Provides: unix_gethostname +// Requires: unix_ll +function unix_gethostname() { unix_ll("unix_gethostname", arguments); } +// Provides: unix_getitimer +// Requires: unix_ll +function unix_getitimer() { unix_ll("unix_getitimer", arguments); } +// Provides: unix_getlogin +// Requires: unix_ll +function unix_getlogin() { unix_ll("unix_getlogin", arguments); } +// Provides: unix_getnameinfo +// Requires: unix_ll +function unix_getnameinfo() { unix_ll("unix_getnameinfo", arguments); } +// Provides: unix_getpeername +// Requires: unix_ll +function unix_getpeername() { unix_ll("unix_getpeername", arguments); } +// Provides: unix_getppid +// Requires: unix_ll +function unix_getppid() { unix_ll("unix_getppid", arguments); } +// Provides: unix_getprotobyname +// Requires: unix_ll +function unix_getprotobyname() { unix_ll("unix_getprotobyname", arguments); } +// Provides: unix_getprotobynumber +// Requires: unix_ll +function unix_getprotobynumber() { unix_ll("unix_getprotobynumber", arguments); } +// Provides: unix_getservbyname +// Requires: unix_ll +function unix_getservbyname() { unix_ll("unix_getservbyname", arguments); } +// Provides: unix_getservbyport +// Requires: unix_ll +function unix_getservbyport() { unix_ll("unix_getservbyport", arguments); } +// Provides: unix_getsockopt +// Requires: unix_ll +function unix_getsockopt() { unix_ll("unix_getsockopt", arguments); } +// Provides: unix_initgroups +// Requires: unix_ll +function unix_initgroups() { unix_ll("unix_initgroups", arguments); } +// Provides: unix_link +// Requires: unix_ll +function unix_link() { unix_ll("unix_link", arguments); } +// Provides: unix_lockf +// Requires: unix_ll +function unix_lockf() { unix_ll("unix_lockf", arguments); } +// Provides: unix_lseek +// Requires: unix_ll +function unix_lseek() { unix_ll("unix_lseek", arguments); } +// Provides: unix_lseek_64 +// Requires: unix_ll +function unix_lseek_64() { unix_ll("unix_lseek_64", arguments); } +// Provides: unix_mkfifo +// Requires: unix_ll +function unix_mkfifo() { unix_ll("unix_mkfifo", arguments); } +// Provides: unix_nice +// Requires: unix_ll +function unix_nice() { unix_ll("unix_nice", arguments); } +// Provides: unix_open +// Requires: unix_ll +function unix_open() { unix_ll("unix_open", arguments); } +// Provides: unix_putenv +// Requires: unix_ll +function unix_putenv() { unix_ll("unix_putenv", arguments); } +// Provides: unix_recv +// Requires: unix_ll +function unix_recv() { unix_ll("unix_recv", arguments); } +// Provides: unix_recvfrom +// Requires: unix_ll +function unix_recvfrom() { unix_ll("unix_recvfrom", arguments); } +// Provides: unix_rename +// Requires: unix_ll +function unix_rename() { unix_ll("unix_rename", arguments); } +// Provides: unix_rewinddir +// Requires: unix_ll +function unix_rewinddir() { unix_ll("unix_rewinddir", arguments); } +// Provides: unix_send +// Requires: unix_ll +function unix_send() { unix_ll("unix_send", arguments); } +// Provides: unix_sendto +// Requires: unix_ll +function unix_sendto() { unix_ll("unix_sendto", arguments); } +// Provides: unix_setgid +// Requires: unix_ll +function unix_setgid() { unix_ll("unix_setgid", arguments); } +// Provides: unix_setgroups +// Requires: unix_ll +function unix_setgroups() { unix_ll("unix_setgroups", arguments); } +// Provides: unix_setitimer +// Requires: unix_ll +function unix_setitimer() { unix_ll("unix_setitimer", arguments); } +// Provides: unix_setsid +// Requires: unix_ll +function unix_setsid() { unix_ll("unix_setsid", arguments); } +// Provides: unix_setsockopt +// Requires: unix_ll +function unix_setsockopt() { unix_ll("unix_setsockopt", arguments); } +// Provides: unix_setuid +// Requires: unix_ll +function unix_setuid() { unix_ll("unix_setuid", arguments); } +// Provides: unix_shutdown +// Requires: unix_ll +function unix_shutdown() { unix_ll("unix_shutdown", arguments); } +// Provides: unix_sigpending +// Requires: unix_ll +function unix_sigpending() { unix_ll("unix_sigpending", arguments); } +// Provides: unix_sigprocmask +// Requires: unix_ll +function unix_sigprocmask() { unix_ll("unix_sigprocmask", arguments); } +// Provides: unix_sigsuspend +// Requires: unix_ll +function unix_sigsuspend() { unix_ll("unix_sigsuspend", arguments); } +// Provides: unix_single_write +// Requires: unix_ll +function unix_single_write() { unix_ll("unix_single_write", arguments); } +// Provides: unix_socketpair +// Requires: unix_ll +function unix_socketpair() { unix_ll("unix_socketpair", arguments); } +// Provides: unix_tcdrain +// Requires: unix_ll +function unix_tcdrain() { unix_ll("unix_tcdrain", arguments); } +// Provides: unix_tcflow +// Requires: unix_ll +function unix_tcflow() { unix_ll("unix_tcflow", arguments); } +// Provides: unix_tcflush +// Requires: unix_ll +function unix_tcflush() { unix_ll("unix_tcflush", arguments); } +// Provides: unix_tcgetattr +// Requires: unix_ll +function unix_tcgetattr() { unix_ll("unix_tcgetattr", arguments); } +// Provides: unix_tcsendbreak +// Requires: unix_ll +function unix_tcsendbreak() { unix_ll("unix_tcsendbreak", arguments); } +// Provides: unix_tcsetattr +// Requires: unix_ll +function unix_tcsetattr() { unix_ll("unix_tcsetattr", arguments); } +// Provides: unix_truncate +// Requires: unix_ll +function unix_truncate() { unix_ll("unix_truncate", arguments); } +// Provides: unix_truncate_64 +// Requires: unix_ll +function unix_truncate_64() { unix_ll("unix_truncate_64", arguments); } +// Provides: unix_umask +// Requires: unix_ll +function unix_umask() { unix_ll("unix_umask", arguments); } +// Provides: unix_utimes +// Requires: unix_ll +function unix_utimes() { unix_ll("unix_utimes", arguments); } +// Provides: unix_write +// Requires: unix_ll +function unix_write() { unix_ll("unix_write", arguments); } +// Provides: unix_exit +// Requires: unix_ll +function unix_exit() { unix_ll("unix_exit", arguments); } +// Provides: unix_spawn +// Requires: unix_ll +function unix_spawn() { unix_ll("unix_spawn", arguments); } +// Provides: unix_fsync +// Requires: unix_ll +function unix_fsync() { unix_ll("unix_fsync", arguments); } +// Provides: unix_inchannel_of_filedescr +// Requires: unix_ll +function unix_inchannel_of_filedescr() { unix_ll("unix_inchannel_of_filedescr", arguments); } +// Provides: unix_outchannel_of_filedescr +// Requires: unix_ll +function unix_outchannel_of_filedescr() { unix_ll("unix_outchannel_of_filedescr", arguments); } +// Provides: caml_mutex_try_lock +// Requires: unix_ll +function caml_mutex_try_lock() { unix_ll("caml_mutex_try_lock", arguments); } +// Provides: caml_thread_join +// Requires: unix_ll +function caml_thread_join() { unix_ll("caml_thread_join", arguments); } +// Provides: caml_thread_sigmask +// Requires: unix_ll +function caml_thread_sigmask() { unix_ll("caml_thread_sigmask", arguments); } +// Provides: caml_unix_map_file_bytecode +// Requires: unix_ll +function caml_unix_map_file_bytecode() { unix_ll("caml_unix_map_file_bytecode", arguments); } +// Provides: caml_wait_signal +// Requires: unix_ll +function caml_wait_signal() { unix_ll("caml_wait_signal", arguments); } diff --git a/editor/code/src/browser.ts b/editor/code/src/browser.ts index 3164eb48..0b45263e 100644 --- a/editor/code/src/browser.ts +++ b/editor/code/src/browser.ts @@ -1,19 +1,81 @@ -import { ExtensionContext } from "vscode"; -import { LanguageClient } from "vscode-languageclient/browser"; +import { ExtensionContext, Uri } from "vscode"; +import { + LanguageClient, + LanguageClientOptions, +} from "vscode-languageclient/browser"; import { activateCoqLSP, ClientFactoryType, deactivateCoqLSP } from "./client"; +import { workspace } from "vscode"; + +class InterruptibleLC extends LanguageClient { + private readonly interrupt_vec?: Int32Array; + + constructor( + id: string, + name: string, + clientOptions: LanguageClientOptions, + worker: Worker + ) { + super(id, name, clientOptions, worker); + + // We don't fail if COI is not enabled, as of Feb 2023 you must either: + // - pass --enable-coi to vscode + // - use `?enable-coi= in the vscode dev setup + // See https://code.visualstudio.com/updates/v1_72#_towards-cross-origin-isolation + // See https://github.com/microsoft/vscode-wasm + if (typeof SharedArrayBuffer !== "undefined") { + this.interrupt_vec = new Int32Array(new SharedArrayBuffer(4)); + worker.postMessage(["SetupInterrupt", this.interrupt_vec]); + } + + this.middleware.sendRequest = (type, param, token, next) => { + this.interrupt(); + return next(type, param, token); + }; + this.middleware.sendNotification = (type, next, params) => { + this.interrupt(); + return next(type, params); + }; + + this.middleware.didChange = (data, next) => { + this.interrupt(); + return next(data); + }; + } + + public interrupt() { + if (this.interrupt_vec) { + Atomics.add(this.interrupt_vec, 0, 1); + } + } +} export function activate(context: ExtensionContext): void { const cf: ClientFactoryType = (context, clientOptions, wsConfig) => { // Pending on having the API to fetch the worker file. - throw "Worker not found"; - let worker = new Worker(""); - return new LanguageClient( + // throw "Worker not found"; + const coqWorker = Uri.joinPath( + context.extensionUri, + "out/coq_lsp_worker.bc.js" + ); + console.log(coqWorker); + + let worker = new Worker(coqWorker.toString(true)); + let client = new InterruptibleLC( "coq-lsp", "Coq LSP Worker", clientOptions, worker ); + return client; }; + + // let files = Uri.joinPath(context.extensionUri, "out/files.json"); + + // workspace.fs.readFile(files).then((content) => { + // let s = new TextDecoder().decode(content); + // console.log(`files: `, JSON.parse(s)); + // }); + activateCoqLSP(context, cf); } diff --git a/examples/documentSymbol.v b/examples/documentSymbol.v index a0149e94..78044a02 100644 --- a/examples/documentSymbol.v +++ b/examples/documentSymbol.v @@ -42,4 +42,4 @@ Module Bar. Theorem not : False. Qed. -End Bar. \ No newline at end of file +End Bar. diff --git a/flake.nix b/flake.nix index 0b4f98d6..5e130af7 100644 --- a/flake.nix +++ b/flake.nix @@ -75,7 +75,7 @@ flakeFormatter = true; - settings.global.excludes = ["./vendor/**"]; + settings.global.excludes = ["./vendor/**" "controller-js/js_stub/**"]; programs.alejandra.enable = true; programs.ocamlformat = { From 81b490c6b910350cdb8f999fbe82f7fff7fa05a5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Sep 2024 17:38:37 +0200 Subject: [PATCH 22/31] [ci] [js] Build JS worker on CI. --- .github/workflows/build.yml | 46 +++++++++++++++ Makefile | 5 ++ etc/0001-coq-lsp-patch.patch | 59 +++++++++++++++++++ ...001-jscoq-lib-system.ml-de-unix-stat.patch | 31 ++++++++++ 4 files changed, 141 insertions(+) create mode 100644 etc/0001-coq-lsp-patch.patch create mode 100644 etc/0001-jscoq-lib-system.ml-de-unix-stat.patch diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 21416bab..3d1bd616 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -85,6 +85,52 @@ jobs: - name: πŸ› Test fcc run: opam exec -- make test-compiler + build-js: + name: Web Worker Build + strategy: + fail-fast: false + runs-on: ubuntu-latest + + steps: + # OPAM figures out everything but the libgmp-dev:i386 + # dependency, maybe worth fixing this upstream in the opam + # repository + - name: Install apt dependencies + run: | + sudo apt-get install aptitude + sudo dpkg --add-architecture i386 + sudo aptitude -o Acquire::Retries=30 update -q + sudo aptitude -o Acquire::Retries=30 install gcc-multilib g++-multilib pkg-config libgmp-dev libgmp-dev:i386 -y + + - name: πŸ”­ Checkout code + uses: actions/checkout@v4 + with: + submodules: recursive + + - name: 🐫 Setup OCaml + uses: ocaml/setup-ocaml@v2 + with: + ocaml-compiler: "ocaml-variants.4.14.2+options,ocaml-option-32bit" + dune-cache: true + + - name: 🐫πŸͺ🐫 Get dependencies + run: | + opam exec -- make opam-deps + opam pin add js_of_ocaml --dev -y + opam pin add js_of_ocaml-compiler --dev -y + opam install zarith_stubs_js js_of_ocaml-ppx -y + + - name: πŸ’‰πŸ’‰πŸ’‰ Patch Coq + run: make patch-for-js + + - name: 🦏🧱🦏 Build coq-lsp JS version 🦏🦏🦏 + run: opam exec -- make js + + - name: Upload artifact + uses: actions/upload-artifact@v4 + with: + name: coq-lsp_worker and front-end + path: editor/code/out/ build-opam: name: Opam dev install strategy: diff --git a/Makefile b/Makefile index ec08903c..030891c7 100644 --- a/Makefile +++ b/Makefile @@ -144,3 +144,8 @@ opam-update-and-reinstall: git pull --recurse-submodules for pkg in coq-core coq-stdlib coqide-server coq; do opam install -y vendor/coq/$$pkg.opam; done opam install . + +.PHONY: patch-for-js +patch-for-js: + cd vendor/coq && patch -p1 < ../../etc/0001-coq-lsp-patch.patch + cd vendor/coq && patch -p1 < ../../etc/0001-jscoq-lib-system.ml-de-unix-stat.patch diff --git a/etc/0001-coq-lsp-patch.patch b/etc/0001-coq-lsp-patch.patch new file mode 100644 index 00000000..f42d9cd4 --- /dev/null +++ b/etc/0001-coq-lsp-patch.patch @@ -0,0 +1,59 @@ +From aa1c239f64a703785d9c4a520eee3aa4f97fa3ba Mon Sep 17 00:00:00 2001 +From: Emilio Jesus Gallego Arias +Date: Thu, 26 Sep 2024 21:46:55 +0200 +Subject: [PATCH] coq-lsp patch + +--- + lib/control.ml | 7 +++++++ + lib/dune | 4 ++++ + lib/jscoq_extern.c | 4 ++++ + 3 files changed, 15 insertions(+) + create mode 100644 lib/jscoq_extern.c + +diff --git a/lib/control.ml b/lib/control.ml +index 2480821c61..49ddb6e7e3 100644 +--- a/lib/control.ml ++++ b/lib/control.ml +@@ -18,7 +18,14 @@ let enable_thread_delay = ref false + + exception Timeout + ++(* implemented in backend/jsoo/js_stub/interrupt.js *) ++external interrupt_pending : unit -> bool = "interrupt_pending" ++ ++let jscoq_event_yield () = ++ if interrupt_pending () then interrupt := true ++ + let check_for_interrupt () = ++ jscoq_event_yield (); + if !interrupt then begin interrupt := false; raise Sys.Break end; + if !enable_thread_delay then begin + incr steps; +diff --git a/lib/dune b/lib/dune +index e7b1418c9b..f23338c03c 100644 +--- a/lib/dune ++++ b/lib/dune +@@ -4,6 +4,10 @@ + (public_name coq-core.lib) + (wrapped false) + (modules_without_implementation xml_datatype) ++ (foreign_stubs ++ (language c) ++ (names jscoq_extern) ++ (flags :standard (:include %{project_root}/config/dune.c_flags))) + (libraries + coq-core.boot coq-core.clib coq-core.config + (select instr.ml from +diff --git a/lib/jscoq_extern.c b/lib/jscoq_extern.c +new file mode 100644 +index 0000000000..7d0bb8c8bc +--- /dev/null ++++ b/lib/jscoq_extern.c +@@ -0,0 +1,4 @@ ++#include ++ ++// jsCoq Stub; actual implementation is in backend/jsoo/js_stub/interrupt.js ++value interrupt_pending() { return Val_false; } +-- +2.43.0 + diff --git a/etc/0001-jscoq-lib-system.ml-de-unix-stat.patch b/etc/0001-jscoq-lib-system.ml-de-unix-stat.patch new file mode 100644 index 00000000..49e45b9d --- /dev/null +++ b/etc/0001-jscoq-lib-system.ml-de-unix-stat.patch @@ -0,0 +1,31 @@ +From 389853f5b1cfd0d9af413f52a8a766dc15107806 Mon Sep 17 00:00:00 2001 +From: Emilio Jesus Gallego Arias +Date: Fri, 27 Sep 2024 16:39:19 +0200 +Subject: [PATCH] [jscoq] [lib/system.ml] de-unix-stat + +--- + lib/system.ml | 8 ++++---- + 1 file changed, 4 insertions(+), 4 deletions(-) + +diff --git a/lib/system.ml b/lib/system.ml +index 8f1315c159..a2473c11c9 100644 +--- a/lib/system.ml ++++ b/lib/system.ml +@@ -69,10 +69,10 @@ let apply_subdir f path name = + let base = try Filename.chop_extension name with Invalid_argument _ -> name in + if ok_dirname base then + let path = if path = "." then name else path//name in +- match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with +- | Unix.S_DIR when name = base -> f (FileDir (path,name)) +- | Unix.S_REG -> f (FileRegular name) +- | _ -> () ++ if Sys.is_directory path && name = base then ++ f (FileDir (path,name)) ++ else ++ f (FileRegular name) + + let readdir dir = try Sys.readdir dir with Sys_error _ -> [||] + +-- +2.43.0 + From d7e543c49a4a240826f0af2acee5e0d163c17a15 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 27 Sep 2024 00:43:19 +0200 Subject: [PATCH 23/31] [js] Build working filesystem for findlib-based worker. We hook `loadfile` to use precompiled `.cma.js` files, using our copy of findlib. The build is very rustical, but works. We also tweak the VM options so they are correct. --- .github/workflows/build.yml | 27 ++++++++++--- Makefile | 50 ++++++++++++++++++++++- controller-js/README.md | 70 ++++++++++++++++++++++++++++++++- controller-js/coq_lsp_worker.ml | 63 +++++++++++++++++++++++------ controller-js/dune | 40 +++++++++++++++---- controller-js/js_stub/unix.js | 3 ++ controller-js/my_dynload.ml | 42 ++++++++++++++++++++ controller-js/my_dynload.mli | 2 + etc/META.threads | 37 +++++++++++++++++ 9 files changed, 308 insertions(+), 26 deletions(-) create mode 100644 controller-js/my_dynload.ml create mode 100644 controller-js/my_dynload.mli create mode 100755 etc/META.threads diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 3d1bd616..e8ea7dd5 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -116,21 +116,38 @@ jobs: - name: 🐫πŸͺ🐫 Get dependencies run: | opam exec -- make opam-deps - opam pin add js_of_ocaml --dev -y - opam pin add js_of_ocaml-compiler --dev -y + opam pin add js_of_ocaml-compiler https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y + opam pin add js_of_ocaml https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y opam install zarith_stubs_js js_of_ocaml-ppx -y - name: πŸ’‰πŸ’‰πŸ’‰ Patch Coq run: make patch-for-js - name: 🦏🧱🦏 Build coq-lsp JS version 🦏🦏🦏 - run: opam exec -- make js + run: | + opam exec -- make controller-js/coq-fs-core.js + opam exec -- make js + + - name: πŸš€ Setup node + uses: actions/setup-node@v4 + with: + node-version: 22 + + - name: 🦏🧱🦏 Build coq-lsp VSCode extension 🦏🦏🦏 + run: opam exec -- make extension - name: Upload artifact uses: actions/upload-artifact@v4 with: name: coq-lsp_worker and front-end - path: editor/code/out/ + path: | + editor/code/package.json + editor/code/README.md + editor/code/CHANGELOG.md + editor/code/syntaxes + editor/code/out/ + editor/code/coq.configuration.json + compression-level: 9 build-opam: name: Opam dev install strategy: @@ -195,7 +212,7 @@ jobs: - name: πŸš€ Setup node uses: actions/setup-node@v4 with: - node-version: 18 + node-version: 22 - run: npm ci - run: npx --yes @vscode/vsce ls diff --git a/Makefile b/Makefile index 030891c7..aadf72e4 100644 --- a/Makefile +++ b/Makefile @@ -1,3 +1,5 @@ +SHELL := /usr/bin/env bash + COQ_BUILD_CONTEXT=../_build/default/coq PKG_SET= \ @@ -79,7 +81,7 @@ winconfig: .PHONY: js js: COQVM = no js: coq_boot - dune build --profile=release controller-js/coq_lsp_worker.bc.cjs + dune build --profile=release --display=quiet $(PKG_SET) controller-js/coq_lsp_worker.bc.cjs mkdir -p editor/code/out/ && cp -a controller-js/coq_lsp_worker.bc.cjs editor/code/out/coq_lsp_worker.bc.js .PHONY: coq_boot @@ -149,3 +151,49 @@ opam-update-and-reinstall: patch-for-js: cd vendor/coq && patch -p1 < ../../etc/0001-coq-lsp-patch.patch cd vendor/coq && patch -p1 < ../../etc/0001-jscoq-lib-system.ml-de-unix-stat.patch + +_LIBROOT=$(shell opam var lib) + +# Super-hack +controller-js/coq-fs-core.js: COQVM = no +controller-js/coq-fs-core.js: coq_boot + dune build --profile=release --display=quiet $(PKG_SET) etc/META.threads + for i in $$(find _build/install/default/lib/coq-core/plugins -name *.cma); do js_of_ocaml --dynlink $$i; done + for i in $$(find _build/install/default/lib/coq-lsp/serlib -wholename */*.cma); do js_of_ocaml --dynlink $$i; done + cd _build/install/default/lib && \ + js_of_ocaml build-fs -o coq-fs-core.js \ + $$(find coq-core/ \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \ + $$(find coq-lsp/ \( -wholename '*/serlib/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/%p ") \ + ../../../../etc/META.threads:/static/lib/threads/META \ + $$(find $(_LIBROOT) -wholename '*/str/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/seq/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/uri/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/base/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/unix/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/zarith/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/yojson/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/findlib/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/dynlink/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/parsexp/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/sexplib/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/sexplib0/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/bigarray/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/cmdliner/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/ppx_hash/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/angstrom/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/stringext/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/ppx_compare/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/ppx_deriving/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/ppx_sexp_conv/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/memprof-limits/META' -printf "%p:/static/lib/%P ") \ + $$(find $(_LIBROOT) -wholename '*/ppx_deriving_yojson/META' -printf "%p:/static/lib/%P ") + # These libs are actually linked, so no cma is needed. + # $$(find $(_LIBROOT) -wholename '*/zarith/*.cma' -printf "%p:/static/lib/%P " -or -wholename '*/zarith/META' -printf "%p:/static/lib/%P ") + cp _build/install/default/lib/coq-fs-core.js controller-js + +# Serlib plugins require: +# ppx_compare.runtime-lib +# ppx_deriving.runtime +# ppx_deriving_yojson.runtime +# ppx_hash.runtime-lib +# ppx_sexp_conv.runtime-lib diff --git a/controller-js/README.md b/controller-js/README.md index 6b2ec291..cd1c4659 100644 --- a/controller-js/README.md +++ b/controller-js/README.md @@ -1,10 +1,78 @@ ## coq-lsp Web Worker README This directory contains the implementation of our LSP-compliant web -worker for Coq / coq-lsp. +worker for Coq, based on jsCoq. As you can see the implementation is minimal, thanks to proper abstraction of the core of the controller. For now it is only safe to use the worker in 32bit OCaml mode. +Support for this build is still experimental. See [the javascript +compilation +meta-issue](https://github.com/ejgallego/coq-lsp/issues/833) for more +information. + +## Building the Worker + +The worker needs two parts to work: + +- the worker binary +- the worker filesystem + +which are then bundled in a single `.js` file. + +Type + +``` +make controller-js/coq-fs-core.js && make js +``` +to build the worker filesystem and the worker, which will be placed under `editor/code/out`. + +As of now the build is very artisanal and not flexible at all, we hope to improve it soon. + +## Testing the worker + +You can test the server using any of the [official methods](https://code.visualstudio.com/api/extension-guides/web-extensions#test-your-web-extension). + +Using the regular setup `dune exec -- code editor/code` and then +selecting "Web Extension" in the run menu works out of the box. + +A quick recipe from the manual is: + +``` +$ make controller-js/coq-fs-core.js && make js +$ npx @vscode/test-web --browser chromium --extensionDevelopmentPath=editor/code +$ chrome localhost:3000 +``` + +you can also download the artifacts from the CI build, and point +`--extensionDevelopmentPath=` to the path you have downloaded the +extension + Coq build. + +## COI + +As of Feb 2023, due to security restrictions, you may need to either: + + - pass `--enable-coi` to `code` + - use ``?enable-coi=` in the vscode dev setup + +in order to have interruptions (`SharedBufferArray`) working. + +See https://code.visualstudio.com/updates/v1_72#_towards-cross-origin-isolation + +## WASM + +We hope to have a WASM backend working soon, based on waCoq, see +https://github.com/microsoft/vscode-wasm + +## Filesystem layout + +We need to have most `META` files in findlib, plus the Coq and +`coq-lsp.serlib.*` plugins. These should be precompiled. + +- `/static/lib`: OCaml findlib root +- `/static/coqlib`: Coq root, with regular paths + + `/static/coqlib/theories` + + `/static/coqlib/user-contrib` + diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml index 91e19577..2fabd2f7 100644 --- a/controller-js/coq_lsp_worker.ml +++ b/controller-js/coq_lsp_worker.ml @@ -127,9 +127,31 @@ let on_init ~io ~root_state ~cmdline ~debug msg = in ignore (setTimeout (process_queue ~state) 0.1)) +let time f x = + let time = Sys.time () in + let res = f x in + let time_new = Sys.time () in + Format.eprintf "loadfile [dynlink] took: %f seconds%!" (time_new -. time); + res + +let loadfile file = + let file_js = Filename.remove_extension file ^ ".js" in + if Sys.file_exists file_js then ( + Format.eprintf "loadfile [eval_js]: %s%!" file; + let js_code = Sys_js.read_file ~name:file_js in + let js_code = + Format.asprintf "(function (globalThis) { @[%s@] })" js_code + in + Js.Unsafe.((eval_string js_code : < .. > Js.t -> unit) global)) + else ( + (* Not precompiled *) + Format.eprintf "loadfile [dynlink]: %s%!" file; + time Dynlink.loadfile file) + let coq_init ~debug = - let load_module = Dynlink.loadfile in - let load_plugin = Coq.Loader.plugin_handler None in + let loader = My_dynload.load_packages ~debug:false ~loadfile in + let load_module = loadfile in + let load_plugin = Coq.Loader.plugin_handler (Some loader) in (* XXX: Fixme at some point? *) let vm, warnings = (false, Some "-vm-compute-disabled") in Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings }) @@ -154,25 +176,42 @@ let main () = let io = CB.cb in Fleche.Io.CallBack.set io; - let stdlib = - let unix_path = "/static/coq/theories/" in - let coq_path = Names.(DirPath.make [ Id.of_string "Coq" ]) in + let stdlib coqlib = + let unix_path = Filename.concat coqlib "theories" in + let coq_path = Names.(DirPath.make [ Id.of_string "Stdlib" ]) in Loadpath. { unix_path; coq_path; implicit = true; has_ml = false; recursive = true } in + let user_contrib coqlib = + let unix_path = Filename.concat coqlib "user-contrib" in + let coq_path = Names.DirPath.empty in + Loadpath. + { unix_path + ; coq_path + ; implicit = false + ; has_ml = false + ; recursive = true + } + in + let cmdline = + let coqlib = "/static/coqlib" in + let findlib_config = Some findlib_path in + let ocamlpath = [] in + let vo_load_path = List.map (fun f -> f coqlib) [ stdlib; user_contrib ] in Coq.Workspace.CmdLine. - { coqlib = "/static/coqlib" - ; coqcorelib = "/static/lib/coq-core" - ; findlib_config = Some findlib_path - ; ocamlpath = [] - ; vo_load_path = [ stdlib ] + { coqlib + ; coqcorelib = "/static/lib/coq-core" (* deprecated upstream *) + ; findlib_config + ; ocamlpath + ; vo_load_path ; ml_include_path = [] - ; require_libraries = [] - ; args = [ "-noinit" ] + ; require_libraries = [ (None, "Stdlib.Init.Prelude") ] + ; args = [ "-noinit"; "-boot" ] } in + let debug = true in let root_state = coq_init ~debug in Worker.set_onmessage (on_init ~io ~root_state ~cmdline ~debug); diff --git a/controller-js/dune b/controller-js/dune index af7826f5..123b03de 100644 --- a/controller-js/dune +++ b/controller-js/dune @@ -10,12 +10,15 @@ js_stub/coq_vm.js js_stub/coq_perf.js js_stub/interrupt.js + coq-fs-core.js + coq-fs.js marshal-arch.js) (flags :standard + --linkall --dynlink - +dynlink.js - ; (:include .extraflags) + ; --toplevel + (:include .extraflags) ; +toplevel.js ; --enable ; with-js-error @@ -24,13 +27,19 @@ ; --no-inline ; --debug-info ; --source-map - ; no coq-fs yet - ; --file=coq-fs + ; --file=%{dep:coq-fs} --setenv PATH=/bin)) (link_flags -linkall -no-check-prims) ; The old makefile set: -noautolink -no-check-prims - (libraries zarith_stubs_js yojson controller)) + (libraries + zarith_stubs_js + yojson + controller + ; js_of_ocaml-toplevel + ; js_of_ocaml-compiler.dynlink + ; js_of_ocaml-compiler.findlib-support + )) (rule (target coq_lsp_worker.bc.cjs) @@ -40,11 +49,28 @@ (rule (targets marshal-arch.js) - ; This is to inject the dep of a FS on the executable if we want. - ; (deps coq-fs) (action (copy js_stub/marshal%{ocaml-config:word_size}.js %{targets}))) +(rule + (targets coq-fs.js) + (deps + (package coq-stdlib)) + (action + (bash + "cd ../vendor/coq && js_of_ocaml build-fs -o ../../controller-js/coq-fs.js $(find theories user-contrib \\( -wholename 'theories/*.vo' -or -wholename 'theories/*.glob' -or -wholename 'theories/*.v' -or -wholename 'user-contrib/*.vo' -or -wholename 'user-contrib/*.v' -or -wholename 'user-contrib/*.glob' \\) -printf '%p:/static/coqlib/%p ')"))) + +; for coq-fs-core.js +; js_of_ocaml build-fs -o coq-fs-core.js $(find coq-core/ -wholename '*/plugins/*/*.cma' -or -wholename '*/META' -printf "%p:/lib/%p") + +; (rule +; (targets coq-fs-core.js) +; (deps +; (package coq-core)) +; (action +; (bash +; "cd ../vendor/coq && js_of_ocaml build-fs -o ../../controller-js/coq-fs.js $(find theories -wholename 'theories/Init/*.vo' -printf '%p:/static/%p '"))) + ; Set debug flags if JSCOQ_DEBUG environment variable is set. ; (ugly, but there are no conditional expressions in Dune) diff --git a/controller-js/js_stub/unix.js b/controller-js/js_stub/unix.js index a606d9bb..07dbbb7c 100644 --- a/controller-js/js_stub/unix.js +++ b/controller-js/js_stub/unix.js @@ -383,6 +383,9 @@ function unix_open() { unix_ll("unix_open", arguments); } // Provides: unix_putenv // Requires: unix_ll function unix_putenv() { unix_ll("unix_putenv", arguments); } +// Provides: unix_realpath +// Requires: unix_ll +function unix_realpath() { unix_ll("unix_realpath", arguments); } // Provides: unix_recv // Requires: unix_ll function unix_recv() { unix_ll("unix_recv", arguments); } diff --git a/controller-js/my_dynload.ml b/controller-js/my_dynload.ml new file mode 100644 index 00000000..bcec1a3d --- /dev/null +++ b/controller-js/my_dynload.ml @@ -0,0 +1,42 @@ +(* Utilities for loading dynamically packages, adapted from ocamlfind, until + upstream merges this patch *) + +open Printf + +let load_pkg ~debug ~loadfile pkg = + if not (Findlib.is_recorded_package pkg) then ( + if debug then eprintf "[DEBUG] Fl_dynload: about to load: %s\n%!" pkg; + (* Determine the package directory: *) + let d = Findlib.package_directory pkg in + (* First try the new "plugin" variable: *) + let preds = Findlib.recorded_predicates () in + let archive = + try Findlib.package_property preds pkg "plugin" + with Not_found -> ( + (* Legacy: use "archive" but require that the predicate "plugin" is + mentioned in the definition *) + try + let v, fpreds = + Findlib.package_property_2 ("plugin" :: preds) pkg "archive" + in + let need_plugin = List.mem "native" preds in + if need_plugin && not (List.mem (`Pred "plugin") fpreds) then "" + else v + with Not_found -> "") + in + (* Split the plugin/archive property and resolve the files: *) + let files = Fl_split.in_words archive in + if debug then eprintf "[DEBUG] Fl_dynload: files=%S\n%!" archive; + List.iter + (fun file -> + if debug then eprintf "[DEBUG] Fl_dynload: loading %S\n%!" file; + let file = Findlib.resolve_path ~base:d file in + loadfile file) + files; + Findlib.record_package Findlib.Record_load pkg) + else if debug then eprintf "[DEBUG] Fl_dynload: not loading: %s\n%!" pkg + +let load_packages ?(debug = false) ?(loadfile = Dynlink.loadfile) pkgs = + let preds = Findlib.recorded_predicates () in + let eff_pkglist = Findlib.package_deep_ancestors preds pkgs in + List.iter (load_pkg ~debug ~loadfile) eff_pkglist diff --git a/controller-js/my_dynload.mli b/controller-js/my_dynload.mli new file mode 100644 index 00000000..f29c74f1 --- /dev/null +++ b/controller-js/my_dynload.mli @@ -0,0 +1,2 @@ +val load_packages : + ?debug:bool -> ?loadfile:(string -> unit) -> string list -> unit diff --git a/etc/META.threads b/etc/META.threads new file mode 100755 index 00000000..6e01dec9 --- /dev/null +++ b/etc/META.threads @@ -0,0 +1,37 @@ +# Specifications for the "threads" library: +version = "[distributed with Ocaml]" +description = "Multi-threading" +requires(mt,mt_vm) = "threads.vm" +# requires(mt,mt_posix) = "threads.posix" +directory = "^" +type_of_threads = "posix" + +browse_interfaces = "" + +warning(-mt) = "Linking problems may arise because of the missing -thread or -vmthread switch" +warning(-mt_vm,-mt_posix) = "Linking problems may arise because of the missing -thread or -vmthread switch" + +package "vm" ( + # --- Bytecode-only threads: + requires = "unix" + directory = "+vmthreads" + exists_if = "threads.cma" + archive(byte,mt,mt_vm) = "threads.cma" + version = "[internal]" +) + +package "posix" ( + # --- POSIX-threads: + requires = "unix" + directory = "+threads" + exists_if = "threads.cma" + archive(byte,mt,mt_posix) = "threads.cma" + archive(native,mt,mt_posix) = "threads.cmxa" + version = "[internal]" +) + +package "none" ( + error = "threading is not supported on this platform" + version = "[internal]" +) + From a304994b1e9fce8f94301bc5c1799cd3658b6a71 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Sep 2024 16:28:55 +0200 Subject: [PATCH 24/31] [js] [doc] [changes] Changes for javascript support. --- CHANGES.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index a3cb25b6..a225207f 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -19,6 +19,10 @@ #829, thanks to @gmalecha for the idea, c.f. Coq issue 19601) - [fleche] Highlight the full first line of the document on initialization error (@ejgallego, #832) + - [fleche] [jscoq] [js] Build worker version of `coq-lsp`. This + provides a full working Coq enviroment in `vscode.dev`. The web + worker version is build as an artifact on CI (@ejgallego + @corwin-of-amber, #433) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- From 9fa6a0f45005e96fff2520aa71fe48541dca676e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Sep 2024 16:32:17 +0200 Subject: [PATCH 25/31] [doc] [js] More docs on our JS setup. --- controller-js/README.md | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/controller-js/README.md b/controller-js/README.md index cd1c4659..244cc00c 100644 --- a/controller-js/README.md +++ b/controller-js/README.md @@ -18,16 +18,23 @@ information. The worker needs two parts to work: - the worker binary -- the worker filesystem +- the worker OCaml filesystem (`controller-js/coq-fs-core.js`) +- the worker Coq filesystem (`controller-js/coq-fs.js`) which are then bundled in a single `.js` file. -Type +The worker OCaml filesystem includes: +- `META` files for anything used by Coq +- transpiled `.cma` to `.js` files for plugins that will be loaded by Coq + +Type: ``` -make controller-js/coq-fs-core.js && make js +make patch-for-js # (only once, patch Coq for JS build) +make controller-js/coq-fs-core.js # build the OCaml filesystem, needed when plugins change +make js # build the worker and link with the FS. ``` -to build the worker filesystem and the worker, which will be placed under `editor/code/out`. +to get a working build in `editor/code/out`. As of now the build is very artisanal and not flexible at all, we hope to improve it soon. @@ -75,4 +82,3 @@ We need to have most `META` files in findlib, plus the Coq and - `/static/coqlib`: Coq root, with regular paths + `/static/coqlib/theories` + `/static/coqlib/user-contrib` - From ba069246fedcdb7a66852afa770c9de3f117344d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Sep 2024 18:44:22 +0200 Subject: [PATCH 26/31] [gitignore] Update for the JS build --- .gitignore | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.gitignore b/.gitignore index 84104728..b0a73c4e 100644 --- a/.gitignore +++ b/.gitignore @@ -14,3 +14,8 @@ nix/profiles/ # examples config, ignore for now examples/.vscode + +# Related to the JS build and testing +/controller-js/coq-fs-core.js +/controller-js/coq_lsp_worker.bc.cjs +/.vscode-test-web/ From 0ae1e563e6e24589746c1d78b93b27c925002861 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Sep 2024 22:03:30 +0200 Subject: [PATCH 27/31] [hover] Fix universe printing in hover. Our code was incomplete. The API here could be really improved Coq-side. About is too verbose for hover, hence our code. We could opt for the version in `prettyp.ml` tho. Fixes #835 --- CHANGES.md | 4 ++- controller/rq_hover.ml | 71 +++++++++++++++++++++++++++++++++++------- examples/print_univs.v | 14 +++++++++ 3 files changed, 76 insertions(+), 13 deletions(-) create mode 100644 examples/print_univs.v diff --git a/CHANGES.md b/CHANGES.md index a225207f..e8038419 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -11,7 +11,7 @@ - [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) + 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 @@ -23,6 +23,8 @@ 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) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index 903bfc56..ad41e9bf 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 : Names.Constant.t option + (** full path of the constant, if any, for example + [Stdlib.Lists.map] *) + ; file : 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 = UVars.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in @@ -37,17 +55,34 @@ 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 + Def { typ; params; full_path = None; file = None } 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 = UVars.make_abstract_instance univs in let impargs = Impargs.select_stronger_impargs (Impargs.implicits_of_global (Names.GlobRef.ConstRef cr)) @@ -56,7 +91,12 @@ let info_of_const env sigma cr = 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 + Def { typ; params = inst; full_path = Some cr; file = source } let info_of_var env vr = let vdef = Environ.lookup_named vr env in @@ -73,7 +113,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 + ; file = None + } let info_of_id env sigma id = let qid = Libnames.qualid_of_string id in @@ -89,8 +135,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 -> @@ -128,11 +174,12 @@ let pp_file fmt = function | Some file -> Format.fprintf fmt " - **in file**: `%s`" file let pp_typ id = function - | Def (typ, cr, file) -> + | Def { typ; params; full_path; file } -> 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 file) | Notation nt -> let nt = Pp.string_of_ppcmds nt in Format.(asprintf "```coq\n%s\n```" nt) 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. From a4c9172d3f7cf3bf80ec64ba3051ad5d597ffcdd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Sep 2024 22:55:45 +0200 Subject: [PATCH 28/31] [hover] Print full paths and source files for inductives too. --- controller/rq_hover.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index ad41e9bf..bd78386f 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -15,7 +15,7 @@ type id_info = | Def of { typ : Pp.t (** type of the ide *) ; params : Pp.t (** params that need display next to the name *) - ; full_path : Names.Constant.t option + ; full_path : Pp.t option (** full path of the constant, if any, for example [Stdlib.Lists.map] *) ; file : string option (** filename where the constant is located *) @@ -63,7 +63,10 @@ let info_of_ind env ((sp, i) : Names.Ind.t) = 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 - Def { typ; params; full_path = None; file = None } + let dp = Names.MutInd.modpath sp |> Names.ModPath.dp in + let source = Coq.Module.(make dp |> Result.to_option |> Option.map source) in + let full_path = Some (Names.MutInd.print sp) in + Def { typ; params; full_path; file = source } let type_of_constant cb = cb.Declarations.const_type @@ -90,13 +93,14 @@ let info_of_const env cr = 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 full_path = Some (Names.Constant.print cr) in let source = Coq.Module.(make dp |> Result.to_option |> Option.map source) in let inst = if Environ.polymorphic_constant cr env then Printer.pr_universe_instance sigma inst else Pp.mt () in - Def { typ; params = inst; full_path = Some cr; file = source } + Def { typ; params = inst; full_path; file = source } let info_of_var env vr = let vdef = Environ.lookup_named vr env in @@ -165,9 +169,7 @@ 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 -> () From 12bcda690f4ee2f4ebf933d4d846fa977f2dcf10 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 28 Sep 2024 22:59:19 +0200 Subject: [PATCH 29/31] [hover] Minor refactoring. --- controller/rq_hover.ml | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index bd78386f..5c11f6f6 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -18,7 +18,7 @@ type id_info = ; full_path : Pp.t option (** full path of the constant, if any, for example [Stdlib.Lists.map] *) - ; file : string option (** filename where the constant is located *) + ; source : string option (** filename where the constant is located *) } let print_params env sigma params = @@ -63,10 +63,12 @@ let info_of_ind env ((sp, i) : Names.Ind.t) = 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 dp = Names.MutInd.modpath sp |> Names.ModPath.dp in - let source = Coq.Module.(make dp |> Result.to_option |> Option.map source) in let full_path = Some (Names.MutInd.print sp) in - Def { typ; params; full_path; file = source } + 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 @@ -92,15 +94,17 @@ let info_of_const env 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 full_path = Some (Names.Constant.print cr) in - let source = Coq.Module.(make dp |> Result.to_option |> Option.map source) in let inst = if Environ.polymorphic_constant cr env then Printer.pr_universe_instance sigma inst else Pp.mt () in - Def { typ; params = inst; full_path; file = source } + 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 @@ -122,7 +126,7 @@ let print_type env sigma x = { typ = Printer.pr_ltype_env env sigma x ; params = Pp.mt () ; full_path = None - ; file = None + ; source = None } let info_of_id env sigma id = @@ -176,12 +180,12 @@ let pp_file fmt = function | Some file -> Format.fprintf fmt " - **in file**: `%s`" file let pp_typ id = function - | Def { typ; params; full_path; 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: %s@\n```@\n@[%a@]@[%a@]@]" id param typ pp_cr - full_path pp_file file) + full_path pp_file source) | Notation nt -> let nt = Pp.string_of_ppcmds nt in Format.(asprintf "```coq\n%s\n```" nt) From 6259a7954c58db3c79edc5a9b8b05d88de51bf14 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 17:27:29 +0200 Subject: [PATCH 30/31] [hover] Disable show notation prototype plugin. It is not of any use yet, just a nuisance for everyone. --- controller/rq_hover.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index 5c11f6f6..c48fd46f 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -227,8 +227,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 From b9d7777dd5e8b10028aee68d7f708e735054ab7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 17:38:52 +0200 Subject: [PATCH 31/31] [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` (cc: #816) 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. This commit switches `documentSymbols` to the immediate mode, when in lazy checking mode. --- CHANGES.md | 9 +++++++++ controller/lsp_core.ml | 11 ++++++++++- controller/request.ml | 8 ++++++++ controller/request.mli | 4 ++++ fleche/theory.ml | 3 +++ fleche/theory.mli | 1 + 6 files changed, 35 insertions(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index e8038419..de4884e1 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -25,6 +25,15 @@ @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/controller/lsp_core.ml b/controller/lsp_core.ml index 102afbf9..eb33483e 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -402,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 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/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