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

[SkySkimmer]

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.

[SkySkimmer]

Doesn't quite work, I get

-   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 0 Coq plugin directory bindings in scope

eg https://gitlab.inria.fr/coq/coq/-/jobs/5062976

[ejgallego]

I'll have a look tomorrow and try to fix it.

[ejgallego]

@SkySkimmer you missed the occurence in coq/args.ml which the important one.

Anyways this code can be removed as we don't use the findlib method anymore, I actually have a coq-lsp branch that does that but it will take a while for me to return back to work unfortunately.

[ejgallego]

@SkySkimmer you mind bumping the vendor/coq submodule to I can use coq-lsp CI to check things are right?

(And adapt to other changes like the worker build, etc...)

Also serlib needs (an easy) fix for its dune files, that basically covers it all.

Note that I plan to make the loader not so hacky, also got a branch for that somewhere.

[SkySkimmer]

@SkySkimmer you mind bumping the vendor/coq submodule to I can use coq-lsp CI to check things are right?

IDK how to do that

[ejgallego]

IDK how to do that

pushd vendor/coq
git checkout $the_branch_you_want
popd
git add vendor/coq && git commit ...

[SkySkimmer]

But the vendored git repo only knows about coq/coq, my branch is in skyskimmer/coq

[ejgallego]

Good questions, I'm not sure I make it work, as I use hub and gh command line tools. Maybe git submodule set-url is the new recommended way?

Never mind if that's too hard.

[SkySkimmer]

I edited .gitmodules to point at my fork

[ejgallego]

Updated rest of the system, including the missing change to coq/args that made Coq CI fail.

Let's see how it goes.

[ejgallego]

• 2 Coq path directory bindings in scope; 0 Coq plugin directory bindings in scope

As I've mentioned, this will change to "X findlib paths in scope" for Rocq 9.0

[ejgallego]

CI green, local and JS tests OK too.