Failure of [coqc --config] with Coq in a workspace

[rlepigre]

Variable expansion based on the output of coqc --config, such as %{coq:version.major}, is broken when Coq itself is in the workspace. This leads to errors like the following:

Error: Could not expand %{coq:version.minor} as running coqc --config failed

The reason making coqc fail is that it does not know where to find the standard library.

This can be reproduced using the following:

mkdir workspace_bug
cd workspace_bug

echo "(lang dune 3.8)" > dune-workspace

git clone git@github.com:coq/coq.git

mkdir test
echo "(rule (action (with-outputs-to coq-version.txt (echo \"%{coq:version.major}\"))))" > test/dune

dune build test

CC @ejgallego @Alizter

[rlepigre]

Note that I'd expect at least the expansion of variable that do not depend on the standard library (like version stuff) to always work, regardless of whether the standard library is available in the workspace or not.

[Alizter]

@rlepigre It is a quirk of Coq, at least at the time, that the standard library location was required to output the version.

Not sure what the best fix is here.

We might be able to trick Coq into giving up it's version by passing a dummy stdlib location.

[rlepigre]

Yeah, that's what I was thinking. Another option would be to rely on coqc -boot -noinit --version instead.

[Alizter]

@rlepigre IIRC -boot -noinit had not effect on this, but this may have changed.

[rlepigre]

On the version I tested (basically 8.19) it has an effect for --version. It does not have an effect for --config though.

[ejgallego]

Thanks again for the report @rlepigre , I am wondering on your test case tho, don't you define a (lang coq ...) version?

I was under the impression we had fixed this, but indeed, let's look into what is going on.

[rlepigre]

I'm not sure what you mean with (lang coq ...) @ejgallego, I do have the following in coqlib/dune-project:

(lang dune 3.8)
(using coq 0.8)
(name coqlib)

[ejgallego]

I meant on the example above, you do: echo "(lang dune 3.8)" > dune-workspace , so I wonder what dune lang version the example in test picks.

Indeed, I don't think the test should be even accepted, coq: variables should be disabled if you don't declare a dune-project with the right setup.

[ejgallego]

Indeed @rlepigre I think #10631 should have fixed this.

But that won't happen until Dune 3.17 I'm afraid, but maybe you can backport the patch?

[rlepigre]

Ah, I see, thanks! I somehow missed that issue and MR.

[ejgallego]

Easy to miss, as the changelog for main now is on several files under doc/changes.

I wouldn't be surprised if we have more problems in this area, please don't hesitate to reopen.