feature(coq): coq macro

[Alizter]

This is a continuation of #5967. The difference here is that the extra variables have been removed in a following commit. We now only expose:

Coq configuration variables:

%{coq:coqlib}
%{coq:coq_native_compiler_default}

Version numbers for Coq:

%{coq:version}
%{coq:ocaml-version}
%{coq:version.major}
%{coq:version.minor}
%{coq:version.suffix}

• close https://github.com/ocaml/dune/pull/5967
• close https://github.com/ocaml/dune/pull/5913

[Alizter]

@ejgallego ping

[ejgallego]

Looks very good to me, thanks! I can do a full code review next week after I'm done with the Sabanci class, but if someone else wants to take over, the interface for this PR looks good to me so you can merge.

Need to update the docs and changelog I think.

[ejgallego]

Also %{coq:coq_native_compiler_default} could be maybe named a bit differently? The flag really means that coqc was configured to output native files by default. But still you can use the native compiler when this flag in configure was not passed.

It is a hack so people could have coq_makefile output native files just by recompiling coq.

[Alizter]

Also %{coq:coq_native_compiler_default} could be maybe named a bit differently? The flag really means that coqc was configured to output native files by default. But still you can use the native compiler when this flag in configure was not passed.

It is a hack so people could have coq_makefile output native files just by recompiling coq.

We can name it whatever we want, I just kept the env var name from configure.

[Alizter]

@ejgallego ping

[Alizter]

@ejgallego I've added a changelog and some doc.

[Alizter]

The expander code is originally @rgrinberg's, but if he has some time, I wouldn't mind another pair of eyes.