[Coq] (stdlib no) broken since 3.8.0 #8958
Description
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.
- Make sure that you have
coq-core.8.18.0installed, but notcoq-stdlib! DUNE_COQ_TEST=enable ./dune.exe build @no-stdliboutputs:
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.
- When you do
git checkout 3.7.1and run the tests again, you will see that they succeed.