I don't understand. What is the use case?

As a use case, assume alice has a local copy of the coq repository. She does something like this:

$ echo $COQBIN
/home/alice/coq/_build/install/default/bin
$ autoconf

and then autoconf finds coqc and coq_makefile in /home/alice/coq/_build/install/default/bin instead of the one (if any) in the PATH directories.

This is useful for instance when the user has a development version of coq and wants to test coq_dpdgraph against it.
It is done in Coquelicot.

It is not vital since the user can still prepend its PATH with its COQBIN before running autoconf, but it would make the building steps more uniform with the other libraries.

Understood. I don't really understand autoconf myself, and there is pressure to remove its use. One proposed solution is to have a build process relying on dune. Another solution that I had in mind was to only rely on opam to perform checks about dependencies. Your use case makes me realize (and remember) that some users are unhappy with opam which forces to re-compile everything for each switch.

My next question is relative to your use case (since I am not an expert on autoconf, I may not be able to implement your need, but I still need to know more if I try). Do you wish COQBIN to be used in priority (even if coqc can be found in the PATH) or do you wish COQBIN to be used as as fallback solution when nothing is found in the PATH

Thank you. I think that COQBIN, if set and non empty usually has priority over the PATH. Then if the user prefers to build it against a released version in her PATH, she can just unset COQBIN or make it empty.

I am now stopping to work on this issue, for lack of time today. I think a solution might be found by playing with the extra optional arguments to command AC_CHECK_PROG (look for the documentation of autoconf here, for instance) it might be possible to just set the path to :$COQBIN:$PATH in the two calls to AC_CHECK_PROG at lines 177 and 192 of configure.ac of today.