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.