[ci] [js] Build JS worker on CI.

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

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

etc/0001-coq-lsp-patch.patch

@@ -0,0 +1,59 @@
+From aa1c239f64a703785d9c4a520eee3aa4f97fa3ba Mon Sep 17 00:00:00 2001
+From: Emilio Jesus Gallego Arias <e+git@x80.org>
+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 <caml/mlvalues.h>
++
++// jsCoq Stub; actual implementation is in backend/jsoo/js_stub/interrupt.js
++value interrupt_pending() { return Val_false; }
+-- 
+2.43.0
+

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 <e+git@x80.org>
+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
+