configure: coq version check doesn't seem to work

[andrew-appel]

I just fetched the master branch of compcert d357b5c and attempted ./configure. It failed with a complaint about coq version, even though I have a supported coq version. I'm in a 64-bit cygwin system:

$ ./configure x86_64-cygwin -use-external-Flocq -clightgen
Testing assembler support for CFI directives... yes
Testing linker support for '-no-pie' / '-nopie' option... yes, '-no-pie'
 -- UNSUPPORTEDversion 8.15.1
Error: CompCert requires a version of Coq between 8.12.0 and 8.15.1
Testing OCaml... version 4.10.0 -- good!
Testing OCaml native-code compiler...yes
Testing OCaml .opt compilers... yes
Testing Menhir... version 20200211 -- good!
Testing GNU make... version 4.3 (command 'make') -- good!
One or several required tools are missing or too old.  Aborting.

$ coqc --version
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.13.1

The reason is that cygwin's newline is CR-LF rather than just LF. It can be fixed, if you care to, by deleting the CR character in the coq_ver test. Here, I have done it with a tr command, but you might choose to do it a different way:

coq_ver=$(${COQBIN}coqc -v 2>/dev/null | tr -d '\r' | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')

Of course, I can work around this with -ignore-coq-version.

[xavierleroy]

Well spotted. We're lucky we did not run into this issue earlier. The OCaml makefiles and scripts are full of tr -d '\r' for this exact reason. Will fix as suggested.

[xavierleroy]

Tentative fix in 5c8f3c2. Let me know if it still fails on your Cygwin installation.

[andrew-appel]

works fine.