Compilation broken if Coq compiled without native compiler

[gares]

Apparently coqc is broken if Coq does not support native compilation but you pass the flag as per #38 . On windows we disable the native compiler (it is the default).

Relevant logs:
https://coq.gitlab.io/-/coq/-/jobs/501853273/artifacts/artifacts/buildlogs/bignums-a33927c06eb0701025f873f7e5951f7b07a89e6e-make_log.txt
https://coq.gitlab.io/-/coq/-/jobs/501853273/artifacts/artifacts/buildlogs/bignums-a33927c06eb0701025f873f7e5951f7b07a89e6e-make_err.txt

I report the bug here, but it is unclear to me, since clients have (AFAICT) no way to ask Coq if native compilation is supported.

CC @maximedenes

[proux01]

I report the bug here, but it is unclear to me, since clients have (AFAICT) no way to ask Coq if native compilation is supported.

Indeed, I resorted to a test in #41

[ejgallego]

This seems like a bug in Coq, right? bignums is just following the documented procedure to enable native IIANM right?

[proux01]

I agree having a fix in Coq would be much better. What could be a reasonable solution? Extending -native-compiler (yes|no|ondemand) to yes|no|ondemand|ifavailable with the latter acting just as yes when native-compile is available and as no otherwise? @maximedenes any opinion?

[gares]

I'd prefer to have coqc ignore the flag if the feature is not available.

[proux01]

Why not, but then this should at least emit a warning. I don't want the flag to be silently ignored.

If we all agree on this, I'll open a PR.

[Zimmi48]

I agree. And this would be consistent with the behavior of native_compute falling back to vm_compute when the former is called from Coq files but is not available.

[gares]

I agree