Merge branch 'main' into v8.20

.github/workflows/build.yml

@@ -60,7 +60,7 @@ jobs:
 
     steps:
       - name: 🔭 Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
 
@@ -83,14 +83,77 @@ jobs:
       - name: 🐛 Test fcc
         run: opam exec -- make test-compiler
 
+  build-js:
+    name: Web Worker Build
+    strategy:
+      fail-fast: false
+    runs-on: ubuntu-latest
+
+    steps:
+      # OPAM figures out everything but the libgmp-dev:i386
+      # dependency, maybe worth fixing this upstream in the opam
+      # repository
+      - name: Install apt dependencies
+        run: |
+          sudo apt-get install aptitude
+          sudo dpkg --add-architecture i386
+          sudo aptitude -o Acquire::Retries=30 update -q
+          sudo aptitude -o Acquire::Retries=30 install gcc-multilib g++-multilib pkg-config libgmp-dev libgmp-dev:i386 -y
+
+      - name: 🔭 Checkout code
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: 🐫 Setup OCaml
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: "ocaml-variants.4.14.2+options,ocaml-option-32bit"
+          dune-cache: true
+
+      - name: 🐫🐪🐫 Get dependencies
+        run: |
+          opam exec -- make opam-deps
+          opam pin add js_of_ocaml-compiler https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y
+          opam pin add js_of_ocaml https://github.com/ejgallego/js_of_ocaml.git#fix_build_fs_target -y
+          opam install zarith_stubs_js js_of_ocaml-ppx -y
+
+      - name: 💉💉💉 Patch Coq
+        run: make patch-for-js
+
+      - name: 🦏🧱🦏 Build coq-lsp JS version 🦏🦏🦏
+        run: |
+          opam exec -- make controller-js/coq-fs-core.js
+          opam exec -- make js
+
+      - name: 🚀 Setup node
+        uses: actions/setup-node@v4
+        with:
+          node-version: 22
+
+      - name: 🦏🧱🦏 Build coq-lsp VSCode extension 🦏🦏🦏
+        run: opam exec -- make extension
+
+      - name: Upload artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: coq-lsp_worker and front-end
+          path: |
+            editor/code/package.json
+            editor/code/README.md
+            editor/code/CHANGELOG.md
+            editor/code/syntaxes
+            editor/code/out/
+            editor/code/coq.configuration.json
+          compression-level: 9
   build-opam:
     name: Opam install
     strategy:
       fail-fast: false
     runs-on: ubuntu-latest
     steps:
       - name: 🔭 Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
 
@@ -122,11 +185,11 @@ jobs:
         working-directory: ./editor/code
     steps:
       - name: 🔭 Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: 🚀 Setup node
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
-          node-version: 18
+          node-version: 22
       - run: npm ci
       - run: npx --yes @vscode/vsce ls
 
@@ -135,7 +198,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: 🔭 Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: recursive
       - name: ❄️ Setup Nix

.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/

CHANGES.md

@@ -1,3 +1,40 @@
+# unreleased
+------------
+
+ - [deps] Bump toolchain so minimal `ppxlib` is 0.26, in order to fix
+   some `ppx_import` oddities. This means our lower bound for the Jane
+   Street packages is now `v0.15`, which should be fine for the
+   foreseeable future (@ejgallego, #813)
+ - [workspace] [coq] Support _CoqProject arguments `-type-in-type` and
+   `-allow-rewrite-rules` (for 8.20) (@ejgallego, #819)
+ - [serlib] Support for ltac2_ltac1 plugin (@ejgallego, #820)
+ - [serlib] Fix Ltac2 AST piercing bug, add test case that should help
+   in the future (@ejgallego, @jim-portegies, #821)
+ - [fleche] [8.20] understand rewrite rules and symbols on document
+   outline (@ejgallego, @Alizter, #825, fixes #824)
+ - [fleche] [coq] support `Restart` meta command (@ejgallego,
+   @Alizter, #828, fixes #827)
+ - [fleche] [plugins] New plugin example `explain_errors`, that will
+   print all errors on a file, with their goal context (@ejgallego,
+   #829, thanks to @gmalecha for the idea, c.f. Coq issue 19601)
+ - [fleche] Highlight the full first line of the document on
+   initialization error (@ejgallego, #832)
+ - [fleche] [jscoq] [js] Build worker version of `coq-lsp`. This
+   provides a full working Coq enviroment in `vscode.dev`. The web
+   worker version is build as an artifact on CI (@ejgallego
+   @corwin-of-amber, #433)
+ - [hover] Fix universe and level printing in hover (#839, fixes #835
+   , @ejgallego , @Alizter)
+ - [fleche] New immediate request serving mode. In this mode, requests
+   are served with whatever document state we have. This is very
+   useful when we are not in continuous mode, and we don't have a good
+   reference as to what to build, for example in
+   `documentSymbols`. The mode actually works pretty well in practice
+   as often language requests will come after goals requests, so the
+   info that is needed is at hand. It could also be tried to set the
+   build target for immediate requests to the view hint, but we should
+   see some motivation for that (@ejgallego, #841)
+
 # coq-lsp 0.2.0: From Green to Blue
 -----------------------------------
 

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

Makefile

@@ -1,3 +1,5 @@
+SHELL := /usr/bin/env bash
+
 COQ_BUILD_CONTEXT=../_build/default/coq
 
 PKG_SET= coq-lsp.install
@@ -44,6 +46,8 @@ build-all: coq_boot
 vendor/coq:
 	$(error Submodules not initialized, please do "make submodules-init")
 
+COQVM=yes
+
 # We set -libdir due to a Coq bug on win32, see
 # https://github.com/coq/coq/pull/17289 , this can be removed once we
 # drop support for Coq 8.16
@@ -52,6 +56,7 @@ vendor/coq/config/coq_config.ml: vendor/coq
 	&& cd vendor/coq \
 	&& ./configure -no-ask -prefix "$$EPATH/_build/install/default/" \
 	        -libdir "$$EPATH/_build/install/default/lib/coq" \
+	        -bytecode-compiler $(COQVM) \
 		-native-compiler no \
 	&& cp theories/dune.disabled theories/dune \
 	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
@@ -69,6 +74,13 @@ winconfig:
 	&& cp theories/dune.disabled theories/dune \
 	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
 
+
+.PHONY: js
+js: COQVM = no
+js: coq_boot
+	dune build --profile=release --display=quiet $(PKG_SET) controller-js/coq_lsp_worker.bc.cjs
+	mkdir -p editor/code/out/ && cp -a controller-js/coq_lsp_worker.bc.cjs editor/code/out/coq_lsp_worker.bc.js
+
 .PHONY: coq_boot
 coq_boot:
 # We do nothing for released versions
@@ -133,3 +145,54 @@ 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
+
+_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

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

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)

controller-js/README.md

@@ -0,0 +1,84 @@
+## coq-lsp Web Worker README
+
+This directory contains the implementation of our LSP-compliant web
+worker for Coq, based on jsCoq.
+
+As you can see the implementation is minimal, thanks to proper
+abstraction of the core of the controller.
+
+For now it is only safe to use the worker in 32bit OCaml mode.
+
+Support for this build is still experimental. See [the javascript
+compilation
+meta-issue](https://github.com/ejgallego/coq-lsp/issues/833) for more
+information.
+
+## Building the Worker
+
+The worker needs two parts to work:
+
+- the worker binary
+- the worker OCaml filesystem (`controller-js/coq-fs-core.js`)
+- the worker Coq filesystem (`controller-js/coq-fs.js`)
+
+which are then bundled in a single `.js` file.
+
+The worker OCaml filesystem includes:
+- `META` files for anything used by Coq
+- transpiled `.cma` to `.js` files for plugins that will be loaded by Coq
+
+Type:
+
+```
+make patch-for-js                 # (only once, patch Coq for JS build)
+make controller-js/coq-fs-core.js # build the OCaml filesystem, needed when plugins change
+make js                           # build the worker and link with the FS.
+```
+to get a working build in `editor/code/out`.
+
+As of now the build is very artisanal and not flexible at all, we hope to improve it soon.
+
+## Testing the worker
+
+You can test the server using any of the [official methods](https://code.visualstudio.com/api/extension-guides/web-extensions#test-your-web-extension).
+
+Using the regular setup `dune exec -- code editor/code` and then
+selecting "Web Extension" in the run menu works out of the box.
+
+A quick recipe from the manual is:
+
+```
+$ make controller-js/coq-fs-core.js && make js
+$ npx @vscode/test-web --browser chromium --extensionDevelopmentPath=editor/code
+$ chrome localhost:3000
+```
+
+you can also download the artifacts from the CI build, and point
+`--extensionDevelopmentPath=` to the path you have downloaded the
+extension + Coq build.
+
+## COI
+
+As of Feb 2023, due to security restrictions, you may need to either:
+
+ - pass `--enable-coi` to `code`
+ - use ``?enable-coi=` in the vscode dev setup
+
+in order to have interruptions (`SharedBufferArray`) working.
+
+See https://code.visualstudio.com/updates/v1_72#_towards-cross-origin-isolation
+
+## WASM
+
+We hope to have a WASM backend working soon, based on waCoq, see
+https://github.com/microsoft/vscode-wasm
+
+## Filesystem layout
+
+We need to have most `META` files in findlib, plus the Coq and
+`coq-lsp.serlib.*` plugins. These should be precompiled.
+
+- `/static/lib`: OCaml findlib root
+- `/static/coqlib`: Coq root, with regular paths
+  + `/static/coqlib/theories`
+  + `/static/coqlib/user-contrib`