From 4f307fd000fb81ca38d6b25affe4e1c3c11fe72f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Sep 2024 17:38:37 +0200 Subject: [PATCH] [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 +