[coq] expand coq.version & co without using coq-lib

[gares]

The file coq_config.ml is able to expand variables by two means:

• coqc --print-version
• coqc -config

The former works fine with just coq-core being built (if one also passes -boot -noinit). The use case is to compose with other projects using the coq.version variable (for example to feed ppx_optcomp) and run dune build @check.

Unfortunately the file coq_config.ml first computes all data and then checks which variable to expand. Hence, both commands are run, and the latter requires a more "complete" build of coq to work.

It would be nice if the by_name dispatching could be used upfront, and only call the command needed in order to fulfill the request.

[Alizter]

IIRC coqc -noinit --version had trouble when the stdlib wasn't available. Can you check that this is the case when only coq-core is installed via opam? We can't really check this in the Dune CI since we run our test-suite with the full coq package.

[ejgallego]

@Alizter did you intend this comment to go in Enrico's PR itself?

[gares]

I think the test suite you have tests it. Indeed I had to fix the expected output by removing a failure and add a version number (for coq 8.16 IIRC).

[Alizter]

@gares IIRC that test-suite still has coq-stdlib around. From what I remember, not having coq-stdlib installed anywhere caused issues with coqc --print-version.

[gares]

I do pass -boot -noinit now, before it did not pass these.

[Alizter]

Right, but back when I tested it doing coqc --print-version -boot -noinit with no coq-stdlib installed caused an error. I am wondering if this is still the case.

[ejgallego]

@Alizter , it is easy to check this in master:

$ git clean -fxd
$ dune build -p coq-core
$ ls _build/install/default/lib/
$ dune exec -- coqc -print-version -boot -noinit

8.20+alpha 4.14.2

For our base CI base (8.16): 8.16.1 4.14.2

So indeed, at least here, it works!

[Alizter]

@ejgallego Do you have an opam switch with Coq around?

[ejgallego]

I do have quite a few.

[Alizter]

@ejgallego Could you try testing this in an isolated environment. The coqlib detection code in coqc does some weird directory checks and if those fails leads to an error in this case I believe. If this is still OK, then I support this PR. But I am under the impression that Coq is lacking the functionality that it supposedly can support.

[ejgallego]

Actually the code is not so weird, it is pretty simple, and we refactored it a lot in the last releases (since 8.8 I guess) so it is not in such a bad shape, tho it could use still quite a few improvements.

The code just tries to first locate coqlib, then it checks prelude is there, as otherwise the auto require import prelude will fail.

Check under dune shouldn't be too different from opam, anyways, checked opam for 8.19 and it works fine.

Note that if Nix uses env vars, this is less tested actually.

$ opam list | grep coq
$ dune exec -- coqc -print-version -boot -noinit

Output 8.19.1 4.14.1

As Enrico pointed out, -boot should avoid triggering this problem.

Actually I just realized before pressing send, that you may be thinking of problems with coqdep or coqchk, that could be the case, but I think we are good in the latest releases too.