Merge pull request #881 from ejgallego/update_jsoo

[js worker] Update js_of_ocaml to 5.9.1 and Coq -> Roqc / stdlib split

.github/workflows/build.yml

@@ -115,9 +115,10 @@ jobs:
 
       - name: 🐫🐪🐫 Get dependencies
         run: |
+          opam update
           opam exec -- make opam-deps
-          opam pin add js_of_ocaml-compiler --dev -y
-          opam pin add js_of_ocaml --dev -y
+          opam pin add js_of_ocaml-compiler -k version 5.9.1 -y
+          opam pin add js_of_ocaml -k version 5.9.1 -y
           opam install zarith_stubs_js js_of_ocaml-ppx -y
 
       - name: 💉💉💉 Patch Coq

CHANGES.md

@@ -4,6 +4,13 @@
  - [fleche] fix quick fixes for errors being lost due to incorrect
    handling of `send_diags_extra_data` (@ejgallego, #850)
  - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)
+ - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, #879)
+ - [js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo
+   Heuzard for longstanding continued support of the jsCoq and coq-lsp
+   projects (@ejgallego, @hhugo, #881)
+ - [js worker] Update stubs (@ejgallego, @hhugo, #881)
+ - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
+   (@ejgallego, #881)
 
 # coq-lsp 0.2.2: To Virtual or not To Virtual
 ---------------------------------------------

controller-js/coq_lsp_worker.ml

@@ -132,7 +132,7 @@ let coq_init ~debug =
   let vm, warnings = (false, Some "-vm-compute-disabled") in
   Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings })
 
-external coq_vm_trap : unit -> unit = "coq_vm_trap"
+external rocq_vm_trap : unit -> unit = "rocq_vm_trap"
 
 (* This code is executed on Worker initialization *)
 let main () =
@@ -146,15 +146,15 @@ let main () =
   setup_std_printers ();
 
   (* setup_interp (); *)
-  coq_vm_trap ();
+  rocq_vm_trap ();
 
   Lsp.Io.set_log_fn (fun n -> Lsp.Base.Message.notification n |> post_message);
   let io = CB.cb in
   Fleche.Io.CallBack.set io;
 
   let stdlib coqlib =
     let unix_path = Filename.concat coqlib "theories" in
-    let coq_path = Names.(DirPath.make [ Id.of_string "Stdlib" ]) in
+    let coq_path = Names.(DirPath.make [ Id.of_string "Corelib" ]) in
     Loadpath.{ unix_path; coq_path; implicit = true; recursive = true }
   in
 
@@ -176,7 +176,7 @@ let main () =
       ; ocamlpath
       ; vo_load_path
       ; ml_include_path = []
-      ; require_libraries = [ (None, "Stdlib.Init.Prelude") ]
+      ; require_libraries = [ (None, "Corelib.Init.Prelude") ]
       ; args = [ "-noinit"; "-boot" ]
       }
   in

controller-js/dune

@@ -30,7 +30,7 @@
    ; --file=%{dep:coq-fs}
    --setenv
    PATH=/bin))
- (link_flags -linkall -no-check-prims)
+ (link_flags -no-check-prims)
  ; The old makefile set: -noautolink -no-check-prims
  (libraries
   zarith_stubs_js