[coq] Improve support for Coq's native compiler

[ejgallego]

Current support for Coq's native_compiler in Dune is unsatisfactory and we should fix it before (using coq 1.0) (maybe we can add a milestone coq-1.0 or something like that?)

In particular, the choice done in Coq's current implementation is a bit similar to how OCaml works for "byte/native":

• at configure time, the user will tell Coq whether native compilation is enabled or not
• then, the build systems will detect that calling coqc -config and generate the .cmxs if needed

There is another interesting alternative which I tried to implement, which is using coqnative which is the standalone native compiler, but it is much slower as of today.

I guess for 1.0, we should just call coqc -config and if native is enabled, and release profile is selected, we just tell Coq to generate the native files too (or setup the coqnative install / build rules)

[rgrinberg]

which is using coqnative which is the standalone native compiler, but it is much slower as of today.

Out of curiosity, why is that the case?

[ejgallego]

@rgrinberg the native compiler still needs to read (Marshall) all the .vo files that are imported, as of today that amounts to a 33% overhead in Coq's stdlib for example.

We should be able to optimize that.

For the purposes of this PR, I think it is not so important if we setup coqnative rules or the current ones. What we need to do in both cases is to read coq -config and act accordingly.

I wish #4908 would be an option, but I understand that is not so easy.

[rgrinberg]

Just to clarify, coqnative only takes .vo files as input?

[ejgallego]

Yes, see the PR #4750 , the rules are really straighforward.

[rgrinberg]

Okay, then I propose that you just let me setup the native rules "jsoo" style for local & installed theories. That means I'm going to set them up "on demand" whenever someone needs a native target rather than on package installation time. However much slower coqnative is, the benefit of eliding the native build for the 90% who don't care for it is going to be far more important.

[ejgallego]

We currently elide the native build unless demanded in the stanza too, so how's coqnative be different here?

[rgrinberg]

Well, what do you do on installation time? E.g. dune build -p mathcomp, do you build and install the stuff for native compute? If the answer is without native compute, what happens when someone uses mathcomp and also wants native compute?

And yes, the cache is what makes all of this possible. With the cache, we don't need to worry about rebuilding the same installed theories over and over.

[ejgallego]

If the answer is without native compute, what happens when someone uses mathcomp and also wants native compute?

What we need to do here is to install the native stuff if Coq was configured with -native on. What we do now is people add (mode native) to dune files using some hack to query coqc -config

On Opam, coqc is configured to use native when the coq-native package is installed.

Regarding coqnative vs coqc -native on it doesn't matter at all with current setup, the first is just slower, both play fine with cache etc...

[rgrinberg]

What we need to do here is to install the native stuff if Coq was configured with -native on. What we do now is people add (mode native) to dune files using some hack to query coqc -config

On Opam, coqc is configured to use native when the coq-native package is installed.

Glad we're on the same page as to what the consequences are. Now let's remind ourselves why this is such a poor user experience. Let's consider the following user session:

• User install mathcomp
• Realizes that she needs native compute to improve performance
• Then runs $ opam install coq-native
• Opam then recompiles ALL coq packages to use native compute. Regardless of whether they're necessary for building mathcomp with native compute or not.
• Bonus step: other unrelated things are now broken because opam selected a slightly different build plan because of whatever reason.

This is a highly inefficient and inconvenient workflow. Moreover, if the user then publishes a package downstream, they have no means to express that a particular theory needs native compute for performance. They can only express an extremely coarse dependency on coq-native which send downstream users into a similar recompilation hell.

Regarding coqnative vs coqc -native on it doesn't matter at all with current setup, the first is just slower, both play fine with cache etc..

Yes, I only expressed a preference for coq-native because it seemed easier to setup the on-demand rules. If it's equivalent effort with both then of course I don't particularly care.

[proux01]

• User install mathcomp
• Realizes that she needs native compute to improve performance
• Then runs $ opam install coq-native
• Opam then recompiles ALL coq packages to use native compute.

We all agree this is not ideal and there is a long term, yet unprecise, plan to depart from that (c.f. coq/ceps#48 for the detailled discussion). However, as a user, I would already be happy if things were just working as you describe (I can just keep two opam switches with and without native for instance). Today with dune, things are even much worse than this not ideal situation, as they look more like:

• User install mathcomp-foo
• Realizes that she needs native compute to improve performance
• Then runs $ opam install coq-native
• Opam then recompiles ALL coq packages to use native compute BUT a few ones built with dune which ignores the native setting

and everything ends up broken. In my opinion, this is the main, if not only, point deterring me from using dune to build Coq libraries nowadays.

[ejgallego]

Indeed @rgrinberg this is not a great experience, tho dune cache would trigger for the .vo files if we setup things a bit more carefully and use coqnative.

I'd be happy indeed if we close this issue with the auto-detection feature, as this provides a very good packaging experience.

The improved workflow you propose is to have a coq-mathcomp-native package, right? I'd be happy to move forward with #4908 then, but seems trickier than I expected.

[Alizter]

Fixed by #6409