Stream: Coq devs & plugin devs

Topic: CoqMakefile environment variables


view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 11:35):

What is the exact status of the COQMF_* variables in CoqMakefile?

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 11:36):

Are they the preferred way to interact with the coq options?

view this post on Zulip Enrico Tassi (Nov 24 2020 at 11:36):

what do you mean exactly?

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 11:36):

Or are they for internal use?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 24 2020 at 11:37):

does it makes sense to let the user override it at the command line?

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 24 2020 at 11:37):

if so, provide also a nicer name

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 11:38):

You mean, without the COQMF?

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 11:39):

Maybe it's a XY problem, so here is the story

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 11:39):

but the problem is that CoqMakefile is unaware of native compilation.

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 11:40):

At least, in the recommended setup, which is setting COQEXTRAFLAGS+="native-compiler yes"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 11:43):

(in particular, the CI unsets native compilation on some dev via COQEXTRAFLAGS)

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 11:43):

"What do?"

view this post on Zulip Enrico Tassi (Nov 24 2020 at 12:00):

I don't get why COQMF_NATIVE_blablah wins over COQEXTRAFLAGS+="-native off".

view this post on Zulip Enrico Tassi (Nov 24 2020 at 12:01):

said otherwise coqc -native-compiler ondemand -native-compiler off is what you get no?

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:03):

Yes, for coqc, so coqc does not compile the file.

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:03):

But there is now a new program coqnative.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 24 2020 at 12:05):

Should it receive COQEXTRAFLAGS as arguments anyway?

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:05):

Morally coqnative is a variant of coqchk.

view this post on Zulip Paolo Giarrusso (Nov 24 2020 at 12:05):

Hm

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:06):

namely, COQMF_NATIVE... and COQEXTRAFLAGS

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:06):

one is easier to manipulate than the other.

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:07):

Shouldn't we rely on that one instead?

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:08):

cc @Erik Martin-Dorel

view this post on Zulip Enrico Tassi (Nov 24 2020 at 12:08):

what happens if it is called on a .vo generated without native on?

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:09):

if the dependencies are not compiled, it will error.

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:09):

coqc does the same btw

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:10):

so, it'll only affect coqmakefile users.

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Enrico Tassi (Nov 24 2020 at 12:12):

can't you always call it but make it do nothing?

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:12):

@Karl Palmskog nope

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:13):

it doesn't change anything, except for people actively deactivating native compilation

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 12:13):

it's still following the configure CEP guidelines

view this post on Zulip 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")

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 13:21):

Yes, but CoqMakefile could use this info still.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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: Oct 16 2021 at 03:02 UTC