diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 68d83d1e..c4b1042b 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -4,12 +4,14 @@ on:
push:
branches:
- main
+ - v8.18
- v8.17
- v8.16
- v8.15
pull_request:
branches:
- main
+ - v8.18
- v8.17
- v8.16
- v8.15
@@ -59,15 +61,17 @@ jobs:
- name: 🐫🐪🐫 Get dependencies
run: opam exec -- make opam-deps
+ - name: 🐛 Test coq-lsp
+ if: matrix.os == 'windows-latest'
+ run: opam exec -- make winconfig
+
- name: 🧱 Build coq-lsp
run: opam exec -- make build
- name: 🐛 Test coq-lsp
- if: matrix.os != 'windows-latest'
run: opam exec -- make test
- name: 🐛 Test fcc
- if: matrix.os != 'windows-latest'
run: opam exec -- make test-compiler
build-nix:
@@ -102,9 +106,9 @@ jobs:
- name: 🚀 Setup node
uses: actions/setup-node@v3
with:
- node-version: 16
+ node-version: 18
- run: npm ci
- - run: npx --yes vsce ls
+ - run: npx --yes @vscode/vsce ls
nix-flake-check:
name: Nix Flake Check
diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index e69de29b..00000000
diff --git a/CHANGES.md b/CHANGES.md
index 72cb0882..2ceb5576 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,17 @@
+# coq-lsp 0.1.8: Dot / Bracket
+------------------------------
+
+ - Update VSCode client dependencies, should bring some performance
+ improvements to goal pretty printing (@ejgallego, #530)
+ - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, #539, fixes #532)
+ - Added link to Python coq-lsp client by Pedro Carrot and Nuno
+ Saavedra (@Nfsaavedra, #536)
+ - Properly concatenate warnings from _CoqProject (@ejgallego,
+ reported by @mituharu, #541, fixes #540)
+ - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
+ parsing problem with extra fields in their requests (@ejgallego,
+ #547, reported by @Zimmi48)
+
# coq-lsp 0.1.7: Just-in-time
-----------------------------
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 3cffc37a..b36ba9c0 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -125,6 +125,19 @@ nix build .?submodules=1
This currently only applies to building the default package (`coq-lsp`), which is
the server. Clients don't have specific submodules as of yet.
+When the flake is out-of-date, for instance when a new version of ocamlformat
+is out, you can update the flake inputs with:
+```sh
+nix flake update
+```
+
+You can also add the `dev` version build to your flake as:
+```nix
+inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; };
+...
+coq-lsp.packages.${system}.default
+```
+
### Code organization
The `coq-lsp` server consists of several components, we present them bottom-up
diff --git a/Makefile b/Makefile
index 753ddf11..03fb1a84 100644
--- a/Makefile
+++ b/Makefile
@@ -26,8 +26,8 @@ test: build test/server/node_modules
cd test/server && npm test
.PHONY: test-compiler
-test-compiler: build
- OCAMLPATH=_build/install/default/lib:$$OCAMLPATH FCC_TEST=true dune runtest
+test-compiler:
+ dune runtest
.PHONY: fmt format
fmt format:
@@ -41,11 +41,27 @@ watch: coq_boot
build-all: coq_boot
dune build $(DUNEOPT) @all
-# We set -libdir due to a Coq bug on win32, see https://github.com/coq/coq/pull/17289
+# 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
vendor/coq/config/coq_config.ml:
- cd vendor/coq \
- && ./configure -no-ask -prefix $(shell pwd)/_build/install/default/ \
- -libdir $(shell pwd)/_build/install/default/lib/coq \
+ EPATH=$(shell pwd) \
+ && cd vendor/coq \
+ && ./configure -no-ask -prefix "$$EPATH/_build/install/default/" \
+ -libdir "$$EPATH/_build/install/default/lib/coq" \
+ -native-compiler no \
+ && cp theories/dune.disabled theories/dune \
+ && cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
+
+# We set windows parameters a bit better, note the need to use forward
+# slashed (cygpath -m) due to escaping :( , a conversion to `-w` is
+# welcomed if someones has time for this
+.PHONY: winconfig
+winconfig:
+ EPATH=$(shell cygpath -am .) \
+ && cd vendor/coq \
+ && ./configure -no-ask -prefix "$$EPATH\\_build\\install\\default\\" \
+ -libdir "$$EPATH\\_build\\install\\default\\lib\\coq\\" \
-native-compiler no \
&& cp theories/dune.disabled theories/dune \
&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
@@ -53,7 +69,7 @@ vendor/coq/config/coq_config.ml:
.PHONY: coq_boot
coq_boot:
# We do nothing for release versions
-# coq_boot: coq/config/coq_config.ml
+# coq_boot: vendor/coq/config/coq_config.ml
.PHONY: clean
clean:
diff --git a/README.md b/README.md
index 51bb7dcf..3ca54510 100644
--- a/README.md
+++ b/README.md
@@ -8,11 +8,15 @@ Studio Code](https://code.visualstudio.com/) extension for the [Coq Proof
Assistant](https://coq.inria.fr). Experimental support for [Vim](#vim) and
[Neovim](#neovim) is also available in their own projects.
-Install for Visual Studio is as easy as:
+**[Install: 🐧 Linux / 🍎 macOs]**:
```
$ opam install coq-lsp && code --install-extension ejgallego.coq-lsp
```
+**[Install: 🪟 Windows ]:**
+
+> see the [instructions](#-server); we will provide an `.exe` installer very soon
+
Key [features](#Features) of `coq-lsp` are continuous and incremental document
checking, advanced error recovery, markdown support, positional goals and
information panel, performance data, and more.
@@ -54,6 +58,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
- [🦄 Emacs](#-emacs)
- [✅ Vim](#-vim)
- [🩱 Neovim](#-neovim)
+ - [🐍 Python](#-python)
- [🗣️ Discussion Channel](#️-discussion-channel)
- [☎ Weekly Calls](#-weekly-calls)
- [❓FAQ](#faq)
@@ -213,13 +218,15 @@ SerAPI](etc/SerAPI.md) document.
## 🛠️ Installation
In order to use `coq-lsp` you'll need to install [**both**](etc/FAQ.md)
-`coq-lsp` and a suitable client. We recommend the Visual Studio Code Extension
-as client.
+`coq-lsp` and a suitable LSP client that understands `coq-lsp` extensions. The
+recommended client is the Visual Studio Code Extension, but we aim to fully
+support other clients officially and will do so once their authors consider them
+ready.
### 🏘️ Supported Coq Versions
-`coq-lsp` supports Coq 8.15, 8.16, Coq 8.17, and Coq's `master` branch. Code for
-each Coq version can be found in the corresponding branch.
+`coq-lsp` supports Coq 8.15, 8.16, Coq 8.17, Coq 8.18, and Coq's `master`
+branch. Code for each Coq version can be found in the corresponding branch.
We recommended a minimum of Coq 8.17, due to better test coverage for that
version. For 8.16, we recommend users to install the custom Coq tree as detailed
@@ -229,32 +236,29 @@ Support for older Coq versions is possible; it is possible to make `coq-lsp`
work with Coq back to Coq 8.10/8.9. If you are interested in making that happen
don't hesitate to get in touch with us.
+Note that this section covers user installs, if you would like to contribute to
+`coq-lsp` and build a development version, please check our [contributing
+guide](./CONTRIBUTING.md)
+
### 🏓 Server
-- **opam**:
+- **opam** (OSX/Linux):
```
opam install coq-lsp
```
- **Nix**:
- - In nixpkgs: [#213397](https://github.com/NixOS/nixpkgs/pull/213397)
- - In your flake:
- ```nix
- inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; };
- ...
- coq-lsp.packages.${system}.default
- ```
-- **Windows**: To install `coq-lsp` on windows, we recommend you use a cygwin
- build, such as the [one described
- here](https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin), tho
- any OCaml env where Coq can be built should work.
- - build `coq-lsp` from source (branch `v8.16`, which will become 0.1.7)
- - Set the path to `coq-lsp.exe` binary in VS Code settings
- - Set the `--ocamlpath=c:\$path_to_opam\lib` argument in VS Code settings if
- you get a findlib error. The Coq Platform ships with an un-configured
- binary. Note, the path should be unquoted
- - If the binary doesn't work, try to run it from the file explorer; if you get
- a `.dll` error you'll need to copy that dll (often `libgmp-10.dll`) to the
- `C:\Windows` folder for `coq-lsp` to work.
+ - In nixpkgs: [coqPackages.coq-lsp](https://github.com/NixOS/nixpkgs/tree/master/pkgs/development/coq-modules/coq-lsp)
+ - An example of a `flake` that uses `coq-lsp` in a development environment is here
+ https://github.com/HoTT/Coq-HoTT/blob/master/flake.nix .
+- **Windows**: To install `coq-lsp` on windows, you need to build the Coq Platform:
+ - Download and uncompress the Platform Script: https://github.com/coq/platform/archive/refs/tags/2023.03.0.zip
+ - From a shell, execute `./coq_platform_make_windows.bat`
+ - Select `C:\cp_817` as the install path, select the packages you want
+ - Run `C:\cp_817\Cygwin.bat`
+ - Run `opam install coq-lsp`
+ - Run `cp /cygdrive/c/cp_817/usr/x86_64-w64-mingw32/sys-root/mingw/bin/libgmp-10.dll /home/User/.opam/CP.2023.03.0~8.17~2023.08/bin`
+ - In VSCode native, you can now set the `Coq-lsp: Path` setting to `C:\cp_817\home\User\.opam\CP.2023.03.0~8.17~2023.08\bin\coq-lsp.exe`
+ - Things should work !
- **Coq Platform** (coming soon)
- See the [bug tracking coq-lsp inclusion](https://github.com/coq/platform/issues/319)
- [Do it yourself!](#server-1)
@@ -296,6 +300,11 @@ programs.vscode = {
- Experimental client by Jaehwang Jung: https://github.com/tomtomjhj/coq-lsp.nvim
+### 🐍 Python
+
+- Interact programmatically with Coq files by using the [Python `coq-lsp` client](https://github.com/sr-lab/coq-lsp-pyclient)
+ by Pedro Carrott and Nuno Saavedra.
+
## 🗣️ Discussion Channel
`coq-lsp` discussion channel it at [Coq's
diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml
index d8dc66e2..b1848906 100644
--- a/controller/lsp_core.ml
+++ b/controller/lsp_core.ml
@@ -35,11 +35,21 @@ module LIO = Lsp.Io
module LSP = Lsp.Base
module Helpers = struct
- (* helpers; fix to have better errors on wrong protocol code *)
+ (* XXX helpers; fix to have better errors on wrong protocol code *)
+ (* Also note that rely sometimes on "subtyping" of fields, that's something to
+ think about better and fix, see #547 *)
let get_uri params =
let document =
- field "textDocument" params
- |> Lsp.Doc.TextDocumentIdentifier.of_yojson |> Result.get_ok
+ match
+ field "textDocument" params |> Lsp.Doc.TextDocumentIdentifier.of_yojson
+ with
+ | Ok uri -> uri
+ | Error err ->
+ (* ppx_deriving_yojson error messages leave a lot to be desired *)
+ let message = Format.asprintf "json parsing failed: %s" err in
+ LIO.logMessage ~lvl:1 ~message;
+ (* XXX Fixme *)
+ CErrors.user_err (Pp.str "failed to parse uri")
in
let Lsp.Doc.TextDocumentIdentifier.{ uri } = document in
uri
diff --git a/coq/workspace.ml b/coq/workspace.ml
index a53ecbee..ffa96e2f 100644
--- a/coq/workspace.ml
+++ b/coq/workspace.ml
@@ -34,16 +34,18 @@ module Warning : sig
type t
val make : string -> t
- val apply : t -> unit
+
+ (** Adds new warnings to the list of current warnings *)
+ val apply : t list -> unit
end = struct
type t = string
let make x = x
- let to_string x = x
let apply w =
- let warn = CWarnings.get_flags () in
- CWarnings.set_flags (warn ^ to_string w)
+ let old_warn = CWarnings.get_flags () in
+ let new_warn = String.concat "," w in
+ CWarnings.set_flags (old_warn ^ "," ^ new_warn)
end
type t =
@@ -236,7 +238,7 @@ let apply ~uri
} =
if debug then CDebug.set_flags "backtrace";
Flags.apply flags;
- List.iter Warning.apply warnings;
+ Warning.apply warnings;
List.iter Mltop.add_ml_dir ml_include_path;
findlib_init ~ml_include_path ~ocamlpath;
List.iter Loadpath.add_vo_path vo_load_path;
diff --git a/coq/workspace.mli b/coq/workspace.mli
index 11cfedc8..f6494856 100644
--- a/coq/workspace.mli
+++ b/coq/workspace.mli
@@ -26,7 +26,10 @@ module Warning : sig
type t
val make : string -> t
- val apply : t -> unit
+
+ (** Adds new warnings to the list of current warnings, the Coq API here is a
+ bit tricky... *)
+ val apply : t list -> unit
end
type t = private
diff --git a/editor/code/.prettierrc b/editor/code/.prettierrc
new file mode 100644
index 00000000..f0eb61e0
--- /dev/null
+++ b/editor/code/.prettierrc
@@ -0,0 +1,6 @@
+{
+ "trailingComma": "es5",
+ "tabWidth": 2,
+ "semi": true,
+ "singleQuote": false
+}
diff --git a/editor/code/.vscodeignore b/editor/code/.vscodeignore
index ebf262cf..4f029d57 100644
--- a/editor/code/.vscodeignore
+++ b/editor/code/.vscodeignore
@@ -3,6 +3,7 @@
.prettierignore
.gitignore
.vscode/
+flakeModule.nix
# Source files
**/*.ts
@@ -18,3 +19,4 @@ esbuild.mjs
views/info/media/
# Perf view
+views/perf/media/
diff --git a/editor/code/package-lock.json b/editor/code/package-lock.json
index e4fae0a3..c82a0bce 100644
--- a/editor/code/package-lock.json
+++ b/editor/code/package-lock.json
@@ -1,7 +1,7 @@
{
"name": "coq-lsp",
"version": "0.1.7",
- "lockfileVersion": 2,
+ "lockfileVersion": 3,
"requires": true,
"packages": {
"": {
@@ -9,7 +9,7 @@
"version": "0.1.7",
"dependencies": {
"@vscode/webview-ui-toolkit": "^1.2.1",
- "jquery": "^3.6.3",
+ "jquery": "^3.7.0",
"object-hash": "^3.0.0",
"react": "^18.2.0",
"react-dom": "^18.2.0",
@@ -19,7 +19,7 @@
},
"devDependencies": {
"@types/jquery": "^3.5.16",
- "@types/node": "^16.11.7",
+ "@types/node": "^18.11.9",
"@types/object-hash": "^3.0.2",
"@types/react": "^18.0.27",
"@types/react-dom": "^18.0.10",
@@ -27,11 +27,11 @@
"@types/vscode": "^1.73.0",
"@types/vscode-webview": "^1.57.1",
"esbuild": "^0.16.17",
- "prettier": "^2.8.1",
- "typescript": "^4.9.4"
+ "prettier": "^3.0.0",
+ "typescript": "^5.1.6"
},
"engines": {
- "vscode": "^1.73.0"
+ "vscode": "^1.75.0"
}
},
"node_modules/@esbuild/android-arm": {
@@ -387,16 +387,16 @@
}
},
"node_modules/@microsoft/fast-element": {
- "version": "1.11.0",
- "resolved": "https://registry.npmjs.org/@microsoft/fast-element/-/fast-element-1.11.0.tgz",
- "integrity": "sha512-VKJYMkS5zgzHHb66sY7AFpYv6IfFhXrjQcAyNgi2ivD65My1XOhtjfKez5ELcLFRJfgZNAxvI8kE69apXERTkw=="
+ "version": "1.12.0",
+ "resolved": "https://registry.npmjs.org/@microsoft/fast-element/-/fast-element-1.12.0.tgz",
+ "integrity": "sha512-gQutuDHPKNxUEcQ4pypZT4Wmrbapus+P9s3bR/SEOLsMbNqNoXigGImITygI5zhb+aA5rzflM6O8YWkmRbGkPA=="
},
"node_modules/@microsoft/fast-foundation": {
- "version": "2.47.0",
- "resolved": "https://registry.npmjs.org/@microsoft/fast-foundation/-/fast-foundation-2.47.0.tgz",
- "integrity": "sha512-EyFuioaZQ9ngjUNRQi8R3dIPPsaNQdUOS+tP0G7b1MJRhXmQWIitBM6IeveQA6ZvXG6H21dqgrfEWlsYrUZ2sw==",
+ "version": "2.49.0",
+ "resolved": "https://registry.npmjs.org/@microsoft/fast-foundation/-/fast-foundation-2.49.0.tgz",
+ "integrity": "sha512-Wk4e4QXFVtT5hPwhMfHyGY30kixM0td8aDs7bAD6NM2z2SCBNvpTTWp+FCjx0I0lpUMlMenb6wsw7pMWQreRkQ==",
"dependencies": {
- "@microsoft/fast-element": "^1.11.0",
+ "@microsoft/fast-element": "^1.12.0",
"@microsoft/fast-web-utilities": "^5.4.1",
"tabbable": "^5.2.0",
"tslib": "^1.13.0"
@@ -432,9 +432,9 @@
}
},
"node_modules/@types/node": {
- "version": "16.18.11",
- "resolved": "https://registry.npmjs.org/@types/node/-/node-16.18.11.tgz",
- "integrity": "sha512-3oJbGBUWuS6ahSnEq1eN2XrCyf4YsWI8OyCvo7c64zQJNplk3mO84t53o8lfTk+2ji59g5ycfc6qQ3fdHliHuA==",
+ "version": "18.16.19",
+ "resolved": "https://registry.npmjs.org/@types/node/-/node-18.16.19.tgz",
+ "integrity": "sha512-IXl7o+R9iti9eBW4Wg2hx1xQDig183jj7YLn8F7udNceyfkbn1ZxmzZXuak20gR40D7pIkIY1kYGx5VIGbaHKA==",
"dev": true
},
"node_modules/@types/object-hash": {
@@ -450,9 +450,9 @@
"dev": true
},
"node_modules/@types/react": {
- "version": "18.0.27",
- "resolved": "https://registry.npmjs.org/@types/react/-/react-18.0.27.tgz",
- "integrity": "sha512-3vtRKHgVxu3Jp9t718R9BuzoD4NcQ8YJ5XRzsSKxNDiDonD2MXIT1TmSkenxuCycZJoQT5d2vE8LwWJxBC1gmA==",
+ "version": "18.2.14",
+ "resolved": "https://registry.npmjs.org/@types/react/-/react-18.2.14.tgz",
+ "integrity": "sha512-A0zjq+QN/O0Kpe30hA1GidzyFjatVvrpIvWLxD+xv67Vt91TWWgco9IvrJBkeyHm1trGaFS/FSGqPlhyeZRm0g==",
"dev": true,
"dependencies": {
"@types/prop-types": "*",
@@ -461,18 +461,18 @@
}
},
"node_modules/@types/react-dom": {
- "version": "18.0.10",
- "resolved": "https://registry.npmjs.org/@types/react-dom/-/react-dom-18.0.10.tgz",
- "integrity": "sha512-E42GW/JA4Qv15wQdqJq8DL4JhNpB3prJgjgapN3qJT9K2zO5IIAQh4VXvCEDupoqAwnz0cY4RlXeC/ajX5SFHg==",
+ "version": "18.2.6",
+ "resolved": "https://registry.npmjs.org/@types/react-dom/-/react-dom-18.2.6.tgz",
+ "integrity": "sha512-2et4PDvg6PVCyS7fuTc4gPoksV58bW0RwSxWKcPRcHZf0PRUGq03TKcD/rUHe3azfV6/5/biUBJw+HhCQjaP0A==",
"dev": true,
"dependencies": {
"@types/react": "*"
}
},
"node_modules/@types/scheduler": {
- "version": "0.16.2",
- "resolved": "https://registry.npmjs.org/@types/scheduler/-/scheduler-0.16.2.tgz",
- "integrity": "sha512-hppQEBDmlwhFAXKJX2KnWLYu5yMfi91yazPb2l+lbJiwW+wdo1gNeRA+3RgNSO39WYX2euey41KEwnqesU2Jew==",
+ "version": "0.16.3",
+ "resolved": "https://registry.npmjs.org/@types/scheduler/-/scheduler-0.16.3.tgz",
+ "integrity": "sha512-5cJ8CB4yAx7BH1oMvdU0Jh9lrEXyPkar6F9G/ERswkCuvP4KQZfZkSjcMbAICCpQTN4OuZn8tz0HiKv9TGZgrQ==",
"dev": true
},
"node_modules/@types/sizzle": {
@@ -488,9 +488,9 @@
"dev": true
},
"node_modules/@types/vscode": {
- "version": "1.73.0",
- "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.73.0.tgz",
- "integrity": "sha512-FhkfF7V3fj7S3WqXu7AxFesBLO3uMkdCPJJPbwyZXezv2xJ6xBWHYM2CmkkbO8wT9Fr3KipwxGGOoQRrYq7mHg==",
+ "version": "1.80.0",
+ "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.80.0.tgz",
+ "integrity": "sha512-qK/CmOdS2o7ry3k6YqU4zD3R2AYlJfbwBoSbKpBoP+GpXNE+0NEgJOli4n0bm0diK5kfBnchgCEj4igQz/44Hg==",
"dev": true
},
"node_modules/@types/vscode-webview": {
@@ -500,9 +500,9 @@
"dev": true
},
"node_modules/@vscode/webview-ui-toolkit": {
- "version": "1.2.1",
- "resolved": "https://registry.npmjs.org/@vscode/webview-ui-toolkit/-/webview-ui-toolkit-1.2.1.tgz",
- "integrity": "sha512-ZpVqLxoFWWk8mmAN7jr1v9yjD6NGBIoflAedNSusmaViqwHZ2znKBwAwcumLOlNlqmST6QMkiTVys7O8rzfd0w==",
+ "version": "1.2.2",
+ "resolved": "https://registry.npmjs.org/@vscode/webview-ui-toolkit/-/webview-ui-toolkit-1.2.2.tgz",
+ "integrity": "sha512-xIQoF4FC3Xh6d7KNKIoIezSiFWYFuf6gQMdDyKueKBFGeKwaHWEn+dY2g3makvvEsNMEDji/woEwvg9QSbuUsw==",
"dependencies": {
"@microsoft/fast-element": "^1.6.2",
"@microsoft/fast-foundation": "^2.38.0",
@@ -526,9 +526,9 @@
}
},
"node_modules/csstype": {
- "version": "3.1.1",
- "resolved": "https://registry.npmjs.org/csstype/-/csstype-3.1.1.tgz",
- "integrity": "sha512-DJR/VvkAvSZW9bTouZue2sSxDwdTN92uHjqeKVm+0dAqdfNykRzQ95tay8aXMBAAPpUiq4Qcug2L7neoRh2Egw==",
+ "version": "3.1.2",
+ "resolved": "https://registry.npmjs.org/csstype/-/csstype-3.1.2.tgz",
+ "integrity": "sha512-I7K1Uu0MBPzaFKg4nI5Q7Vs2t+3gWWW648spaF+Rg7pI9ds18Ugn+lvg4SHczUdKlHI5LWBXyqfS8+DufyBsgQ==",
"dev": true
},
"node_modules/esbuild": {
@@ -574,9 +574,9 @@
"integrity": "sha512-vlVu3N8d6yEMpMsEm+7sUBAI81aqYYuEvfK0jNqmdb/OPXzzH7QWDDnVjMvDSY47JdHEqx/dfC/q8WkfoTmpGQ=="
},
"node_modules/jquery": {
- "version": "3.6.3",
- "resolved": "https://registry.npmjs.org/jquery/-/jquery-3.6.3.tgz",
- "integrity": "sha512-bZ5Sy3YzKo9Fyc8wH2iIQK4JImJ6R0GWI9kL1/k7Z91ZBNgkRXE6U0JfHIizZbort8ZunhSI3jw9I6253ahKfg=="
+ "version": "3.7.0",
+ "resolved": "https://registry.npmjs.org/jquery/-/jquery-3.7.0.tgz",
+ "integrity": "sha512-umpJ0/k8X0MvD1ds0P9SfowREz2LenHsQaxSohMZ5OMNEU2r0tf8pdeEFTHMFxWVxKNyU9rTtK3CWzUCTKJUeQ=="
},
"node_modules/js-tokens": {
"version": "4.0.0",
@@ -625,15 +625,15 @@
}
},
"node_modules/prettier": {
- "version": "2.8.1",
- "resolved": "https://registry.npmjs.org/prettier/-/prettier-2.8.1.tgz",
- "integrity": "sha512-lqGoSJBQNJidqCHE80vqZJHWHRFoNYsSpP9AjFhlhi9ODCJA541svILes/+/1GM3VaL/abZi7cpFzOpdR9UPKg==",
+ "version": "3.0.0",
+ "resolved": "https://registry.npmjs.org/prettier/-/prettier-3.0.0.tgz",
+ "integrity": "sha512-zBf5eHpwHOGPC47h0zrPyNn+eAEIdEzfywMoYn2XPi0P44Zp0tSq64rq0xAREh4auw2cJZHo9QUob+NqCQky4g==",
"dev": true,
"bin": {
- "prettier": "bin-prettier.js"
+ "prettier": "bin/prettier.cjs"
},
"engines": {
- "node": ">=10.13.0"
+ "node": ">=14"
},
"funding": {
"url": "https://github.com/prettier/prettier?sponsor=1"
@@ -703,16 +703,16 @@
"integrity": "sha512-Xni35NKzjgMrwevysHTCArtLDpPvye8zV/0E4EyYn43P7/7qvQwPh9BGkHewbMulVntbigmcT7rdX3BNo9wRJg=="
},
"node_modules/typescript": {
- "version": "4.9.4",
- "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.4.tgz",
- "integrity": "sha512-Uz+dTXYzxXXbsFpM86Wh3dKCxrQqUcVMxwU54orwlJjOpO3ao8L7j5lH+dWfTwgCwIuM9GQ2kvVotzYJMXTBZg==",
+ "version": "5.1.6",
+ "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.1.6.tgz",
+ "integrity": "sha512-zaWCozRZ6DLEWAWFrVDz1H6FVXzUSfTy5FUMWsQlU8Ym5JP9eO4xkTIROFCQvhQf61z6O/G6ugw3SgAnvvm+HA==",
"dev": true,
"bin": {
"tsc": "bin/tsc",
"tsserver": "bin/tsserver"
},
"engines": {
- "node": ">=4.2.0"
+ "node": ">=14.17"
}
},
"node_modules/vscode-jsonrpc": {
@@ -755,468 +755,5 @@
"resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz",
"integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A=="
}
- },
- "dependencies": {
- "@esbuild/android-arm": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.16.17.tgz",
- "integrity": "sha512-N9x1CMXVhtWEAMS7pNNONyA14f71VPQN9Cnavj1XQh6T7bskqiLLrSca4O0Vr8Wdcga943eThxnVp3JLnBMYtw==",
- "dev": true,
- "optional": true
- },
- "@esbuild/android-arm64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/android-arm64/-/android-arm64-0.16.17.tgz",
- "integrity": "sha512-MIGl6p5sc3RDTLLkYL1MyL8BMRN4tLMRCn+yRJJmEDvYZ2M7tmAf80hx1kbNEUX2KJ50RRtxZ4JHLvCfuB6kBg==",
- "dev": true,
- "optional": true
- },
- "@esbuild/android-x64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/android-x64/-/android-x64-0.16.17.tgz",
- "integrity": "sha512-a3kTv3m0Ghh4z1DaFEuEDfz3OLONKuFvI4Xqczqx4BqLyuFaFkuaG4j2MtA6fuWEFeC5x9IvqnX7drmRq/fyAQ==",
- "dev": true,
- "optional": true
- },
- "@esbuild/darwin-arm64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/darwin-arm64/-/darwin-arm64-0.16.17.tgz",
- "integrity": "sha512-/2agbUEfmxWHi9ARTX6OQ/KgXnOWfsNlTeLcoV7HSuSTv63E4DqtAc+2XqGw1KHxKMHGZgbVCZge7HXWX9Vn+w==",
- "dev": true,
- "optional": true
- },
- "@esbuild/darwin-x64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/darwin-x64/-/darwin-x64-0.16.17.tgz",
- "integrity": "sha512-2By45OBHulkd9Svy5IOCZt376Aa2oOkiE9QWUK9fe6Tb+WDr8hXL3dpqi+DeLiMed8tVXspzsTAvd0jUl96wmg==",
- "dev": true,
- "optional": true
- },
- "@esbuild/freebsd-arm64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/freebsd-arm64/-/freebsd-arm64-0.16.17.tgz",
- "integrity": "sha512-mt+cxZe1tVx489VTb4mBAOo2aKSnJ33L9fr25JXpqQqzbUIw/yzIzi+NHwAXK2qYV1lEFp4OoVeThGjUbmWmdw==",
- "dev": true,
- "optional": true
- },
- "@esbuild/freebsd-x64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/freebsd-x64/-/freebsd-x64-0.16.17.tgz",
- "integrity": "sha512-8ScTdNJl5idAKjH8zGAsN7RuWcyHG3BAvMNpKOBaqqR7EbUhhVHOqXRdL7oZvz8WNHL2pr5+eIT5c65kA6NHug==",
- "dev": true,
- "optional": true
- },
- "@esbuild/linux-arm": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/linux-arm/-/linux-arm-0.16.17.tgz",
- "integrity": "sha512-iihzrWbD4gIT7j3caMzKb/RsFFHCwqqbrbH9SqUSRrdXkXaygSZCZg1FybsZz57Ju7N/SHEgPyaR0LZ8Zbe9gQ==",
- "dev": true,
- "optional": true
- },
- "@esbuild/linux-arm64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/linux-arm64/-/linux-arm64-0.16.17.tgz",
- "integrity": "sha512-7S8gJnSlqKGVJunnMCrXHU9Q8Q/tQIxk/xL8BqAP64wchPCTzuM6W3Ra8cIa1HIflAvDnNOt2jaL17vaW+1V0g==",
- "dev": true,
- "optional": true
- },
- "@esbuild/linux-ia32": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/linux-ia32/-/linux-ia32-0.16.17.tgz",
- "integrity": "sha512-kiX69+wcPAdgl3Lonh1VI7MBr16nktEvOfViszBSxygRQqSpzv7BffMKRPMFwzeJGPxcio0pdD3kYQGpqQ2SSg==",
- "dev": true,
- "optional": true
- },
- "@esbuild/linux-loong64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/linux-loong64/-/linux-loong64-0.16.17.tgz",
- "integrity": "sha512-dTzNnQwembNDhd654cA4QhbS9uDdXC3TKqMJjgOWsC0yNCbpzfWoXdZvp0mY7HU6nzk5E0zpRGGx3qoQg8T2DQ==",
- "dev": true,
- "optional": true
- },
- "@esbuild/linux-mips64el": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/linux-mips64el/-/linux-mips64el-0.16.17.tgz",
- "integrity": "sha512-ezbDkp2nDl0PfIUn0CsQ30kxfcLTlcx4Foz2kYv8qdC6ia2oX5Q3E/8m6lq84Dj/6b0FrkgD582fJMIfHhJfSw==",
- "dev": true,
- "optional": true
- },
- "@esbuild/linux-ppc64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/linux-ppc64/-/linux-ppc64-0.16.17.tgz",
- "integrity": "sha512-dzS678gYD1lJsW73zrFhDApLVdM3cUF2MvAa1D8K8KtcSKdLBPP4zZSLy6LFZ0jYqQdQ29bjAHJDgz0rVbLB3g==",
- "dev": true,
- "optional": true
- },
- "@esbuild/linux-riscv64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/linux-riscv64/-/linux-riscv64-0.16.17.tgz",
- "integrity": "sha512-ylNlVsxuFjZK8DQtNUwiMskh6nT0vI7kYl/4fZgV1llP5d6+HIeL/vmmm3jpuoo8+NuXjQVZxmKuhDApK0/cKw==",
- "dev": true,
- "optional": true
- },
- "@esbuild/linux-s390x": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/linux-s390x/-/linux-s390x-0.16.17.tgz",
- "integrity": "sha512-gzy7nUTO4UA4oZ2wAMXPNBGTzZFP7mss3aKR2hH+/4UUkCOyqmjXiKpzGrY2TlEUhbbejzXVKKGazYcQTZWA/w==",
- "dev": true,
- "optional": true
- },
- "@esbuild/linux-x64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/linux-x64/-/linux-x64-0.16.17.tgz",
- "integrity": "sha512-mdPjPxfnmoqhgpiEArqi4egmBAMYvaObgn4poorpUaqmvzzbvqbowRllQ+ZgzGVMGKaPkqUmPDOOFQRUFDmeUw==",
- "dev": true,
- "optional": true
- },
- "@esbuild/netbsd-x64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/netbsd-x64/-/netbsd-x64-0.16.17.tgz",
- "integrity": "sha512-/PzmzD/zyAeTUsduZa32bn0ORug+Jd1EGGAUJvqfeixoEISYpGnAezN6lnJoskauoai0Jrs+XSyvDhppCPoKOA==",
- "dev": true,
- "optional": true
- },
- "@esbuild/openbsd-x64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/openbsd-x64/-/openbsd-x64-0.16.17.tgz",
- "integrity": "sha512-2yaWJhvxGEz2RiftSk0UObqJa/b+rIAjnODJgv2GbGGpRwAfpgzyrg1WLK8rqA24mfZa9GvpjLcBBg8JHkoodg==",
- "dev": true,
- "optional": true
- },
- "@esbuild/sunos-x64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.16.17.tgz",
- "integrity": "sha512-xtVUiev38tN0R3g8VhRfN7Zl42YCJvyBhRKw1RJjwE1d2emWTVToPLNEQj/5Qxc6lVFATDiy6LjVHYhIPrLxzw==",
- "dev": true,
- "optional": true
- },
- "@esbuild/win32-arm64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/win32-arm64/-/win32-arm64-0.16.17.tgz",
- "integrity": "sha512-ga8+JqBDHY4b6fQAmOgtJJue36scANy4l/rL97W+0wYmijhxKetzZdKOJI7olaBaMhWt8Pac2McJdZLxXWUEQw==",
- "dev": true,
- "optional": true
- },
- "@esbuild/win32-ia32": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/win32-ia32/-/win32-ia32-0.16.17.tgz",
- "integrity": "sha512-WnsKaf46uSSF/sZhwnqE4L/F89AYNMiD4YtEcYekBt9Q7nj0DiId2XH2Ng2PHM54qi5oPrQ8luuzGszqi/veig==",
- "dev": true,
- "optional": true
- },
- "@esbuild/win32-x64": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/@esbuild/win32-x64/-/win32-x64-0.16.17.tgz",
- "integrity": "sha512-y+EHuSchhL7FjHgvQL/0fnnFmO4T1bhvWANX6gcnqTjtnKWbTvUMCpGnv2+t+31d7RzyEAYAd4u2fnIhHL6N/Q==",
- "dev": true,
- "optional": true
- },
- "@microsoft/fast-element": {
- "version": "1.11.0",
- "resolved": "https://registry.npmjs.org/@microsoft/fast-element/-/fast-element-1.11.0.tgz",
- "integrity": "sha512-VKJYMkS5zgzHHb66sY7AFpYv6IfFhXrjQcAyNgi2ivD65My1XOhtjfKez5ELcLFRJfgZNAxvI8kE69apXERTkw=="
- },
- "@microsoft/fast-foundation": {
- "version": "2.47.0",
- "resolved": "https://registry.npmjs.org/@microsoft/fast-foundation/-/fast-foundation-2.47.0.tgz",
- "integrity": "sha512-EyFuioaZQ9ngjUNRQi8R3dIPPsaNQdUOS+tP0G7b1MJRhXmQWIitBM6IeveQA6ZvXG6H21dqgrfEWlsYrUZ2sw==",
- "requires": {
- "@microsoft/fast-element": "^1.11.0",
- "@microsoft/fast-web-utilities": "^5.4.1",
- "tabbable": "^5.2.0",
- "tslib": "^1.13.0"
- }
- },
- "@microsoft/fast-react-wrapper": {
- "version": "0.1.48",
- "resolved": "https://registry.npmjs.org/@microsoft/fast-react-wrapper/-/fast-react-wrapper-0.1.48.tgz",
- "integrity": "sha512-9NvEjru9Kn5ZKjomAMX6v+eF0DR+eDkxKDwDfi+Wb73kTbrNzcnmlwd4diN15ygH97kldgj2+lpvI4CKLQQWLg==",
- "requires": {
- "@microsoft/fast-element": "^1.9.0",
- "@microsoft/fast-foundation": "^2.41.1"
- }
- },
- "@microsoft/fast-web-utilities": {
- "version": "5.4.1",
- "resolved": "https://registry.npmjs.org/@microsoft/fast-web-utilities/-/fast-web-utilities-5.4.1.tgz",
- "integrity": "sha512-ReWYncndjV3c8D8iq9tp7NcFNc1vbVHvcBFPME2nNFKNbS1XCesYZGlIlf3ot5EmuOXPlrzUHOWzQ2vFpIkqDg==",
- "requires": {
- "exenv-es6": "^1.1.1"
- }
- },
- "@types/jquery": {
- "version": "3.5.16",
- "resolved": "https://registry.npmjs.org/@types/jquery/-/jquery-3.5.16.tgz",
- "integrity": "sha512-bsI7y4ZgeMkmpG9OM710RRzDFp+w4P1RGiIt30C1mSBT+ExCleeh4HObwgArnDFELmRrOpXgSYN9VF1hj+f1lw==",
- "dev": true,
- "requires": {
- "@types/sizzle": "*"
- }
- },
- "@types/node": {
- "version": "16.18.11",
- "resolved": "https://registry.npmjs.org/@types/node/-/node-16.18.11.tgz",
- "integrity": "sha512-3oJbGBUWuS6ahSnEq1eN2XrCyf4YsWI8OyCvo7c64zQJNplk3mO84t53o8lfTk+2ji59g5ycfc6qQ3fdHliHuA==",
- "dev": true
- },
- "@types/object-hash": {
- "version": "3.0.2",
- "resolved": "https://registry.npmjs.org/@types/object-hash/-/object-hash-3.0.2.tgz",
- "integrity": "sha512-tfyXl1JPCf2hzIDK29gO7qGqJjThKBzg/Cn3bA68R9NmWdOx+f7k5mm4to/n43BHspCwcoUC6FU4NpUoK/h9bQ==",
- "dev": true
- },
- "@types/prop-types": {
- "version": "15.7.5",
- "resolved": "https://registry.npmjs.org/@types/prop-types/-/prop-types-15.7.5.tgz",
- "integrity": "sha512-JCB8C6SnDoQf0cNycqd/35A7MjcnK+ZTqE7judS6o7utxUCg6imJg3QK2qzHKszlTjcj2cn+NwMB2i96ubpj7w==",
- "dev": true
- },
- "@types/react": {
- "version": "18.0.27",
- "resolved": "https://registry.npmjs.org/@types/react/-/react-18.0.27.tgz",
- "integrity": "sha512-3vtRKHgVxu3Jp9t718R9BuzoD4NcQ8YJ5XRzsSKxNDiDonD2MXIT1TmSkenxuCycZJoQT5d2vE8LwWJxBC1gmA==",
- "dev": true,
- "requires": {
- "@types/prop-types": "*",
- "@types/scheduler": "*",
- "csstype": "^3.0.2"
- }
- },
- "@types/react-dom": {
- "version": "18.0.10",
- "resolved": "https://registry.npmjs.org/@types/react-dom/-/react-dom-18.0.10.tgz",
- "integrity": "sha512-E42GW/JA4Qv15wQdqJq8DL4JhNpB3prJgjgapN3qJT9K2zO5IIAQh4VXvCEDupoqAwnz0cY4RlXeC/ajX5SFHg==",
- "dev": true,
- "requires": {
- "@types/react": "*"
- }
- },
- "@types/scheduler": {
- "version": "0.16.2",
- "resolved": "https://registry.npmjs.org/@types/scheduler/-/scheduler-0.16.2.tgz",
- "integrity": "sha512-hppQEBDmlwhFAXKJX2KnWLYu5yMfi91yazPb2l+lbJiwW+wdo1gNeRA+3RgNSO39WYX2euey41KEwnqesU2Jew==",
- "dev": true
- },
- "@types/sizzle": {
- "version": "2.3.3",
- "resolved": "https://registry.npmjs.org/@types/sizzle/-/sizzle-2.3.3.tgz",
- "integrity": "sha512-JYM8x9EGF163bEyhdJBpR2QX1R5naCJHC8ucJylJ3w9/CVBaskdQ8WqBf8MmQrd1kRvp/a4TS8HJ+bxzR7ZJYQ==",
- "dev": true
- },
- "@types/throttle-debounce": {
- "version": "5.0.0",
- "resolved": "https://registry.npmjs.org/@types/throttle-debounce/-/throttle-debounce-5.0.0.tgz",
- "integrity": "sha512-Pb7k35iCGFcGPECoNE4DYp3Oyf2xcTd3FbFQxXUI9hEYKUl6YX+KLf7HrBmgVcD05nl50LIH6i+80js4iYmWbw==",
- "dev": true
- },
- "@types/vscode": {
- "version": "1.73.0",
- "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.73.0.tgz",
- "integrity": "sha512-FhkfF7V3fj7S3WqXu7AxFesBLO3uMkdCPJJPbwyZXezv2xJ6xBWHYM2CmkkbO8wT9Fr3KipwxGGOoQRrYq7mHg==",
- "dev": true
- },
- "@types/vscode-webview": {
- "version": "1.57.1",
- "resolved": "https://registry.npmjs.org/@types/vscode-webview/-/vscode-webview-1.57.1.tgz",
- "integrity": "sha512-ghW5SfuDmsGDS2A4xkvGsLwDRNc3Vj5rS6rPOyPm/IryZuf3wceZKxgYaUoW+k9f0f/CB7y2c1rRsdOWZWn0PQ==",
- "dev": true
- },
- "@vscode/webview-ui-toolkit": {
- "version": "1.2.1",
- "resolved": "https://registry.npmjs.org/@vscode/webview-ui-toolkit/-/webview-ui-toolkit-1.2.1.tgz",
- "integrity": "sha512-ZpVqLxoFWWk8mmAN7jr1v9yjD6NGBIoflAedNSusmaViqwHZ2znKBwAwcumLOlNlqmST6QMkiTVys7O8rzfd0w==",
- "requires": {
- "@microsoft/fast-element": "^1.6.2",
- "@microsoft/fast-foundation": "^2.38.0",
- "@microsoft/fast-react-wrapper": "^0.1.18"
- }
- },
- "balanced-match": {
- "version": "1.0.2",
- "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.2.tgz",
- "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw=="
- },
- "brace-expansion": {
- "version": "2.0.1",
- "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-2.0.1.tgz",
- "integrity": "sha512-XnAIvQ8eM+kC6aULx6wuQiwVsnzsi9d3WxzV3FpWTGA19F621kwdbsAcFKXgKUHZWsy+mY6iL1sHTxWEFCytDA==",
- "requires": {
- "balanced-match": "^1.0.0"
- }
- },
- "csstype": {
- "version": "3.1.1",
- "resolved": "https://registry.npmjs.org/csstype/-/csstype-3.1.1.tgz",
- "integrity": "sha512-DJR/VvkAvSZW9bTouZue2sSxDwdTN92uHjqeKVm+0dAqdfNykRzQ95tay8aXMBAAPpUiq4Qcug2L7neoRh2Egw==",
- "dev": true
- },
- "esbuild": {
- "version": "0.16.17",
- "resolved": "https://registry.npmjs.org/esbuild/-/esbuild-0.16.17.tgz",
- "integrity": "sha512-G8LEkV0XzDMNwXKgM0Jwu3nY3lSTwSGY6XbxM9cr9+s0T/qSV1q1JVPBGzm3dcjhCic9+emZDmMffkwgPeOeLg==",
- "dev": true,
- "requires": {
- "@esbuild/android-arm": "0.16.17",
- "@esbuild/android-arm64": "0.16.17",
- "@esbuild/android-x64": "0.16.17",
- "@esbuild/darwin-arm64": "0.16.17",
- "@esbuild/darwin-x64": "0.16.17",
- "@esbuild/freebsd-arm64": "0.16.17",
- "@esbuild/freebsd-x64": "0.16.17",
- "@esbuild/linux-arm": "0.16.17",
- "@esbuild/linux-arm64": "0.16.17",
- "@esbuild/linux-ia32": "0.16.17",
- "@esbuild/linux-loong64": "0.16.17",
- "@esbuild/linux-mips64el": "0.16.17",
- "@esbuild/linux-ppc64": "0.16.17",
- "@esbuild/linux-riscv64": "0.16.17",
- "@esbuild/linux-s390x": "0.16.17",
- "@esbuild/linux-x64": "0.16.17",
- "@esbuild/netbsd-x64": "0.16.17",
- "@esbuild/openbsd-x64": "0.16.17",
- "@esbuild/sunos-x64": "0.16.17",
- "@esbuild/win32-arm64": "0.16.17",
- "@esbuild/win32-ia32": "0.16.17",
- "@esbuild/win32-x64": "0.16.17"
- }
- },
- "exenv-es6": {
- "version": "1.1.1",
- "resolved": "https://registry.npmjs.org/exenv-es6/-/exenv-es6-1.1.1.tgz",
- "integrity": "sha512-vlVu3N8d6yEMpMsEm+7sUBAI81aqYYuEvfK0jNqmdb/OPXzzH7QWDDnVjMvDSY47JdHEqx/dfC/q8WkfoTmpGQ=="
- },
- "jquery": {
- "version": "3.6.3",
- "resolved": "https://registry.npmjs.org/jquery/-/jquery-3.6.3.tgz",
- "integrity": "sha512-bZ5Sy3YzKo9Fyc8wH2iIQK4JImJ6R0GWI9kL1/k7Z91ZBNgkRXE6U0JfHIizZbort8ZunhSI3jw9I6253ahKfg=="
- },
- "js-tokens": {
- "version": "4.0.0",
- "resolved": "https://registry.npmjs.org/js-tokens/-/js-tokens-4.0.0.tgz",
- "integrity": "sha512-RdJUflcE3cUzKiMqQgsCu06FPu9UdIJO0beYbPhHN4k6apgJtifcoCtT9bcxOpYBtpD2kCM6Sbzg4CausW/PKQ=="
- },
- "loose-envify": {
- "version": "1.4.0",
- "resolved": "https://registry.npmjs.org/loose-envify/-/loose-envify-1.4.0.tgz",
- "integrity": "sha512-lyuxPGr/Wfhrlem2CL/UcnUc1zcqKAImBDzukY7Y5F/yQiNdko6+fRLevlw1HgMySw7f611UIY408EtxRSoK3Q==",
- "requires": {
- "js-tokens": "^3.0.0 || ^4.0.0"
- }
- },
- "lru-cache": {
- "version": "6.0.0",
- "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-6.0.0.tgz",
- "integrity": "sha512-Jo6dJ04CmSjuznwJSS3pUeWmd/H0ffTlkXXgwZi+eq1UCmqQwCh+eLsYOYCwY991i2Fah4h1BEMCx4qThGbsiA==",
- "requires": {
- "yallist": "^4.0.0"
- }
- },
- "minimatch": {
- "version": "5.1.6",
- "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-5.1.6.tgz",
- "integrity": "sha512-lKwV/1brpG6mBUFHtb7NUmtABCb2WZZmm2wNiOA5hAb8VdCS4B3dtMWyvcoViccwAW/COERjXLt0zP1zXUN26g==",
- "requires": {
- "brace-expansion": "^2.0.1"
- }
- },
- "object-hash": {
- "version": "3.0.0",
- "resolved": "https://registry.npmjs.org/object-hash/-/object-hash-3.0.0.tgz",
- "integrity": "sha512-RSn9F68PjH9HqtltsSnqYC1XXoWe9Bju5+213R98cNGttag9q9yAOTzdbsqvIa7aNm5WffBZFpWYr2aWrklWAw=="
- },
- "prettier": {
- "version": "2.8.1",
- "resolved": "https://registry.npmjs.org/prettier/-/prettier-2.8.1.tgz",
- "integrity": "sha512-lqGoSJBQNJidqCHE80vqZJHWHRFoNYsSpP9AjFhlhi9ODCJA541svILes/+/1GM3VaL/abZi7cpFzOpdR9UPKg==",
- "dev": true
- },
- "react": {
- "version": "18.2.0",
- "resolved": "https://registry.npmjs.org/react/-/react-18.2.0.tgz",
- "integrity": "sha512-/3IjMdb2L9QbBdWiW5e3P2/npwMBaU9mHCSCUzNln0ZCYbcfTsGbTJrU/kGemdH2IWmB2ioZ+zkxtmq6g09fGQ==",
- "requires": {
- "loose-envify": "^1.1.0"
- }
- },
- "react-dom": {
- "version": "18.2.0",
- "resolved": "https://registry.npmjs.org/react-dom/-/react-dom-18.2.0.tgz",
- "integrity": "sha512-6IMTriUmvsjHUjNtEDudZfuDQUoWXVxKHhlEGSk81n4YFS+r/Kl99wXiwlVXtPBtJenozv2P+hxDsw9eA7Xo6g==",
- "requires": {
- "loose-envify": "^1.1.0",
- "scheduler": "^0.23.0"
- }
- },
- "scheduler": {
- "version": "0.23.0",
- "resolved": "https://registry.npmjs.org/scheduler/-/scheduler-0.23.0.tgz",
- "integrity": "sha512-CtuThmgHNg7zIZWAXi3AsyIzA3n4xx7aNyjwC2VJldO2LMVDhFK+63xGqq6CsJH4rTAt6/M+N4GhZiDYPx9eUw==",
- "requires": {
- "loose-envify": "^1.1.0"
- }
- },
- "semver": {
- "version": "7.5.3",
- "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.3.tgz",
- "integrity": "sha512-QBlUtyVk/5EeHbi7X0fw6liDZc7BBmEaSYn01fMU1OUYbf6GPsbTtd8WmnqbI20SeycoHSeiybkE/q1Q+qlThQ==",
- "requires": {
- "lru-cache": "^6.0.0"
- }
- },
- "tabbable": {
- "version": "5.3.3",
- "resolved": "https://registry.npmjs.org/tabbable/-/tabbable-5.3.3.tgz",
- "integrity": "sha512-QD9qKY3StfbZqWOPLp0++pOrAVb/HbUi5xCc8cUo4XjP19808oaMiDzn0leBY5mCespIBM0CIZePzZjgzR83kA=="
- },
- "throttle-debounce": {
- "version": "5.0.0",
- "resolved": "https://registry.npmjs.org/throttle-debounce/-/throttle-debounce-5.0.0.tgz",
- "integrity": "sha512-2iQTSgkkc1Zyk0MeVrt/3BvuOXYPl/R8Z0U2xxo9rjwNciaHDG3R+Lm6dh4EeUci49DanvBnuqI6jshoQQRGEg=="
- },
- "tslib": {
- "version": "1.14.1",
- "resolved": "https://registry.npmjs.org/tslib/-/tslib-1.14.1.tgz",
- "integrity": "sha512-Xni35NKzjgMrwevysHTCArtLDpPvye8zV/0E4EyYn43P7/7qvQwPh9BGkHewbMulVntbigmcT7rdX3BNo9wRJg=="
- },
- "typescript": {
- "version": "4.9.4",
- "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.4.tgz",
- "integrity": "sha512-Uz+dTXYzxXXbsFpM86Wh3dKCxrQqUcVMxwU54orwlJjOpO3ao8L7j5lH+dWfTwgCwIuM9GQ2kvVotzYJMXTBZg==",
- "dev": true
- },
- "vscode-jsonrpc": {
- "version": "8.1.0",
- "resolved": "https://registry.npmjs.org/vscode-jsonrpc/-/vscode-jsonrpc-8.1.0.tgz",
- "integrity": "sha512-6TDy/abTQk+zDGYazgbIPc+4JoXdwC8NHU9Pbn4UJP1fehUyZmM4RHp5IthX7A6L5KS30PRui+j+tbbMMMafdw=="
- },
- "vscode-languageclient": {
- "version": "8.1.0",
- "resolved": "https://registry.npmjs.org/vscode-languageclient/-/vscode-languageclient-8.1.0.tgz",
- "integrity": "sha512-GL4QdbYUF/XxQlAsvYWZRV3V34kOkpRlvV60/72ghHfsYFnS/v2MANZ9P6sHmxFcZKOse8O+L9G7Czg0NUWing==",
- "requires": {
- "minimatch": "^5.1.0",
- "semver": "^7.3.7",
- "vscode-languageserver-protocol": "3.17.3"
- }
- },
- "vscode-languageserver-protocol": {
- "version": "3.17.3",
- "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.17.3.tgz",
- "integrity": "sha512-924/h0AqsMtA5yK22GgMtCYiMdCOtWTSGgUOkgEDX+wk2b0x4sAfLiO4NxBxqbiVtz7K7/1/RgVrVI0NClZwqA==",
- "requires": {
- "vscode-jsonrpc": "8.1.0",
- "vscode-languageserver-types": "3.17.3"
- }
- },
- "vscode-languageserver-types": {
- "version": "3.17.3",
- "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.17.3.tgz",
- "integrity": "sha512-SYU4z1dL0PyIMd4Vj8YOqFvHu7Hz/enbWtpfnVbJHU4Nd1YNYx8u0ennumc6h48GQNeOLxmwySmnADouT/AuZA=="
- },
- "yallist": {
- "version": "4.0.0",
- "resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz",
- "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A=="
- }
}
}
diff --git a/editor/code/package.json b/editor/code/package.json
index 273aa811..009d99ed 100644
--- a/editor/code/package.json
+++ b/editor/code/package.json
@@ -11,7 +11,7 @@
],
"publisher": "ejgallego",
"engines": {
- "vscode": "^1.73.0"
+ "vscode": "^1.75.0"
},
"categories": [
"Programming Languages",
@@ -28,9 +28,6 @@
"type": "git",
"url": "https://github.com/ejgallego/coq-lsp"
},
- "activationEvents": [
- "onLanguage:coq"
- ],
"contributes": {
"languages": [
{
@@ -281,7 +278,7 @@
},
"devDependencies": {
"@types/jquery": "^3.5.16",
- "@types/node": "^16.11.7",
+ "@types/node": "^18.11.9",
"@types/object-hash": "^3.0.2",
"@types/react": "^18.0.27",
"@types/react-dom": "^18.0.10",
@@ -289,12 +286,12 @@
"@types/vscode": "^1.73.0",
"@types/vscode-webview": "^1.57.1",
"esbuild": "^0.16.17",
- "prettier": "^2.8.1",
- "typescript": "^4.9.4"
+ "prettier": "^3.0.0",
+ "typescript": "^5.1.6"
},
"dependencies": {
"@vscode/webview-ui-toolkit": "^1.2.1",
- "jquery": "^3.6.3",
+ "jquery": "^3.7.0",
"object-hash": "^3.0.0",
"react": "^18.2.0",
"react-dom": "^18.2.0",
diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts
index b4ecd217..405ea840 100644
--- a/editor/code/src/goals.ts
+++ b/editor/code/src/goals.ts
@@ -127,7 +127,11 @@ export class InfoPanel {
version
);
let cursor: GoalRequest = { textDocument, position };
- let strCursor: GoalRequest = { textDocument, position, pp_format: "Str" };
+ let strCursor: GoalRequest = {
+ textDocument,
+ position,
+ pp_format: "Str",
+ };
this.sendGoalsRequest(client, cursor);
let vizx = extensions.getExtension("inQWIRE.vizx");
if (vizx?.isActive) {
diff --git a/editor/code/views/info/CoqPp.tsx b/editor/code/views/info/CoqPp.tsx
index 5fec96c1..b4f42ccf 100644
--- a/editor/code/views/info/CoqPp.tsx
+++ b/editor/code/views/info/CoqPp.tsx
@@ -23,14 +23,18 @@ export function CoqPp({
return (
);
} else {
let rendered = FormatPrettyPrint.pp2DOM(content, "vertical");
return (
);
}
diff --git a/editor/code/views/info/media/coqpp.css b/editor/code/views/info/media/coqpp.css
index 1fcb0ff1..0b5f9e7f 100644
--- a/editor/code/views/info/media/coqpp.css
+++ b/editor/code/views/info/media/coqpp.css
@@ -64,10 +64,14 @@ div.Pp_box:not([data-mode="vertical"]) > .Pp_break:not(.br) > span.prev-indent {
color: #aabb22;
}
-.constr\.variable {
+body.vscode-dark .constr\.variable {
color: #7fbfff;
}
+body.vscode-light .constr\.variable {
+ color: #007bff;
+}
+
.module\.definition {
color: #777ddd;
}
@@ -80,14 +84,22 @@ div.Pp_box:not([data-mode="vertical"]) > .Pp_break:not(.br) > span.prev-indent {
color: #9674b8;
}
-.tactic\.primitive {
+body.vscode-dark .tactic\.primitive {
color: #c0c0c0;
}
-.tactic\.string {
+body.vscode-light .tactic\.primitive {
+ color: #5c5b5b;
+}
+
+body.vscode-dark .tactic\.string {
color: #99ff99;
}
+body.vscode-light .tactic\.string {
+ color: #71ba71;
+}
+
.constr\.reference:hover,
.constr\.type:hover,
.constr\.variable:hover,
diff --git a/editor/code/views/perf/App.tsx b/editor/code/views/perf/App.tsx
index e0615508..95090348 100644
--- a/editor/code/views/perf/App.tsx
+++ b/editor/code/views/perf/App.tsx
@@ -5,7 +5,7 @@ import {
VSCodeDataGridRow,
VSCodeDataGridCell,
} from "@vscode/webview-ui-toolkit/react";
-import "./App.css";
+import "./media/App.css";
import { Range } from "vscode-languageserver-types";
import { DocumentPerfParams } from "../../lib/types";
diff --git a/editor/code/views/perf/App.css b/editor/code/views/perf/media/App.css
similarity index 100%
rename from editor/code/views/perf/App.css
rename to editor/code/views/perf/media/App.css
diff --git a/etc/release_notes/v0.1.7.md b/etc/release_notes/v0.1.7.md
index 77e5c093..46b7f36c 100644
--- a/etc/release_notes/v0.1.7.md
+++ b/etc/release_notes/v0.1.7.md
@@ -12,8 +12,9 @@ like to thank all the users and contributors for their feedback and
work, and in particular Alex Sanchez-Stern who did a large amount of
beta testing and tweaks.
-Following a suggestion by Hugo Herbelin, we now follow a naming
-scheme reminiscent of Isabelle's:
+Following a suggestion by Hugo Herbelin, we now follow a naming scheme
+reminiscent of Isabelle's to distinguish the several `coq-lsp`
+components:
- `coq-lsp` refers to the Coq LSP server
@@ -26,11 +27,12 @@ This release also ships with some new features:
command line compiler that provides direct access to `coq-lsp`
internal checking engine (Flèche). A very preliminary plugin API for
Flèche is also available. `fcc` does understand Coq markdown files
- (`.mv`), and can use the programmable error recovery mode from
- Flèche, etc...
+ (`.mv`), produces errors and output in a machine-friendly format
+ (JSON), can use the programmable error recovery mode from Flèche,
+ etc...
-- Coq Markdown files (`.mv`) are now regular Markdown files in
- `coq-lsp/VSCode`, thus one can do live proofs and use standard
+- Coq Markdown files (`.mv`) are now handled as regular Markdown files
+ in `coq-lsp/VSCode`, thus one can do live proofs and use standard
Markdown mode commands like preview at the same time (contributed by
@4ever2)
@@ -44,8 +46,8 @@ This release also ships with some new features:
it can run on the Browser context, full support is expected in the
next release.
-- A new notification for performance data has been added to server,
- and a prototype panel displaying this data is now available for
+- A new notification for performance data has been added to server.
+ A prototype panel displaying this data is now available for
`coq-lsp/VSCode`.
`coq-lsp` release notes are archived at [1]
@@ -120,7 +122,7 @@ Please find below the full list of changes:
[1] https://github.com/ejgallego/coq-lsp/tree/main/etc/release_notes
[2] https://github.com/inQWIRE/ViZX
[3] https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp/topic/coq-lsp.20under.20Emacs.2E
-[4] https://github.com/pcarrott/coq-lsp-pyclient
+[4] https://github.com/sr-lab/coq-lsp-pyclient
Kind regards,
The coq-lsp team
diff --git a/examples/Ltac2_plugin.v b/examples/Ltac2_plugin.v
new file mode 100644
index 00000000..8d362775
--- /dev/null
+++ b/examples/Ltac2_plugin.v
@@ -0,0 +1,7 @@
+Require Export Ltac2.Notations.
+
+Print nat.
+
+Ltac2 test1 () := refine '(id _).
+
+Ltac2 test () := refine '(id _).
\ No newline at end of file
diff --git a/examples/coreact.mv b/examples/coreact.mv
index 5c19fabe..c8d89c1b 100644
--- a/examples/coreact.mv
+++ b/examples/coreact.mv
@@ -29,7 +29,7 @@ Record Category := {
}.
```
-### Error recover
+### Error recovery
```coq
Lemma addnC n m : n + m = m + n.
diff --git a/examples/display_large.v b/examples/display_large.v
new file mode 100644
index 00000000..9698c4dd
--- /dev/null
+++ b/examples/display_large.v
@@ -0,0 +1,17 @@
+Require Import ZArith.
+
+Open Scope Z.
+
+Goal 2^17000 <> 0.
+Time cbv.
+(* This computes in a few ms, but display takes 15s in CoqIDE and VSCoq *)
+congruence.
+Qed.
+
+Definition hideZ {z : Z} := z.
+Opaque hideZ.
+
+Goal @hideZ (2^17000) <> 0.
+Time cbv.
+(* This computes in a few ms and displays immediately in CoqIDE and VSCoq if implicit arguments are off *)
+Abort.
diff --git a/lsp/doc.ml b/lsp/doc.ml
index e7c34d42..27490f19 100644
--- a/lsp/doc.ml
+++ b/lsp/doc.ml
@@ -17,8 +17,10 @@ module TextDocumentItem = struct
[@@deriving yojson]
end
+(* Sometimes we use this to parse VersionedTextDocumentIdentifier, we use {
+ strict = false } as a quick fix *)
module TextDocumentIdentifier = struct
- type t = { uri : Lang.LUri.File.t } [@@deriving yojson]
+ type t = { uri : Lang.LUri.File.t } [@@deriving yojson { strict = false }]
end
module OVersionedTextDocumentIdentifier = struct
diff --git a/test/CoqProject/_CoqProject b/test/CoqProject/_CoqProject
index 1f555a69..da0de778 100644
--- a/test/CoqProject/_CoqProject
+++ b/test/CoqProject/_CoqProject
@@ -2,5 +2,6 @@
-Q . test
-arg -w -arg -local-declaration
+-arg -w -arg +non-primitive-record
test.v
diff --git a/test/CoqProject/test.v b/test/CoqProject/test.v
index 11151b3d..ea6b2bcf 100644
--- a/test/CoqProject/test.v
+++ b/test/CoqProject/test.v
@@ -1 +1,7 @@
Variable (A : nat).
+
+Set Primitive Projections.
+
+Record a := { _ : nat }.
+
+Print Options.
diff --git a/test/compiler/dune b/test/compiler/dune
index 7a63250c..c485508b 100644
--- a/test/compiler/dune
+++ b/test/compiler/dune
@@ -2,4 +2,6 @@
(deps
(source_tree proj1)
(source_tree proj2)
+ ; For the plugins to be built
+ (package coq-lsp)
%{bin:fcc}))
diff --git a/test/compiler/run.t b/test/compiler/run.t
index a445e664..aa2855e4 100644
--- a/test/compiler/run.t
+++ b/test/compiler/run.t
@@ -1,6 +1,7 @@
General tests for the Flèche Compiler
Describe the project
+ $ export FCC_TEST=true
$ fcc --root proj1
[message] Configuration loaded from Command-line arguments
- coqlib is at: [TEST_PATH]
diff --git a/test/server/package-lock.json b/test/server/package-lock.json
index 66731a8c..e7ba7a2c 100644
--- a/test/server/package-lock.json
+++ b/test/server/package-lock.json
@@ -2283,9 +2283,10 @@
}
},
"node_modules/jest-snapshot/node_modules/semver": {
- "version": "7.3.8",
+ "version": "7.5.4",
+ "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz",
+ "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==",
"dev": true,
- "license": "ISC",
"dependencies": {
"lru-cache": "^6.0.0"
},
@@ -2811,9 +2812,10 @@
}
},
"node_modules/semver": {
- "version": "6.3.0",
+ "version": "6.3.1",
+ "resolved": "https://registry.npmjs.org/semver/-/semver-6.3.1.tgz",
+ "integrity": "sha512-BR7VvDCVHO+q2xBEWskxS6DJE1qRnb7DxzUrogb71CWoSficBxYsiAGd+Kl0mmq/MprG9yArRkyrQxTO6XjMzA==",
"dev": true,
- "license": "ISC",
"bin": {
"semver": "bin/semver.js"
}
@@ -3072,9 +3074,10 @@
}
},
"node_modules/ts-jest/node_modules/semver": {
- "version": "7.3.8",
+ "version": "7.5.4",
+ "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz",
+ "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==",
"dev": true,
- "license": "ISC",
"dependencies": {
"lru-cache": "^6.0.0"
},