Merge pull request #883 from SkySkimmer/rocq-cli

Adapt to coq/coq#19927 (coq-core renamed to rocq-runtime)

.github/workflows/build.yml

@@ -170,7 +170,7 @@ jobs:
         run: |
           opam install lwt logs # Also build pet-server
           opam install memprof-limits # We need to do this to avoid coq-lsp rebuilding Coq below due to deptops
-          opam install vendor/coq/{coq-core,rocq-core,stdlib/coq-stdlib,coqide-server,coq}.opam
+          opam install vendor/coq/{rocq-runtime,coq-core,rocq-core,stdlib/coq-stdlib,coqide-server,coq}.opam
 
       - name: Install `coq-lsp` into OPAM switch
         run: opam install .

.gitmodules

@@ -1,3 +1,3 @@
 [submodule "coq"]
 	path = vendor/coq
-	url = https://github.com/coq/coq.git
+	url = https://github.com/skyskimmer/coq.git

CHANGES.md

@@ -11,6 +11,8 @@
  - [js worker] Update stubs (@ejgallego, @hhugo, #881)
  - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
    (@ejgallego, #881)
+ - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
+   #883)
 
 # coq-lsp 0.2.2: To Virtual or not To Virtual
 ---------------------------------------------

Makefile

@@ -3,7 +3,7 @@ SHELL := /usr/bin/env bash
 COQ_BUILD_CONTEXT=../_build/default/coq
 
 PKG_SET= \
-vendor/coq/coq-core.install \
+vendor/coq/rocq-runtime.install \
 vendor/coq/rocq-core.install \
 vendor/coq/stdlib/coq-stdlib.install \
 coq-lsp.install
@@ -146,7 +146,7 @@ make-fmt: build fmt
 .PHONY: opam-update-and-reinstall
 opam-update-and-reinstall:
 	git pull --recurse-submodules
-	for pkg in coq-core rocq-core stdlib/coq-stdlib coqide-server coq; do opam install -y vendor/coq/$$pkg.opam; done
+	for pkg in rocq-runtime coq-core rocq-core stdlib/coq-stdlib coqide-server coq; do opam install -y vendor/coq/$$pkg.opam; done
 	opam install .
 
 .PHONY: patch-for-js
@@ -160,12 +160,12 @@ _LIBROOT=$(shell opam var lib)
 VENDORED_SETUP:=true
 
 ifdef VENDORED_SETUP
-_CCROOT=_build/install/default/lib/coq-core
+_CCROOT=_build/install/default/lib/rocq-runtime
 else
 # We could use `opam var lib` as well here, as the idea to rely on
 # coqc was to avoid having a VENDORED_SETUP variable, which we now
 # have anyways.
-_CCROOT=$(shell coqc -where)/../coq-core
+_CCROOT=$(shell coqc -where)/../rocq-runtime
 endif
 
 # Super-hack
@@ -175,7 +175,7 @@ controller-js/coq-fs-core.js: coq_boot
 	for i in $$(find $(_CCROOT)/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
 	js_of_ocaml build-fs -o controller-js/coq-fs-core.js \
-	    $$(find $(_CCROOT)/                          \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/coq-core/%P ") \
+	    $$(find $(_CCROOT)/                          \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/rocq-runtime/%P ") \
 	    $$(find _build/install/default/lib/coq-lsp/  \( -wholename '*/serlib/*/*.js'  -or -wholename '*/META' \) -printf "%p:/static/lib/coq-lsp/%P ") \
 	    ./etc/META.threads:/static/lib/threads/META \
 	    $$(find $(_LIBROOT) -wholename '*/str/META'                 -printf "%p:/static/lib/%P ") \

controller-js/coq_lsp_worker.ml

@@ -171,7 +171,7 @@ let main () =
     let vo_load_path = List.map (fun f -> f coqlib) [ stdlib; user_contrib ] in
     Coq.Workspace.CmdLine.
       { coqlib
-      ; coqcorelib = "/static/lib/coq-core" (* deprecated upstream *)
+      ; coqcorelib = "/static/lib/rocq-runtime" (* deprecated upstream *)
       ; findlib_config
       ; ocamlpath
       ; vo_load_path

controller-js/dune

@@ -61,12 +61,12 @@
    "export COQW=$(coqc -where) && js_of_ocaml build-fs -o coq-fs.js $(cd $COQW && find theories user-contrib \\( -wholename 'theories/*.vo' -or -wholename 'theories/*.glob' -or -wholename 'theories/*.v' -or -wholename 'user-contrib/*.vo' -or -wholename 'user-contrib/*.v' -or -wholename 'user-contrib/*.glob' \\) -printf \"$COQW/%p:/static/coqlib/%p \")")))
 
 ; for coq-fs-core.js
-; js_of_ocaml build-fs -o coq-fs-core.js $(find coq-core/ -wholename '*/plugins/*/*.cma' -or -wholename '*/META' -printf "%p:/lib/%p")
+; js_of_ocaml build-fs -o coq-fs-core.js $(find rocq-runtime/ -wholename '*/plugins/*/*.cma' -or -wholename '*/META' -printf "%p:/lib/%p")
 
 ; (rule
 ;  (targets coq-fs-core.js)
 ;  (deps
-;   (package coq-core))
+;   (package rocq-runtime))
 ;  (action
 ;   (bash
 ;    "cd ../vendor/coq && js_of_ocaml build-fs -o ../../controller-js/coq-fs.js $(find theories -wholename 'theories/Init/*.vo' -printf '%p:/static/%p '")))

coq/args.ml

@@ -21,8 +21,8 @@ let coqcorelib =
   let doc = "Path to Coq plugin directories." in
   Arg.(
     value
-    & opt string (Filename.concat Coq_config.coqlib "../coq-core/")
-    & info [ "coqcorelib" ] ~docv:"COQCORELIB" ~doc)
+    & opt string (Filename.concat Coq_config.coqlib "../rocq-runtime/")
+    & info [ "rocqcorelib" ] ~docv:"COQCORELIB" ~doc)
 
 let findlib_config =
   let doc = "Override findlib's config file" in

coq/dune

@@ -10,7 +10,7 @@
    (memprof-limits -> limits_mp_impl.real.ml)
    (!memprof-limits -> limits_mp_impl.fake.ml))
   lang
-  coq-core.vernac
+  rocq-runtime.vernac
   coq-lsp.serlib
   ; EJGA: This is due to Coq.Args, feel free to move to its own lib if
   ; needed

coq/loader.ml

@@ -39,24 +39,24 @@ let check_package_exists fl_pkg =
 let map_serlib fl_pkg =
   let supported = match fl_pkg with
     (* Supported by serlib *)             (* directory   *)
-    | "coq-core.plugins.btauto"           (* btauto *)
-    | "coq-core.plugins.cc_core"          (* cc_core  *)
-    | "coq-core.plugins.cc"               (* cc  *)
-    | "coq-core.plugins.extraction"       (* extraction  *)
-    | "coq-core.plugins.firstorder_core"  (* firstorder_core  *)
-    | "coq-core.plugins.firstorder"       (* firstorder  *)
-    | "coq-core.plugins.funind"           (* funind      *)
-    | "coq-core.plugins.ltac"             (* ltac        *)
-    | "coq-core.plugins.ltac2"            (* ltac2       *)
-    | "coq-core.plugins.ltac2_ltac1"      (* ltac2_ltac1 *)
-    | "coq-core.plugins.micromega"        (* micromega   *)
-    | "coq-core.plugins.micromega_core"   (* micromega_core *)
-    | "coq-core.plugins.ring"             (* ring        *)
-    | "coq-core.plugins.ssreflect"        (* ssreflect   *)
-    | "coq-core.plugins.ssrmatching"      (* ssrmatching *)
-    | "coq-core.plugins.number_string_notation" (* syntax *)
-    | "coq-core.plugins.tauto"            (* tauto *)
-    | "coq-core.plugins.zify"             (* zify *)
+    | "rocq-runtime.plugins.btauto"           (* btauto *)
+    | "rocq-runtime.plugins.cc_core"          (* cc_core  *)
+    | "rocq-runtime.plugins.cc"               (* cc  *)
+    | "rocq-runtime.plugins.extraction"       (* extraction  *)
+    | "rocq-runtime.plugins.firstorder_core"  (* firstorder_core  *)
+    | "rocq-runtime.plugins.firstorder"       (* firstorder  *)
+    | "rocq-runtime.plugins.funind"           (* funind      *)
+    | "rocq-runtime.plugins.ltac"             (* ltac        *)
+    | "rocq-runtime.plugins.ltac2"            (* ltac2       *)
+    | "rocq-runtime.plugins.ltac2_ltac1"      (* ltac2_ltac1 *)
+    | "rocq-runtime.plugins.micromega"        (* micromega   *)
+    | "rocq-runtime.plugins.micromega_core"   (* micromega_core *)
+    | "rocq-runtime.plugins.ring"             (* ring        *)
+    | "rocq-runtime.plugins.ssreflect"        (* ssreflect   *)
+    | "rocq-runtime.plugins.ssrmatching"      (* ssrmatching *)
+    | "rocq-runtime.plugins.number_string_notation" (* syntax *)
+    | "rocq-runtime.plugins.tauto"            (* tauto *)
+    | "rocq-runtime.plugins.zify"             (* zify *)
       -> true
     | _ ->
       not_available_warn fl_pkg ": serlib support is missing";

etc/0001-coq-lsp-patch.patch

@@ -34,15 +34,15 @@ index e7b1418c9b..f23338c03c 100644
 --- a/lib/dune
 +++ b/lib/dune
 @@ -4,6 +4,10 @@
-  (public_name coq-core.lib)
+  (public_name rocq-runtime.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
+   rocq-runtime.boot rocq-runtime.clib rocq-runtime.config
    (select instr.ml from
 diff --git a/lib/jscoq_extern.c b/lib/jscoq_extern.c
 new file mode 100644

lang/dune

@@ -2,7 +2,7 @@
  (name lang)
  (public_name coq-lsp.lang)
  (modules :standard \ utf_tests)
- (libraries uri coq-core.library))
+ (libraries uri rocq-runtime.library))
 
 ; We had to do this due to ppx_inline_test enabling backtraces
 

petanque/json_shell/shell.ml

@@ -6,7 +6,7 @@ let init_coq ~debug =
 
 let cmdline : Coq.Workspace.CmdLine.t =
   { coqlib = Coq_config.coqlib
-  ; coqcorelib = Filename.concat Coq_config.coqlib "../coq-core"
+  ; coqcorelib = Filename.concat Coq_config.coqlib "../rocq-runtime"
   ; findlib_config = None
   ; ocamlpath = []
   ; vo_load_path = []

serlib/dune

@@ -9,4 +9,4 @@
    ppx_hash
    ppx_compare
    ppx_deriving_yojson))
- (libraries coq-core.vernac sexplib))
+ (libraries rocq-runtime.vernac sexplib))

serlib/plugins/btauto/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.btauto serlib sexplib))
+ (libraries rocq-runtime.plugins.btauto serlib sexplib))

serlib/plugins/cc/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.cc serlib sexplib))
+ (libraries rocq-runtime.plugins.cc serlib sexplib))

serlib/plugins/cc_core/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.cc_core serlib sexplib))
+ (libraries rocq-runtime.plugins.cc_core serlib sexplib))

serlib/plugins/extraction/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.extraction serlib))
+ (libraries rocq-runtime.plugins.extraction serlib))

serlib/plugins/firstorder/dune

@@ -4,4 +4,4 @@
  (synopsis "Serialization Library for Coq Firstorder Plugin")
  (preprocess
   (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare))
- (libraries coq-core.plugins.firstorder serlib sexplib))
+ (libraries rocq-runtime.plugins.firstorder serlib sexplib))

serlib/plugins/firstorder_core/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.firstorder_core serlib sexplib))
+ (libraries rocq-runtime.plugins.firstorder_core serlib sexplib))

serlib/plugins/funind/dune

@@ -4,4 +4,4 @@
  (synopsis "Serialization Library for Coq Fundind Plugin")
  (preprocess
   (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare))
- (libraries coq-core.plugins.funind serlib serlib_ltac sexplib))
+ (libraries rocq-runtime.plugins.funind serlib serlib_ltac sexplib))

serlib/plugins/ltac/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.ltac serlib sexplib))
+ (libraries rocq-runtime.plugins.ltac serlib sexplib))

serlib/plugins/ltac2/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.ltac2 serlib sexplib))
+ (libraries rocq-runtime.plugins.ltac2 serlib sexplib))

serlib/plugins/ltac2_ltac1/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.ltac2_ltac1 serlib sexplib serlib_ltac2))
+ (libraries rocq-runtime.plugins.ltac2_ltac1 serlib sexplib serlib_ltac2))

serlib/plugins/micromega/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.micromega serlib sexplib))
+ (libraries rocq-runtime.plugins.micromega serlib sexplib))

serlib/plugins/micromega_core/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.micromega_core serlib sexplib))
+ (libraries rocq-runtime.plugins.micromega_core serlib sexplib))

serlib/plugins/nsatz_core/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.nsatz_core serlib sexplib))
+ (libraries rocq-runtime.plugins.nsatz_core serlib sexplib))

serlib/plugins/ring/dune

@@ -4,4 +4,4 @@
  (synopsis "Serialization Library for Coq Setoid Newring Plugin")
  (preprocess
   (staged_pps ppx_import ppx_sexp_conv ppx_hash ppx_compare))
- (libraries coq-core.plugins.ring serlib serlib_ltac sexplib))
+ (libraries rocq-runtime.plugins.ring serlib serlib_ltac sexplib))

serlib/plugins/ssr/dune

@@ -10,7 +10,7 @@
    ppx_hash
    ppx_compare))
  (libraries
-  coq-core.plugins.ssreflect
+  rocq-runtime.plugins.ssreflect
   serlib
   serlib_ltac
   serlib_ssrmatching

serlib/plugins/ssrmatching/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.ssrmatching serlib serlib_ltac sexplib))
+ (libraries rocq-runtime.plugins.ssrmatching serlib serlib_ltac sexplib))

serlib/plugins/syntax/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.number_string_notation serlib sexplib))
+ (libraries rocq-runtime.plugins.number_string_notation serlib sexplib))

serlib/plugins/tauto/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.tauto serlib sexplib))
+ (libraries rocq-runtime.plugins.tauto serlib sexplib))

serlib/plugins/zify/dune

@@ -9,4 +9,4 @@
    ppx_deriving_yojson
    ppx_hash
    ppx_compare))
- (libraries coq-core.plugins.zify serlib sexplib))
+ (libraries rocq-runtime.plugins.zify serlib sexplib))