Emilio Jesús Gallego Arias

@coqbot run full CI

@Alizter the status of this PR is a bit complex as indeed here we are in a build situation that is sadly very non-deterministic due to path relativization. To sum...

@SkySkimmer see windows CI @ppedrot I know how to make progress so I'm unsure what you mean by nobody? The code we have to interact with findlib is pretty messy,...

Moreover my previous answer for Ali sums the situation up pretty well.

> > I know how to make progress so I'm unsure what you mean by nobody? > > Your summary seems to indicate there is a mysterious dune bug involved....

By the way, in terms of build systems roadmap, this PR is of priority wishlist. I am unsure why you have decided suddenly that this PR is critical, but it...

> What is path relativization? Where is it implemented? What is wrong with it? It is a procedure in coqdep that turns the absolute path returned by findlib into a...

> > By the way, in terms of build systems roadmap, this PR is of priority wishlist. > > It's important because whenever we deal with plugins like in #19313...

> There's a bunch of random hacks to remember, as you can see the PR still doesn't work I see the PR is merged, but indeed I still don't understand...

> The pushed commit (I also rebased) seems to work Good, indeed only real blocker was the path normalization stuff. We need to try if things still work with regular...