CEP for packaging coq-native #48

erikmd · 2020-10-28T16:56:08Z

This CEP describes a new strategy for setting the default value for the -native-compiler option (in coqc and in the opam packaging).

It has been written by @proux01 and I, following a suggestion by @Zimmi48 − in coq/coq#12757 (comment)

I Cc some coq devs involved in the features/packaging discussed here: @maximedenes @silene @ejgallego @gares @palmskog @clarus @SkySkimmer @vbgl @Blaisorblade (sorry if I forget someone, but feel free to Cc other coq devs recursively…)

Direct link to the rendered .md (final version)

@erikmd

* Drivers: @erikmd and @proux01

ejgallego · 2020-10-28T20:25:45Z

IMHO depopts is flawed and should be avoided, as we did for example in the packaging of lablgtk3; there are several issues as this proposal stands:

compilation is not anymore deterministic, this is gonna be at odds with other packaging systems such as Debian's
the build system has to understand the packaging setup, this is fragile and behaves badly in compositional setups
the flag is all-or-nothing, so in the case of only needing a few packages with native support users still do pay the full price

I strongly recommend that instead libraries provide a coq-$lib-native package with the corresponding files, as outlined in related discussions.

silene · 2020-10-28T20:53:35Z

I am a bit confused by items 2 and 3. If item 2 changes the default to -native-compiler on, why is item 3 needed?

By the way, I still strongly believe that any solution that requires item 3 is a bad solution.

Also, it seems that item 1 completely forbids native_compute (unless coq-native is installed). The tactic cannot even be used in ondemand mode. Am I misunderstanding?

Blaisorblade · 2020-10-29T04:31:01Z

Also, it seems that item 1 completely forbids native_compute (unless coq-native is installed). The tactic cannot even be used in ondemand mode. Am I misunderstanding?

That's intentional, because today that's the only way to avoid any overhead from native-compute searching/loading native libraries. It'd be better if you could compile it in, but still have no overhead by default, if that's easy enough to do, but this hasn't been done since 8.11 because of problems.

But to be sure: would it be so hard to require a command-line option (and otherwise immutable) to make native-compute available? The challenge IIRC was with "more mutable" flags.

silene · 2020-10-29T04:43:25Z

hat's the only way to avoid any overhead from native-compute searching/loading native libraries.

What do you mean? Are you saying that the overhead is currently paid even if no native libraries are compiled (which is the whole point of ondemand)?

silene · 2020-10-29T05:05:27Z

To be clearer, I see three meaningful cases:

If no compiler is installed or if dynamic linking is broken, then -native-compiler no is enforced.
If the standard library is not compiled to native code, then -native-compiler yes is forbidden (because impossible) and -native-compiler ondemand is the default. (That is, if the user types native_compute, it works. But no native library is ever precompiled.)
If package coq-native is installed (or whichever global configuration method is chosen), then -native-compiler yes is the default, i.e., native libraries are precompiled for any user contribution.

Zimmi48 · 2020-10-29T08:33:05Z

I am a bit confused by items 2 and 3. If item 2 changes the default to -native-compiler on, why is item 3 needed?

By the way, I still strongly believe that any solution that requires item 3 is a bad solution.

According to the text of the CEP, item 2 is for upcoming versions of Coq and item 3 is only for already released versions of Coq.

silene · 2020-10-29T08:41:13Z

According to the text of the CEP

Oops, my mistake. This is indeed written not just once but twice in the CEP. (But not in the detailed description of item 3, so I kind of missed it.)

palmskog · 2020-10-29T09:44:59Z

While I understand the motivation and rationale behind the proposal, I can see using depopts like this lead to a nightmare in when debugging errors in Coq projects using opam packages.

More specifically, under this proposal, is there any way at all to determine post-hoc with any certainty that Coq was actually compiled with native compute? For example, it looks like it is possible to install (or uninstall) coq-native after you have already compiled Coq without (or with) native compute support, and opam will not complain, or require a recompile of Coq.

Zimmi48 · 2020-10-29T09:52:07Z

opam will not complain, or require a recompile of Coq

Is that how deopts work? This would be crazy!

silene · 2020-10-29T09:53:11Z

For example, it looks like it is possible to install (or uninstall) coq-native after you have already compiled Coq without (or with) native compute support, and opam will not complain, or require a recompile of Coq.

Are you sure? I thought that was the whole point of depopts. Such a package is not strictly needed, but it behaves as if it was depends, and thus forces a recompilation when added, changed, or removed (unless marked build-only).

silene · 2020-10-29T09:56:55Z

Documentation of depopts: "The implementation uses this information to define build order and trigger recompilations, but won't automatically install depopts when installing the package." (Emphasis is mine.)

Zimmi48 · 2020-10-29T10:08:41Z

OK, so this invalidates Karl's argument and also Emilio's claim that "compilation is not anymore deterministic".

Zimmi48 · 2020-10-29T10:12:25Z

It seems to me that the most important argument of Emilio against this is actually the third one: "the flag is all-or-nothing, so in the case of only needing a few packages with native support users still do pay the full price".

And this comes with an alternative proposal:

I strongly recommend that instead libraries provide a coq-$lib-native package with the corresponding files, as outlined in related discussions.

It seems to me that the trade-off / debate is here: loss of flexibility for the user (native compilation is for a whole switch, unless they mess with opam pin edit) vs a lot more packaging work (every package has to be duplicated).

silene · 2020-10-29T10:33:48Z

It is a huge pain for packagers, but it is also a minor pain for users. Indeed, if users want to use native_compute, they need to double check that all the libraries their current proof depend on have been compiled with -native-compiler yes (i.e., the -native version of the packages have been installed and not just the standard ones). Otherwise, Coq will silently revert to the slower ondemand mode for native_compute.

In the case of a single coq-native package, that is the only package the users have to check. And presumably users will check it only once, and then they can just forget about it, even if they later need to install new dependencies for their proof.

gares · 2020-10-29T11:00:29Z

I would go for the simpler option, one package to opt in your switch. Exactly as you opt in a compiler feature like flambda.
If opam was able to distribute binaries, then I would lean toward the other option. But it can't, so it's just more pain for packages and users, IMO.

Blaisorblade · 2020-10-29T11:26:13Z

Are you saying that the overhead is currently paid even if no native libraries are compiled (which is the whole point of ondemand)?

Ondemand will try to load native libraries, and it will succeed on the std library. We noticed when that costed 10x on one MacOS machine, but I can measure overhead even on Linux.

And yes, that should have better fixes, but that seems hard and hasn’t happened for years. But I’m happy to be proven wrong.

On the “separate foo-native package” idea, I thought that relied on new Coq features of creating native code from vo files? IIRC they were described as “easy”, but that was months ago.

silene · 2020-10-29T11:48:59Z

Ondemand will try to load native libraries, and it will succeed on the std library.

But that is only if the standard library has been compiled to native code. I don't see any reason to compile the standard library to native code if the coq-native package is not installed. Why would you want to do that?

Blaisorblade · 2020-10-29T12:47:17Z

I don't see any reason to compile the standard library to native code if the coq-native package is not installed. Why would you want to do that?

Hm, that was in today's setup. You have a point; however, you're making a (reasonable but untested) assumption that native-compiler ondemand doesn't have any downsides left in this scenario.

On the one hand, it might be worth trying that out, and changing that in the future if more bugs show up.
On the other hand, what would be the use of native_compute in this scenario? The usecases are likely limited.

silene · 2020-10-29T13:12:24Z

what would be the use of native_compute in this scenario? The usecases are likely limited.

The difference between yes and ondemand is that you pay a large overhead at the start of your native_compute call. It can take a few seconds to compile all the dependencies of your current goal on-the-fly.

So, if you want to use native_compute because your vm_compute proof takes 5 seconds, then it is worth it only in mode -native-compiler yes. But if your vm_compute proof takes a few minutes, then native_compute is worth it whether the mode is yes or ondemand.

As I explained in some other venue, the interval tactic offers an i_native_compute option that instructs the tactic to use native_compute instead of vm_compute under the hood. And this option is certainly useful and used, even in ondemand mode. But the choice is currently left to the user, because the tactic cannot guess whether the proof will be numerically intensive and thus will last long enough to compensate the initial overhead.

To summarize, the use cases for native_compute are the same whether the mode is yes or on ondemand. It is just that the threshold at which the user decides to replace vm_compute by native_compute is later for ondemand.

(Currently, if you have an Opam installation of CoqInterval, then MathComp, Flocq, Coquelicot, and Bignums, are compiled on-the-fly to native code when you use tactics interval and integral, since none of these library are compiled with -native-compiler yes. So, my assumption about ondemand has seen a lot of testing.)

ppedrot · 2020-10-29T13:13:35Z

My 2cts:

If we go that way, it seems that the ondemand flag becomes mostly useless and could even be deprecated in a future release.
There is also the option to store the native compilation result inside the vo files. Doing this would prevent further split of the packages in two parts as proposed by @ejgallego, but it would probably make the current mainline proposal slightly easier, by explicitly marking the vo files as being native-able or not.

ejgallego · 2020-10-29T18:31:02Z

OK, so this invalidates Karl's argument and also Emilio's claim that "compilation is not anymore deterministic".

No it doesn't in the sense that any 3rd party package can actually produce non-local changes, so it turns out that builds are not compositional anymore, in the sense that building A and B separately is not the same as building A + B.

See the thread for lablgtk.

I am strongly against any solution using depopts.

ejgallego · 2020-10-29T18:34:27Z

I am strongly against any solution using depopts.

On the other hand using two packages as Enrico proposes should work fine; so we could go in the line of a virtual coq package depending on either coq-compiler or coq-compiler-native.

ejgallego · 2020-10-29T21:38:34Z

There is also the option to store the native compilation result inside the vo files. Doing this would prevent further split of the packages in two parts as proposed by @ejgallego, but it would probably make the current mainline proposal slightly easier, by explicitly marking the vo files as being native-able or not.

IMHO whether to add the cmxs inside the vo is pretty orthogonal to the packaging discussion at hand, indeed having the objects separately is a bit more flexible.

One question that I think has not been addressed is what control the user has over their own libs. For example it is not clear if the user should have control à la (mode native) flag that is implemented in ocaml/dune#3210 .

silene · 2020-10-30T06:19:20Z

I am strongly against any solution using depopts.

That does not make sense to me. You say that builds involving packages with depopts directives are non-compositional, which is true. But so are builds with conflicts directives or version-specific depends directives.

For example, you say that having two packages coq-compiler and coq-native-compiler is fine. But since they each will have a conflicts directive regarding the other, we still get non-compositional builds.

The very reason we have a tool like Opam which embeds a full-blown constraint solver is because builds are inherently non-compositional in the real world.

By the way, even your idea of having coq-$lib-native packages is inherently non-compositional, since they will have to conflict with the corresponding non-native packages. The only way we could make it compositional is if Coq was changed so that it can build the .cmxs files independently of the .vo files, which I hope is not what you are proposing.

ppedrot · 2020-10-30T11:17:33Z

The only way we could make it compositional is if Coq was changed so that it can build the .cmxs files independently of the .vo files

It shouldn't be that hard though. I must confess I'd prefer a solution where native libraries are a parallel package, rather than the solution advocated in this CEP which is essentially introducing a different, incompatible Coq compiler flavour.

silene · 2020-10-30T12:53:59Z

I'd prefer a solution where native libraries are a parallel package

Even if they are parallel packages (which will be painful for maintainers), they will transitively need to depend on coq-stdlib-native (or whatever its name), which itself will depend on a version of Coq that is not compiled with -native-compiler no. So, I am not sure to understand how that avoids having two compiler flavors. Or do you mean that -native-compiler no should never be available as an Opam package?

erikmd · 2020-10-30T12:59:30Z

@ppedrot

The only way we could make it compositional is if Coq was changed so that it can build the .cmxs files independently of the .vo files

It shouldn't be that hard though.

I'm not very savvy on that .cmxs change, however IINM it would only be applicable for upcoming releases of Coq… while this CEP proposes a unified change for each coq opam package since 8.5.

I must confess I'd prefer a solution where native libraries are a parallel package, rather than the solution advocated in this CEP which is essentially introducing a different, incompatible Coq compiler flavour.

OK. but IMHO this "compiler flavor" (which amounts to define a package flag setting the -native-compiler option for generating .coq-native/* files for the stdlib and the 3rd party coq packages) seems much simpler for the opam-coq-archive maintainers and contributors and coq users: they just need to handle this choice in a single package choice, rather than maintaining 2 flavors for each coq library (coq-$library, coq-$library-native), all the more as:

these two flavors coq-$library and coq-$library-native should be marked as mutually incompatible, and should rely on the same flavor for each of their dependencies to be consistent,
and having these two flavors per coq library would not get rid of the need to have two versions of the coq package itself (either with a depopt or with another solution), because of the choice of natively-precompiling the stdlib or not…

So I tend to agree with @silene and @gares 's remarks #48 (comment) and #48 (comment)

erikmd · 2020-11-16T19:58:35Z

Hi @silene, good catch! that makes sense, indeed.

$ cat foo.v
From mathcomp Require Import ssralg.
Definition z := GRing.zero.

$ coqc -native-compiler yes  foo.v
File "./.coq-native/Nfoo.native", line 11, characters 2-68:
Error: Unbound module Nmathcomp_algebra_ssralg
File "./foo.v", line 3, characters 0-27:
Warning: Removed file ./foo.vo
Error: Native compiler exited with status 2

erikmd · 2020-11-16T20:05:57Z

so I guess the CEP is ready to be merged if no one objects :)

(unless you'd want to add yet another remark in this section about the scenario we discussed again just now?)

proux01

A few minor comments, LGTM otherwise.

text/048-packaging-coq-native.md

erikmd · 2020-11-17T21:40:37Z

Applied. Thanks again @proux01 :)

This an implementation of point 2 of CEP coq#48 coq/ceps#48 Option -native-compiler of the configure script now impacts the default value of the option -native-compiler of coqc. The -native-compiler option of the configure script is added an ondemand value, which becomes the default, thus preserving the previous default behavior. The stdlib is still precompiled when configuring with -native-compiler yes. It is not precompiled otherwise.

This an implementation of point 2 of CEP coq/ceps#48 coq/ceps#48 Option -native-compiler of the configure script now impacts the default value of the option -native-compiler of coqc. The -native-compiler option of the configure script is added an ondemand value, which becomes the default, thus preserving the previous default behavior. The stdlib is still precompiled when configuring with -native-compiler yes. It is not precompiled otherwise.

This an implementation of point 2 of CEP coq/ceps#48 coq/ceps#48 Option -native-compiler of the configure script now impacts the default value of the option -native-compiler of coqc. The -native-compiler option of the configure script is added an ondemand value, which becomes the default, thus preserving the previous default behavior. The stdlib is still precompiled when configuring with -native-compiler yes. It is not precompiled otherwise. (cherry picked from commit 1596cdb)

erikmd · 2020-11-23T16:59:18Z

Hi, the implem. of item 2 (coq/coq#13352) is now part of the v8.13 branch; I'm going to prepare the PR of item 1 (for Coq < 8.13).
Should the CEP PR be merged beforehand (Cc @Zimmi48)?

Zimmi48

No, go ahead with your PR, but let's merge this one soon.
I propose to merge by the end of the week if no more comments (with my renaming suggestion taken into account or not).

text/048-packaging-coq-native.md

erikmd · 2020-12-07T09:20:59Z

Hi @proux01 @Zimmi48, hi all,

just FYI when ocaml/opam-repository#17690 will be merged, I plan to add the coq-native package in all Docker-Coq images for Coq ≥ 8.5. Indeed given that there has been no change regarding "item 3" up to now, it will essentially keep the docker-coq images backward-compatible (i.e., native_compute will stay enabled and the standard library be precompiled).

The question whether it is the best option might arise though for coqorg/coq:8.13-beta1 and coqorg/coq:dev, as this will change the default behavior of coqc for reverse dependencies.

But if you don't object, I'll do the same change in docker-coq for Coq ≥ 8.13 (adding coq-native).

Indeed when I discussed this quickly with Théo at the CUDW, he mentioned this may be useful to further test users' libs w.r.t. the native precompilation − and it is always possible to override the coqc -native-compiler flag, as Pierre did in PR coq/coq#13352 :
https://github.com/coq/coq/pull/13352/files#diff-884511acd9617ef77c36fb77c0824bcb8d49a4877212494817d7dedcfbae693f

* Otherwise, with Coq 8.13: #=== ERROR while compiling coq-coqeal.1.0.5 ===================================# # [...] # File "./refinements/multipoly.v", line 1532, characters 0-67: # Warning: Duplicate clear of sz_m' [duplicate-clear,ssr] # File "./refinements/.coq-native/NCoqEAL_refinements_multipoly.native", line 66, characters 14-82: # Error: Unbound module NSsrMultinomials_mpoly # Error: Native compiler exited with status 2 * This fix is temporary: when multinomials will require Coq >= 8.12.1, one could then rely on ocaml/dune#3210, which provides the `(mode native)` stanza. * For details, see also: coq/ceps#48

* Otherwise, with (coq.8.13.2 + coq-native): #=== ERROR while compiling coq-coqeal.1.0.5 ===================================# # [...] # File "./refinements/multipoly.v", line 1532, characters 0-67: # Warning: Duplicate clear of sz_m' [duplicate-clear,ssr] # File "./refinements/.coq-native/NCoqEAL_refinements_multipoly.native", line 66, characters 14-82: # Error: Unbound module NSsrMultinomials_mpoly # Error: Native compiler exited with status 2 * This fix is temporary: when multinomials will require Coq >= 8.12.1, one could then rely on ocaml/dune#3210, which provides the `(mode native)` stanza. * For details, see also: coq/ceps#48

liyishuai · 2022-06-05T03:47:24Z

text/048-packaging-coq-native.md

+# Note to library developers and package maintainers
+
+To fully benefit from `native_compute` with a library using Coq 8.5+, some (`opam`) packaging update may be required for this library's dependencies:
+
+- for `coq_makefile`: no change required for Coq 8.13+; otherwise follow **item 3** above (related to Section [Precompiling for `native_compute`](https://coq.github.io/doc/master/refman/practical-tools/utilities.html?highlight=coq_makefile#precompiling-for-native-compute) in Coq refman);
+- for `dune / coq.theory`: this will require Coq 8.12.1+ and a version of `dune` implementing [PR ocaml/dune#3210](https://github.com/ocaml/dune/pull/3210) (cf. [this comment](https://github.com/coq/ceps/pull/48#issuecomment-727020253) by **@ejgallego**); otherwise (without native support), Dune will just ignore the native parts and no `./coq-native/*.cmxs` file will be installed.
+
+Note that these changes could be performed directly in the existing packages gathered in the [coq/opam-coq-archive](https://github.com/coq/opam-coq-archive) repository.


Please make this section more visible, at least by searching "native" in refman.

I found here by searching "native" on Discourse and following the link in this post, which doesn't seem so intuitive.

Actually since Dune 3.0 we could just make native work automatically, I'm gonna open a dune issue.

Please emphasize that Coq stanza should also be upgraded to (coq 0.3). I figured it out by reading between the lines in ocaml/dune#3210.

erikmd added 3 commits October 28, 2020 17:54

Create CEP "packaging-coq-native"

3d31b4f

* Drivers: @erikmd and @proux01

Rephrase some sentences & Fix typos

e8dfd27

Update the CEPS URL

a87d800

docs: Final edits for the CEP 48

7337e5e

erikmd force-pushed the packaging-coq-native branch from eaab5d7 to 7337e5e Compare November 16, 2020 20:28

proux01 approved these changes Nov 17, 2020

View reviewed changes

Address review by @proux01

35b5450

erikmd force-pushed the packaging-coq-native branch from d3c6f5d to 35b5450 Compare November 17, 2020 21:39

erikmd added 2 commits November 17, 2020 22:52

fix: Make the stdlib remark clearer

0fdc291

docs: Add URL

ae68948

Zimmi48 approved these changes Nov 23, 2020

View reviewed changes

text/048-packaging-coq-native.md Outdated Show resolved Hide resolved

Replace "meta-package" with "virtual package"

bd40b83

erikmd mentioned this pull request Nov 23, 2020

Packaging coq-native ocaml/opam-repository#17690

Merged

Zimmi48 merged commit f2e5103 into coq:master Nov 27, 2020

erikmd deleted the packaging-coq-native branch November 27, 2020 12:17

erikmd mentioned this pull request Dec 7, 2020

Add depopts: coq-native in coq.opam.docker coq/coq#13588

Merged

Zimmi48 mentioned this pull request Dec 24, 2020

Updating Coq's (native-compiler, flambda) configure options in opam packages coq/coq#12757

Closed

erikmd mentioned this pull request Apr 8, 2021

fix: Use coq_makefile instead of dune, temporarily math-comp/multinomials#41

Closed

liyishuai mentioned this pull request Jun 5, 2022

Update Dune Lysxia/coq-simple-io#55

Merged

liyishuai reviewed Jun 5, 2022

View reviewed changes

proux01 mentioned this pull request Jun 7, 2022

[coq] Improve support for Coq's native compiler ocaml/dune#5831

Closed

CEP for packaging coq-native #48

CEP for packaging coq-native #48

Conversation

erikmd commented Oct 28, 2020 • edited Loading

ejgallego commented Oct 28, 2020

silene commented Oct 28, 2020

Blaisorblade commented Oct 29, 2020

silene commented Oct 29, 2020

silene commented Oct 29, 2020

Zimmi48 commented Oct 29, 2020

silene commented Oct 29, 2020

palmskog commented Oct 29, 2020 • edited Loading

Zimmi48 commented Oct 29, 2020

silene commented Oct 29, 2020

silene commented Oct 29, 2020

Zimmi48 commented Oct 29, 2020

Zimmi48 commented Oct 29, 2020

silene commented Oct 29, 2020

gares commented Oct 29, 2020

Blaisorblade commented Oct 29, 2020

silene commented Oct 29, 2020

Blaisorblade commented Oct 29, 2020 • edited Loading

silene commented Oct 29, 2020

ppedrot commented Oct 29, 2020

ejgallego commented Oct 29, 2020

ejgallego commented Oct 29, 2020

ejgallego commented Oct 29, 2020

silene commented Oct 30, 2020

ppedrot commented Oct 30, 2020

silene commented Oct 30, 2020

erikmd commented Oct 30, 2020

erikmd commented Nov 16, 2020

erikmd commented Nov 16, 2020

proux01 left a comment

Choose a reason for hiding this comment

erikmd commented Nov 17, 2020

erikmd commented Nov 23, 2020

Zimmi48 left a comment

Choose a reason for hiding this comment

erikmd commented Dec 7, 2020 • edited Loading

liyishuai Jun 5, 2022

Choose a reason for hiding this comment

ejgallego Jun 5, 2022

Choose a reason for hiding this comment

liyishuai Jun 5, 2022

Choose a reason for hiding this comment

erikmd commented Oct 28, 2020 •

edited

Loading

palmskog commented Oct 29, 2020 •

edited

Loading

Blaisorblade commented Oct 29, 2020 •

edited

Loading

erikmd commented Dec 7, 2020 •

edited

Loading