Merge pull request #433 from ejgallego/js

[controller] [js] Initial javascript JSSO controller

.github/workflows/build.yml

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

.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

@@ -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
 -----------------------------------

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= \
@@ -47,6 +49,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 +59,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 +77,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: vendor/coq/config/coq_config.ml
 
@@ -134,3 +146,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

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`