It may be prettier to have a new value for the -native-compiler configure option.
ie instead of -native-compiler-default-yes yes one would pass -native-compiler yes-yes (or some other string instead of yes-yes)

It may be prettier to have a new value for the -native-compiler configure option.

+1

I'm not sure if hardcoding this is a good idea; IMHO these kind of options should be better controlled by the build system [coq_makefile or dune]. Having this kind of hardcoded values makes it the life of the build system harder due to a combinatorial explosion on possible flags values. Now the build system has to do another query to see what coqc is going to do by default, and maybe override it in case the user wants a quick build.

It may be prettier to have a new value for the -native-compiler configure option.
ie instead of -native-compiler-default-yes yes one would pass -native-compiler yes-yes (or some other string instead of yes-yes)

Indeed, here is an offer with ondemand.

I'm not sure if hardcoding this is a good idea; IMHO these kind of options should be better controlled by the build system [coq_makefile or dune].

To me, this always has been and definitely remains a configure option. But if you have a rationale supporting your opinion, I'd be happy to hear it.

Now the build system has to do another query to see what coqc is going to do by default,

Sorry, I din't follow you, why would you like to know the default value ?

and maybe override it in case the user wants a quick build.

If by quick you mean without native, you can just pass -native-compiler no to coqc, nothing new here.

Anyway, this PR is certainly missing a dune part. I was unable to write it because I still don't understand how the configuration phase is done in the dune build process.

To me, this always has been and definitely remains a configure option. But if you have a rationale supporting your opinion, I'd be happy to hear it.

The example I pointed out is a good one I think: when in dev mode, you may want to skip native compilation for performance purposes, of even proofs as done in vos , so indeed you want a coqc that is able to work both ways.

Sorry, I din't follow you, why would you like to know the default value ?

The build system needs to know what object files will coqc produce, in particular to prevent stale files when building incrementally. For example if you compile a.v with native, then you compile again without native, an incremental build needs to clean the stale cmxs files.

Anyway, this PR is certainly missing a dune part. I was unable to write it because I still don't understand how the configuration phase is done in the dune build process.

Nothing to be done for dune in this tree, dune rules would have to be adapted themselves to query the configure option of coqc. This introduces a bit painful build dependency tho, as .v rules cannot be computed until the configure rule has been queried. Usually, the more static the build DAG is, the better performance you may get. This is a concern in the real world once you have 10 or 100s thousand targets [which happens when doing a composed build]

One alternative is just to patch coq_makefile, so when the configure flag is set, it uses the right flag.

One alternative is just to patch coq_makefile, so when the configure flag is set, it uses the right flag.

That wouldn't work for build systems other than coq_makefile.

Nothing to be done for dune in this tree, dune rules would have to be adapted themselves to query the configure option of coqc.

dune could call coqc with the option always explicit, not relying on the default.

dune could call coqc with the option always explicit, not relying on the default.

That would completely ruin the whole point of the CEP though.

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

That wouldn't work for build systems other than coq_makefile

Well it is not gonna work either now as unless you patch them, they won't realize that additional files are being built.

By the way, we should converge to a single build system for Coq packages so that would be moot [and if people want to have their own DIY build system, IMHO they are on their own]

That wouldn't work for build systems other than coq_makefile

Well it is not gonna work either now as unless you patch them, they won't realize that additional files are being built.

No, coq_makefile is working fine, whenever .coq-native are produced, they get installed,that's it.

By the way, we should converge to a single build system for Coq packages so that would be moot [and if people want to have their own DIY build system, IMHO they are on their own]

Well, we shouldn't make their life ridiculously harder though.

No, coq_makefile is working fine, whenever .coq-native are produced, they get installed,that's it.

I was answering to your question about systems other than coq_makefile.

Well, we shouldn't make their life ridiculously harder though.

Actually this PR would make their life harder as now they have to implement a method to query Coq config options in order to know what's being built

The build system needs to know what object files will coqc produce, in particular to prevent stale files when building incrementally. For example if you compile a.v with native, then you compile again without native, an incremental build needs to clean the stale cmxs files.

That may be a stupid question but can't we just clean the cmxs whether there is actually one or not ?

No, coq_makefile is working fine, whenever .coq-native are produced, they get installed,that's it.

I was answering to your question about systems other than coq_makefile.

Sorry, they indeed would have to do the same (and the few cases I'm aware of do it).

I wrongly believed that the related CEP was backwards compatible, but with this PR I realize now that it requires changes to the coqc binary. Since it was its main interest, I think I should make an alternative proposal based on split compilation that is essentially a configure-agnostic way of achieving on-demand compilation.

That may be a stupid question but can't we just clean the cmxs whether there is actually one or not ?

Well that'd result in a pretty suboptimal incremental build.

By the way, we should converge to a single build system for Coq packages so that would be moot [and if people want to have their own DIY build system, IMHO they are on their own]

That discussion should happen in a separate issue — I thought we had already concluded that too many packages still rely on coq_makefile for a switch, and migrating many of them would anyway fall on coq-community. We also agreed that dune has pretty limited programmability, as long as a dhall-ocaml doesn’t get born.

I'm not sure if hardcoding this is a good idea; IMHO these kind of options should be better controlled by the build system [coq_makefile or dune]. Having this kind of hardcoded values makes it the life of the build system harder due to a combinatorial explosion on possible flags values. Now the build system has to do another query to see what coqc is going to do by default, and maybe override it in case the user wants a quick build.

That might be great when using dune, but it’s not as great when using opam. A point of the CEP was to get better behavior by default, even without changing each coq package around. Technically, that limits changes to the repos of coq, dune, and maybe opam-coq-repository. And even if everybody used dune, I’m not sure that would save much opam-packaging work — unless the result of installing an opam-dune package depends on some global flag, which IIUC you were objecting to?

I wrongly believed that the related CEP was backwards compatible, but with this PR I realize now that it requires changes to the coqc binary.

These changes seem easy enough to get in for 8.13, and they give you a better default. You said split packages would not get in before 8.14; even if your PR can be finished in time, it’s not clear the build-system changes can be done in time as well for 8.13, and ditto for the changes to all the packages.

That may be a stupid question but can't we just clean the cmxs whether there is actually one or not ?

Well that'd result in a pretty suboptimal incremental build.

Why? You could also move potential outputs out-of-the way, and restore them if needed. I’m also not sure why “asking coq for a bunch of flags” is intrinsically hard — add one coq option to dump the config in machine-readable format, and call that at the start.

These changes seem easy enough to get in for 8.13, and they give you a better default.

You can only coq_makefile as suggested an still you get the same effect; this PR, as-is, is breaking everything else.

Why? You could also move potential outputs out-of-the way, and restore them if needed.

If you clean the cmxs files, then you need to regenerate them again at each build, all of them. To restore the outputs you need to know them, that's beyond what make can do.

I’m also not sure why “asking coq for a bunch of flags” is intrinsically hard — add one coq option to dump the config in machine-readable format, and call that at the start.

First, it adds complexity. Not having to parse anything is much much better than having to parse. Second, when you compose with coq, a common scenario for example in CI, your build rules need to get Coq configure and queried, a move from a static dependency graph to a dynamic graph. While doable, I don't think the benefits justify the added complexity.

Hi @ejgallego,

You can only coq_makefile as suggested an still you get the same effect; this PR, as-is, is breaking everything else.

by "breaking everything else", do you just mean "this PR breaks the CI currently", or "this PR is incomplete because the dune counterpart is missing in this PR"? − because as I'm not very fluent with dune, it is hard for me to see how easy it is to finalize that part…

it adds complexity. Not having to parse anything is much much better than having to parse.

But I believe the native_compiler configure option was already there… so it just amounts to a change of a bool option to a 3-valued option :)
and this increase of complexity is just due to the fact this PR currently puts forth a new default value for coqc -native-compiler, while keeping the ability to trigger the "ondemand" behavior (albeit the discussion in the CEP mentioned at some point that this "ondemand" behavior could just as well have been disabled, IIRC)

You can only [change] coq_makefile as suggested an[d] still you get the same effect;

This does sound interesting, and potentially better! It doesn't help users of DIY build systems — but they can make the same choice independently.

this PR, as-is, is breaking everything else.

More accurately, I think it breaks dune and might help DIY build system; changing coq_makefile seems indeed potentially better.

Why? You could also move potential outputs out-of-the way, and restore them if needed.

If you clean the cmxs files, then you need to regenerate them again at each build, all of them. To restore the outputs you need to know them, that's beyond what make can do.

No? If you recompile a %.v->%.vo file, remove only %.cmxs. Or move it away and restore it if coq has not created the cmxs file. E.g.:

%.vo: %.v
	mv "%.cmxs" "%.cmxs-old"
	coqc ...
	[ -f "%.cmxs" ] || mv "%.cmxs-old" "%.cmxs"

Optionally, restore the old file even if the contents have not changed (à la KBuild), to restore the old timestamps, but adding features to coq_makefile is likely overkill.

I do agree that the above change might add some complexity to weigh in to this proposal, and 4 lines of untested bash don't prove it's easy.

You can only [change] coq_makefile as suggested an[d] still you get the same effect;

This does sound interesting, and potentially better! It doesn't help users of DIY build systems — but they can make the same choice independently.

Coul you be more precise? If that means configuring coq_makefile rather than coqc, this just breaks every build sytem (but coq_makefile).

this just breaks every build sytem (but coq_makefile).

Let’s assume Emilio’s proposal won’t break dune. Let coq_makefile pass the desired default setting of native_compute to coq. Why are other build-systems broken, if they'd get the same behavior as today?
I see they won't get better defaults, but the existing defaults will work as well/badly as today.
And support for alternative build systems must have some limit — keeping coqc behaviors unchanged.

keeping coqc behaviors unchanged

Note that the default behavior of coqc is not changed by this pull request. If the user does not explicitly pass -native-compiler yes to the configure script, then coqc will behave exactly the same as today (whether the -native-compiler option is passed or not).

Since there seems to be some confusion, let me stress the following point. This pull request does not change the behavior of coqc; it changes the behavior of the configure script. Rather than modifying the behavior of configure -native-compiler yes, @SkySkimmer proposed to add configure -native-compiler yes-yes instead. I tend to prefer @proux01 's solution, since it makes the correspondence between the options of configure and coqc more intuitive. But honestly, both -native-compiler variants are fine with me, as long as we finally fix the mistake done by some misguided idiot five years ago.

The only difference in default behavior is that the stdlib is no longer precompiled for native compute (which you were interested in @Blaisorblade IIRC ;-) )

Let coq_makefile pass the desired default setting of native_compute to coq. Why are other build-systems broken, if they'd get the same behavior as today?

Because they won't get the expected behavior for native_compute users (except maybe by hacking them to discover the setting hidden in coq_makefile).

After implementing @SkySkimmer 's idea just above, there is no more duplicate job.

Hi @proux01!
if you need to push-force again, note that this commit validsdp@6c538ed
has a buggy hyperlink coq#48 in the commit message (it should read coq/ceps#48)

After implementing @SkySkimmer 's idea just above, there is no more duplicate job.

Thanks a lot for your patience @proux01 ; I'd say that the PR looks good to go.

We had a failure on the test suite however:

File "./primitive/float/compare.v", line 326, characters 0-48:
Error:
Dynlink error: The module `Coq_native18246a' is already loaded (either by the main program or a previously-dynlinked library)

0m0.000000s 0m0.000000s
0m11.230000s 0m13.280000s
==========> FAILURE <==========
    primitive/float/compare.v...Error! (should be accepted)

This is not the first time I see this, and it looks quite fishy. I'll re-run the job for now.

re-running fixed the failure, I think we can merge , @gares , do you need your comments addressed before merge?

We had a failure on the test suite however:

File "./primitive/float/compare.v", line 326, characters 0-48:
Error:
Dynlink error: The module `Coq_native18246a' is already loaded (either by the main program or a previously-dynlinked library)

0m0.000000s 0m0.000000s
0m11.230000s 0m13.280000s
==========> FAILURE <==========
    primitive/float/compare.v...Error! (should be accepted)

This is not the first time I see this, and it looks quite fishy. I'll re-run the job for now.

We should probably have a look with a native_compute and dynlink expert at some point. I unfortunately know close to nothing on the subject.

I just removed equations and metacoq specific code following upstream fixes.

So I do need to update the pins... anyway, please merge.

@coqbot: merge now

I'm surprised this didn't break the fiat-parsers CI, as it breaks the CI on our end because the native compiler hangs for over ten minutes trying to compile libraries to native code. Is the correct solution to this to add -arg -native-compiler -arg ondemand to _CoqProject?

Apparently, we got the CI to pass with export COQEXTRAFLAGS='-native-compiler no' so yes, something like that should work.