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

There are many more occurrences of `coq-core` in this repo but I don't know what they're doing. This patch is just enough to fix Coq's CI.
ejgallego · Dec 11, 2024 · c66de24 · c66de24
1 parent c110000
commit c66de24
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 19 deletions.
diff --git 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/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 = []