Pierre-Marie Pédrot (Nov 24 2020 at 11:35): Pierre-Marie Pédrot (Nov 24 2020 at 11:35):What is the exact status of the COQMF_* variables in CoqMakefile?
Pierre-Marie Pédrot (Nov 24 2020 at 11:36):Are they the preferred way to interact with the coq options?
Enrico Tassi (Nov 24 2020 at 11:36):what do you mean exactly?
Pierre-Marie Pédrot (Nov 24 2020 at 11:36):Or are they for internal use?
Pierre-Marie Pédrot (Nov 24 2020 at 11:36):More specifically, the default native-compiler configure PR introduced a new variable COQMF_COQ_NATIVE_COMPILER_DEFAULT
Enrico Tassi (Nov 24 2020 at 11:36):Yes, if you are include Makefile.coq.conf
No, if you are make -f Makefile.coq VARIABLE=value
Enrico Tassi (Nov 24 2020 at 11:37):does it makes sense to let the user override it at the command line?
Pierre-Marie Pédrot (Nov 24 2020 at 11:37):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
Enrico Tassi (Nov 24 2020 at 11:37):if so, provide also a nicer name
Pierre-Marie Pédrot (Nov 24 2020 at 11:38):You mean, without the COQMF?
Pierre-Marie Pédrot (Nov 24 2020 at 11:39):Maybe it's a XY problem, so here is the story
Pierre-Marie Pédrot (Nov 24 2020 at 11:39):I have https://github.com/coq/coq/pull/13287 which is fairly functional right now.
Pierre-Marie Pédrot (Nov 24 2020 at 11:39):but the problem is that CoqMakefile is unaware of native compilation.
Pierre-Marie Pédrot (Nov 24 2020 at 11:40):At least, in the recommended setup, which is setting COQEXTRAFLAGS+="native-compiler yes"
Pierre-Marie Pédrot (Nov 24 2020 at 11:41):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
Pierre-Marie Pédrot (Nov 24 2020 at 11:42):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
Pierre-Marie Pédrot (Nov 24 2020 at 11:42):so, since we have introduced recently this more precise environment variable, I believe we should advertise it instead of the generic COQEXTRAFLAGS
Pierre-Marie Pédrot (Nov 24 2020 at 11:43):(in particular, the CI unsets native compilation on some dev via COQEXTRAFLAGS)
Pierre-Marie Pédrot (Nov 24 2020 at 11:43):"What do?"
Enrico Tassi (Nov 24 2020 at 12:00):I don't get why COQMF_NATIVE_blablah wins over COQEXTRAFLAGS+="-native off".
Enrico Tassi (Nov 24 2020 at 12:01):said otherwise coqc -native-compiler ondemand -native-compiler off is what you get no?
Pierre-Marie Pédrot (Nov 24 2020 at 12:03):Yes, for coqc, so coqc does not compile the file.
Pierre-Marie Pédrot (Nov 24 2020 at 12:03):But there is now a new program coqnative.
Pierre-Marie Pédrot (Nov 24 2020 at 12:04):This program extracts a cmxs out of a vo, and it called from CoqMakefile when the COQMF_NATIVE variable is set to yes.
Pierre-Marie Pédrot (Nov 24 2020 at 12:05):This program does not take as an imput all the Coq flags since most of them are irrelevant.
Paolo Giarrusso (Nov 24 2020 at 12:05):Should it receive COQEXTRAFLAGS as arguments anyway?
Pierre-Marie Pédrot (Nov 24 2020 at 12:05):Morally coqnative is a variant of coqchk.
Paolo Giarrusso (Nov 24 2020 at 12:05):Hm
Pierre-Marie Pédrot (Nov 24 2020 at 12:05):Nope, it takes only the library path, which already have their dedicated variable in coqmakefile
Pierre-Marie Pédrot (Nov 24 2020 at 12:06):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.
Pierre-Marie Pédrot (Nov 24 2020 at 12:06):namely, COQMF_NATIVE... and COQEXTRAFLAGS
Pierre-Marie Pédrot (Nov 24 2020 at 12:06):one is easier to manipulate than the other.
Pierre-Marie Pédrot (Nov 24 2020 at 12:07):Shouldn't we rely on that one instead?
Pierre-Marie Pédrot (Nov 24 2020 at 12:08):cc @Erik Martin-Dorel
Enrico Tassi (Nov 24 2020 at 12:08):what happens if it is called on a .vo generated without native on?
Pierre-Marie Pédrot (Nov 24 2020 at 12:09):if the dependencies are not compiled, it will error.
Pierre-Marie Pédrot (Nov 24 2020 at 12:09):coqc does the same btw
Pierre-Marie Pédrot (Nov 24 2020 at 12:10):The above PR is just optionally moving the responsibility of native compilation to a program different from coqc
Pierre-Marie Pédrot (Nov 24 2020 at 12:10):so, it'll only affect coqmakefile users.
Enrico Tassi (Nov 24 2020 at 12:12):you move the responsability but you don't pass the same flags... aren't you looking for troubles?
Karl Palmskog (Nov 24 2020 at 12:12):in other words, nearly every third-party Coq project maintainer will now have to make decisions about native compilation...
Enrico Tassi (Nov 24 2020 at 12:12):can't you always call it but make it do nothing?
Pierre-Marie Pédrot (Nov 24 2020 at 12:12):@Karl Palmskog nope
Pierre-Marie Pédrot (Nov 24 2020 at 12:13):it doesn't change anything, except for people actively deactivating native compilation
Pierre-Marie Pédrot (Nov 24 2020 at 12:13):it's still following the configure CEP guidelines
Pierre-Marie Pédrot (Nov 24 2020 at 12:14):(i.e. the only behaviour change is if you set configure native-yes and COQEXTRAPARAMS="native no")
Pierre-Marie Pédrot (Nov 24 2020 at 12:18):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
Pierre Roux (Nov 24 2020 at 13:12):@ppedrot : note that currently, NATIVE_COMPILER_DEFAULT doesn't set/unset or trigger anything, it just tells yu what the default behavior is
Pierre-Marie Pédrot (Nov 24 2020 at 13:21):Yes, but CoqMakefile could use this info still.
Pierre-Marie Pédrot (Nov 24 2020 at 13:22):The constraint for the introduction of split-native is to be transparent for exotic (i.e. non-coqmakefile build systems)
Pierre-Marie Pédrot (Nov 24 2020 at 13:22):But it doesn't prevent us to document a preferred flag for native compilation compared to COQEXTRAFLAGS
Pierre-Marie Pédrot (Nov 24 2020 at 13:23):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: Sep 09 2024 at 04:02 UTC