[Coq] (stdlib no) broken since 3.8.0

[LasseBlaauwbroek]

Starting with Dune 3.8.0, due to #6563, dune can no longer build in (stdlib no) mode when the stdlib is not installed. This is because it is checking coqc --config, which gives an exit code of 1. It has always done that, but Dune didn't seem to check it before 3.8.0

Reproduction

We can reproduce the problem with Dune's own tests.

1. Make sure that you have coq-core.8.18.0 installed, but not coq-stdlib!
2. DUNE_COQ_TEST=enable ./dune.exe build @no-stdlib outputs:

File "test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t", line 1, characters 0-0:
------ test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t
++++++ test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t.corrected
File "test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t", line 7, characters 0-1:
 |Test that when `(stdlib no)` is provided, the standard library is not bound to `Coq`
 |and the prelude is not imported
 |
 |  $ dune build --display=short foo.vo
 |  Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
 |  3.8 and will be removed in an upcoming Dune version.
-|        coqdep .basic.theory.d
-|          coqc foo.{glob,vo}
+|  cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.
+|  cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.
+|  [1]
 |
 |  $ dune build --display=short bar.vo
 |  Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
 |  3.8 and will be removed in an upcoming Dune version.
-|          coqc bar.{glob,vo} (exit 1)
-|  File "./bar.v", line 1, characters 20-23:
-|  Error: The reference nat was not found in the current environment.
-|  
+|  cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.
+|  cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.

3. When you do git checkout 3.7.1 and run the tests again, you will see that they succeed.

CC @ejgallego @Alizter

[Alizter]

The fact that coqc --config fails when no stdlib is present is a bug and should be reported upstream. We can work around it in Dune but we will no longer be able to use native compilation rules in this case. It's also difficult to test as we would have to have another CI job that has just coq-core which seems a bit wasteful of our CI resources.

[LasseBlaauwbroek]

An issue for this already exists: coq/coq#16295

[Alizter]

I'm going to recreate the issue you ran into and see if I can make a reproduction case without the special setup. What's weird is that rereading the code, it seems there should be a fail-safe for when config fails, so I'm not sure what exactly is failing here just yet.

[Alizter]

I've chased down the issue some more and it now appears that coqc --config is not the culprit. It's actually because we are querying coqc --version but that too fails! I'll make this more resilient. This is yet another bug in Coq that should probably be reported upstream. It's a shame that something as simple as a version number has to initialize the Coq enviornment and trigger unrelated errors.

[LasseBlaauwbroek]

Ah, good find!

I should note that coqc --version -boot does work without stdlib. So that should be an easy fix :-)

[ejgallego]

Good find @Alizter ! Indeed we need to be a bit more defensive on this side, and fix Coq upstream of course!

[ejgallego]

Thanks @LasseBlaauwbroek for the report by the way; we have a couple more open issues pending for composed / (no stdlib) builds; that means that indeed we are blocked on our own projects to dune 3.7

I hope to be able to have some time for this soon.

[Alizter]

I have tests and fixes ready for this, just need some time to clean them up.