diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 25d9b6ddd..148036ca2 100644 --- a/.github/workflows/build.yml +++ b/.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 . diff --git a/.gitmodules b/.gitmodules index fd7494c3b..22af1b516 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,3 @@ [submodule "coq"] path = vendor/coq - url = https://github.com/coq/coq.git + url = https://github.com/skyskimmer/coq.git diff --git a/CHANGES.md b/CHANGES.md index a62938e9c..c7047cb9c 100644 --- a/CHANGES.md +++ b/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 --------------------------------------------- diff --git a/Makefile b/Makefile index ff23f773b..18356cfb1 100644 --- a/Makefile +++ b/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 ") \ diff --git a/controller-js/coq_lsp_worker.ml b/controller-js/coq_lsp_worker.ml index 5ee4ef58b..b0fbf0289 100644 --- a/controller-js/coq_lsp_worker.ml +++ b/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 diff --git a/controller-js/dune b/controller-js/dune index 4805bb4d9..79071d9ab 100644 --- a/controller-js/dune +++ b/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 '"))) diff --git a/coq/args.ml b/coq/args.ml index e3fcadfd8..e7ff53688 100644 --- a/coq/args.ml +++ b/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 diff --git a/coq/dune b/coq/dune index a6a55756f..8385ea6d3 100644 --- a/coq/dune +++ b/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 diff --git a/coq/loader.ml b/coq/loader.ml index 854bc2b1a..d6f273e0d 100644 --- a/coq/loader.ml +++ b/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"; diff --git a/etc/0001-coq-lsp-patch.patch b/etc/0001-coq-lsp-patch.patch index f42d9cd43..cfae7c601 100644 --- a/etc/0001-coq-lsp-patch.patch +++ b/etc/0001-coq-lsp-patch.patch @@ -34,7 +34,7 @@ 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 @@ -42,7 +42,7 @@ index e7b1418c9b..f23338c03c 100644 + (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 diff --git a/lang/dune b/lang/dune index dfca2321a..b1ad1bc61 100644 --- a/lang/dune +++ b/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 diff --git a/petanque/json_shell/shell.ml b/petanque/json_shell/shell.ml index a9dccdb4d..451c8d03e 100644 --- a/petanque/json_shell/shell.ml +++ b/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 = [] diff --git a/serlib/dune b/serlib/dune index 1b863e4ef..8c54a7034 100644 --- a/serlib/dune +++ b/serlib/dune @@ -9,4 +9,4 @@ ppx_hash ppx_compare ppx_deriving_yojson)) - (libraries coq-core.vernac sexplib)) + (libraries rocq-runtime.vernac sexplib)) diff --git a/serlib/plugins/btauto/dune b/serlib/plugins/btauto/dune index f29b7d502..0740fce03 100644 --- a/serlib/plugins/btauto/dune +++ b/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)) diff --git a/serlib/plugins/cc/dune b/serlib/plugins/cc/dune index 28ca0e2d8..3ee774c65 100644 --- a/serlib/plugins/cc/dune +++ b/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)) diff --git a/serlib/plugins/cc_core/dune b/serlib/plugins/cc_core/dune index 3be9c76ce..09ab4a052 100644 --- a/serlib/plugins/cc_core/dune +++ b/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)) diff --git a/serlib/plugins/extraction/dune b/serlib/plugins/extraction/dune index 2c19356cc..a21b2cc39 100644 --- a/serlib/plugins/extraction/dune +++ b/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)) diff --git a/serlib/plugins/firstorder/dune b/serlib/plugins/firstorder/dune index ee351fc9c..36e46370f 100644 --- a/serlib/plugins/firstorder/dune +++ b/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)) diff --git a/serlib/plugins/firstorder_core/dune b/serlib/plugins/firstorder_core/dune index 3d3833747..91a7aac87 100644 --- a/serlib/plugins/firstorder_core/dune +++ b/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)) diff --git a/serlib/plugins/funind/dune b/serlib/plugins/funind/dune index 591c05710..e5acaba6f 100644 --- a/serlib/plugins/funind/dune +++ b/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)) diff --git a/serlib/plugins/ltac/dune b/serlib/plugins/ltac/dune index b2668504f..741f5c0e7 100644 --- a/serlib/plugins/ltac/dune +++ b/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)) diff --git a/serlib/plugins/ltac2/dune b/serlib/plugins/ltac2/dune index fe468ad67..a887b2547 100644 --- a/serlib/plugins/ltac2/dune +++ b/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)) diff --git a/serlib/plugins/ltac2_ltac1/dune b/serlib/plugins/ltac2_ltac1/dune index 1ff121690..2135edef8 100644 --- a/serlib/plugins/ltac2_ltac1/dune +++ b/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)) diff --git a/serlib/plugins/micromega/dune b/serlib/plugins/micromega/dune index 9f0296e9a..2e8971fe7 100644 --- a/serlib/plugins/micromega/dune +++ b/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)) diff --git a/serlib/plugins/micromega_core/dune b/serlib/plugins/micromega_core/dune index ff4e2658a..2b8d40bf4 100644 --- a/serlib/plugins/micromega_core/dune +++ b/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)) diff --git a/serlib/plugins/nsatz_core/dune b/serlib/plugins/nsatz_core/dune index c84888208..c7fd20a72 100644 --- a/serlib/plugins/nsatz_core/dune +++ b/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)) diff --git a/serlib/plugins/ring/dune b/serlib/plugins/ring/dune index 6b7b8e47c..6bdf2bf92 100644 --- a/serlib/plugins/ring/dune +++ b/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)) diff --git a/serlib/plugins/ssr/dune b/serlib/plugins/ssr/dune index 277917c86..967b62ffe 100644 --- a/serlib/plugins/ssr/dune +++ b/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 diff --git a/serlib/plugins/ssrmatching/dune b/serlib/plugins/ssrmatching/dune index f4192e2dd..9e5a32596 100644 --- a/serlib/plugins/ssrmatching/dune +++ b/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)) diff --git a/serlib/plugins/syntax/dune b/serlib/plugins/syntax/dune index aea4ef0a0..964d2991b 100644 --- a/serlib/plugins/syntax/dune +++ b/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)) diff --git a/serlib/plugins/tauto/dune b/serlib/plugins/tauto/dune index 9170dbc02..012395e1b 100644 --- a/serlib/plugins/tauto/dune +++ b/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)) diff --git a/serlib/plugins/zify/dune b/serlib/plugins/zify/dune index 96332e6aa..6989c49d2 100644 --- a/serlib/plugins/zify/dune +++ b/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)) diff --git a/vendor/coq b/vendor/coq index 476460fb0..d1763f039 160000 --- a/vendor/coq +++ b/vendor/coq @@ -1 +1 @@ -Subproject commit 476460fb01e3f40edf2f4a63470d0cbbd1d89f7a +Subproject commit d1763f039edae16305a282ba7ea161fa5db13b20