[config] Re-enable use of configure option -bytecode-compiler

[ejgallego]

Since #16931 , ./configure -bytecode-compiler no had no effect, as we stopped checking the flag.

We do instead like native and set default options flag. I wonder if these options defaults should better read from the kernel tho.

[silene]

Note that this is not the same behavior as with -native-compiler. If one does

./configure -native-compiler no
...
coqc -native-compiler yes

then native compilation is still disabled (and a warning is displayed).

With your pull request, if one does

./configure -bytecode-compiler no
...
coqc -bytecode-compiler yes

then bytecode compilation is now enabled. Should both flags behave the same?

[ejgallego]

then bytecode compilation is now enabled. Should both flags behave the same?

As you prefer folks, I guess in the native case it makes more sense to respect the configure flag as the VM may not be available, but I don't really have a preference.

My use case is similar, the VM is not available in any of the JavaScripts / WebAssembly builds.

I noticed this bug as indeed our build was passing -bytecode-compiler no to Coq, however we got the VM trap triggered.

Now jsCoq / coq-lsp builds do set the enable_VM setup correctly at init, so configure doesn't matter so much.

[erikmd]

Should both flags behave the same?

I believe so.

FWIW, the behavior of the -native-compiler flag is well-documented in the CEP 48 (which is still up-to-date in this regard).

[SkySkimmer]

Should both flags behave the same?

IMO yes

[ppedrot]

What do we do with this? 9.0 branch is coming around.

[ppedrot]

Last call, this needs to be assigned and merged before Monday AoE to make it into 9.0.

[ppedrot]

Thus postponing.

[SkySkimmer]

@ejgallego what help are you looking for?

[ejgallego]

@SkySkimmer code needs update to match the semantics used in native, per-discussion, it seems we need to add a warning for the case config = no; cmdline = yes