What is the exact status of the
COQMF_* variables in CoqMakefile?
Are they the preferred way to interact with the coq options?
what do you mean exactly?
Or are they for internal use?
More specifically, the default native-compiler configure PR introduced a new variable COQMF_COQ_NATIVE_COMPILER_DEFAULT
Yes, if you are
No, if you are
make -f Makefile.coq VARIABLE=value
does it makes sense to let the user override it at the command line?
I was wondering whether we shouldn't base the decision of native compilation from the COQ_NATIVE_COMPILER_DEFAULT, rather than the currently recommended COQEXTRAFLAGS
if so, provide also a nicer name
You mean, without the COQMF?
Maybe it's a XY problem, so here is the story
I have https://github.com/coq/coq/pull/13287 which is fairly functional right now.
but the problem is that CoqMakefile is unaware of native compilation.
At least, in the recommended setup, which is setting COQEXTRAFLAGS+="native-compiler yes"
in the above PR, CoqMakefile decides to native compile instead depending on the configure flag, which is available to it as the COQMF_NATIVE_blablah
it works, but if people relied on the COQEXTRAFLAGS environment variable to unset native compilation while the configure option is set to yes, it will native compile it altogether
so, since we have introduced recently this more precise environment variable, I believe we should advertise it instead of the generic COQEXTRAFLAGS
(in particular, the CI unsets native compilation on some dev via COQEXTRAFLAGS)
I don't get why COQMF_NATIVE_blablah wins over COQEXTRAFLAGS+="-native off".
coqc -native-compiler ondemand -native-compiler off is what you get no?
Yes, for coqc, so coqc does not compile the file.
But there is now a new program coqnative.
This program extracts a cmxs out of a vo, and it called from CoqMakefile when the COQMF_NATIVE variable is set to yes.
This program does not take as an imput all the Coq flags since most of them are irrelevant.
Should it receive COQEXTRAFLAGS as arguments anyway?
Morally coqnative is a variant of coqchk.
Nope, it takes only the library path, which already have their dedicated variable in coqmakefile
So, essentially my question boils down to the following: since the merge of the native configure flag, we now have two ways to trigger a native compilation.
namely, COQMF_NATIVE... and COQEXTRAFLAGS
one is easier to manipulate than the other.
Shouldn't we rely on that one instead?
cc @Erik Martin-Dorel
what happens if it is called on a .vo generated without native on?
if the dependencies are not compiled, it will error.
coqc does the same btw
The above PR is just optionally moving the responsibility of native compilation to a program different from coqc
so, it'll only affect coqmakefile users.
you move the responsability but you don't pass the same flags... aren't you looking for troubles?
in other words, nearly every third-party Coq project maintainer will now have to make decisions about native compilation...
can't you always call it but make it do nothing?
@Karl Palmskog nope
it doesn't change anything, except for people actively deactivating native compilation
it's still following the configure CEP guidelines
(i.e. the only behaviour change is if you set configure native-yes and COQEXTRAPARAMS="native no")
so, in any case, it seems to me more natural to rely on a specific flag rather than a generic one, which was precisely introduced for that matter
@ppedrot : note that currently,
NATIVE_COMPILER_DEFAULT doesn't set/unset or trigger anything, it just tells yu what the default behavior is
Yes, but CoqMakefile could use this info still.
The constraint for the introduction of split-native is to be transparent for exotic (i.e. non-coqmakefile build systems)
But it doesn't prevent us to document a preferred flag for native compilation compared to COQEXTRAFLAGS
If you're unlucky enough to be a development that needs to do something specific for native compilation (either explicitly activating / deactivating it) it won't change your already hard life
Last updated: May 28 2023 at 13:30 UTC