Fix Corelib detection on dune exec -- rocq with dune 3.24

[rlepigre-skylabs-ai]

See #Dune devs & users > dune exec changed?.

CC @SkySkimmer

[rlepigre-skylabs-ai]

@coqbot run full ci

[SkySkimmer]

Isn't this a dune bug? I'm not sure we want workaround code for it.

If we do want code for it maybe we could rely on INSIDE_DUNE instead of unconditionally crawling the filesystem?

[rlepigre-skylabs-ai]

Isn't this a dune bug? I'm not sure we want workaround code for it.

I'm not sure this qualifies as a dune bug, as we're kind of abusing implementation details. The change proposed in ocaml/dune#14432 seems pretty reasonable to me, but maybe @Alizter can comment.

For context, we relied on dune exec -- rocq to resolve to _build/install/default/bin/rocq to locate Corelib and so on relative to the binary. Now, this is broken and one needs to run _build/install/default/bin/rocq directly for things to work as expected.

If we do want code for it maybe we could rely on INSIDE_DUNE instead of unconditionally crawling the filesystem?

Something like that might mess with composed builds, and would also prevent running _build/default/topbin/rocq.exe directly (not sure that last one is an issue though).

[SkySkimmer]

https://dune.readthedocs.io/en/latest/reference/cli.html#describe-dune-exec

Execute a command in a similar environment as if installation was performed.

How is running from the build layout "as if installation was performed"?
How can we justify dune exec -- rocq and dune exec -- env rocq giving different results?

Something like that might mess with composed builds, and would also prevent running _build/default/topbin/rocq.exe directly (not sure that last one is an issue though).

It's explicitly not supported when configured relocatable. relocatable rocq expects the install layout, not the build layout.

[SkySkimmer]

Checking if basename (dirname argv[0]) is "topbin" could also work to detect the build layout

[rlepigre-skylabs-ai]

Checking if basename (dirname argv[0]) is "topbin" could also work to detect the build layout

That would definitely work too.

[SkySkimmer]

BTW coq_config_to_make call (in test-suite/dune) is probably broken by this dune change too (I didn't check though).