Skip to content

Latest commit

 

History

History
180 lines (135 loc) · 10.9 KB

048-packaging-coq-native.md

File metadata and controls

180 lines (135 loc) · 10.9 KB
Raw

  • Title: Packaging coq with native_compute

  • Drivers: Erik Martin-Dorel (@erikmd), Pierre Roux (@proux01)

  • URL: #48

Motivation

Currently, the use of native_compute in libraries involving many dependencies is inconvenient (so that nobody actually uses this feature). Indeed, all their dependencies need to be recompiled with the -native-compiler yes option passed to coqc. And this needs to be done in a specific way for each dependency, depending on the build system it uses (see e.g., the doc of coq_makefile), if possible at all.

The overall aim of this proposal is to provide an opam virtual package (named e.g. coq-native) that users can install to automatically (re)compile everything with native_compute (no need for any manual opam pin edit).

Summary

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

The proposed design tackles the following two use cases:

  1. Most users' (who don't even want to hear about native_compute) preferred behavior would be compiling the stdlib and subsequent Coq libraries with -native-compiler no by default.
  2. native_compute users' preferred behavior would be to easily recompile all their libraries with coqc -native-compiler yes (while doing this currently with opam requires passing custom environment variables (if possible) which aren't the same across the build systems used by libraries, thus making the setup for efficiently using native_compute terribly unpractical).

Also, this proposal makes the configuration uniform across the platforms (while native_compute was permanently disabled for macOS to workaround performance issues, cf. coq/coq#11178).

Detailed design

The proposal is three-fold:

  • item 1. Update the coq packaging in ocaml/opam-repository so that Coq's standard library is compiled with -native-compiler yes only if an additional virtual package coq-native has been installed by the user.
  • item 2. Extend the ./configure -native-compiler options:
    • option ./configure -native-compiler yes now impacts the default value of option coqc -native-compiler (in order to precompile both stdlib and third-party libraries with -native-compiler yes);
    • option -native-compiler ondemand (which becomes the default when compiling coq manually) preserves the previous default behavior (modulo the stdlib that is not precompiled anymore).
  • item 3. Optionally: to enhance native_compute support with old versions of Coq (the releases of Coq before 8.13, where item 2 was not implemented), update the opam packaging of the considered libraries.

Regarding item 1:

  • Add an opam metapackage coq-native.1:
opam-version: "2.0"
maintainer: "Erik Martin-Dorel"
authors: "Coq"
homepage: "https://coq.inria.fr/"
bug-reports: "https://github.com/coq/coq/issues"
conflicts: [
  "coq" {< "8.5"}
]
synopsis: "Package flag enabling coq's native-compiler flag"
description: """
This package acts as a package flag for the ambient switch, taken into
account by coq (and possibly any coq library) to enable native_compute
at configure time, triggering the installation of .coq-native/* files
for the coq standard library and subsequent coq libraries.

This implements item 1 of CEP #48 <https://github.com/coq/ceps/pull/48>.

Remarks:

1. you might face with issues installing this package flag under macOS,
   see <https://github.com/coq/coq/issues/11178>.
2. this package is not intended to be used as a dependency of other
   packages (notably as installing or uninstalling this package may
   trigger a rebuild of all coq packages in the ambient switch).
3. the option set by this package will be automatically propagated to
   coqc for coq >= 8.13 (but the packaging of coq libraries for
   earlier versions of coq may need an update: for details, see item 3
   of CEP #48 <https://github.com/coq/ceps/pull/48>).
"""
  • Add the following lines in the opam packages of coq:
diff --git a/packages/coq/coq.8.11.2/opam b/packages/coq/coq.8.11.2/opam
index fdb19e9da7..3d3dee7570 100644
--- a/packages/coq/coq.8.11.2/opam
+++ b/packages/coq/coq.8.11.2/opam
@@ -23,6 +23,9 @@ depends: [
   "num"
   "conf-findutils" {build}
 ]
+depopts: [
+  "coq-native"
+]
 build: [
   [
     "./configure"
@@ -33,7 +36,9 @@ build: [
     "-libdir" "%{lib}%/coq"
     "-datadir" "%{share}%/coq"
     "-coqide" "no"
-    "-native-compiler" {os = "macos"} "no" {os = "macos"}
+    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
   ]
   [make "-j%{jobs}%"]
   [make "-j%{jobs}%" "byte"]

Regarding item 2:

The coqc option -native-compiler ondemand corresponds to the default behavior since 4ad6855 (8.5beta3).

The following array, adapted from this coq/coq#12564 comment (and that other one), summarizes all behaviors (the changes are highlighted in bold):

configure (<8.13) configure (>=8.13) coqc outcome requirements
N/A yes yes (default if omitted) .coq-native/* + temporary (when calling native_compute) dependencies should be compiled with the same native flags
N/A yes ondemand temporary none
N/A yes no none none
yes ondemand yes .coq-native/* + temporary (when calling native_compute) dependencies should be compiled with the same native flags
yes ondemand ondemand (default if omitted) temporary none
yes ondemand no none none
no no yes none none
no no ondemand none none
no no no none none

Note also that (for each version of coq), the stdlib is only precompiled with ./configure -native-compiler yes. It is not precompiled with ./configure -native-compiler ondemand for coq >= 8.13.

PR coq/coq#13352 implements this item.

Regarding item 3:

Assuming we want to use native_compute on Coq < 8.13 with coq-mathcomp-ssreflect (or any library built with coq_makefile), the opam file has to be extended like this (see e.g. Coq's refman):

diff --git a/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.10.0/opam b/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.10.0/opam
--- a/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.10.0/opam
+++ b/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.10.0/opam
@@ -6,7 +6,8 @@
 dev-repo: "git+https://github.com/math-comp/math-comp.git"
 license: "CeCILL-B"
 
-build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
+build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed}]
 install: [ make "-C" "mathcomp/ssreflect" "install" ]
 depends: [ "coq" { (>= "8.7" & < "8.12~") } ]

Doing this, one can notice that the appropriate .coq-native directory has successfully been installed along the .vo of the library:

find "$(opam config var lib)" -name ".coq-native" | grep ssreflect

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 in Coq refman);
  • for dune / coq.theory: this will require Coq 8.12.1+ and a version of dune implementing PR ocaml/dune#3210 (cf. this comment 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 repository.

Alternatives

  • A different but related idea was mentioned in Zulip: "OPAM: try out coq as a compiler" (PR coq/opam-coq-archive#595).

    • This would require opam 2.0 (which is not a drawback).
    • This could be viewed as an alternative of this CEP's package flag.
    • Unfortunately, this alternative would be even coarser than this CEP (as all opam packages, not only those of coq libraries, would be recompiled).

  • A new strategy, called split-native, has been discussed in the CEP PR:

    • Assume a coq package foo2 depends on foo1; there would be two extra packages foo2-native and foo1-native, with at least the following dependencies:
      • foo2 → foo1
      • foo2-native → foo1-native
      • foo2-native → foo2
      • foo1-native → foo1
    • This idea relies on the ability to generate ./coq-native/*.cmxs directly from the .vo files.
    • A PoC of this idea has been implemented in PR coq/coq#13287.
    • Yet this PR won't be ready for Coq 8.13, and it will also require some extra tooling, to automatically generate the *-native packages, and more generally keep coq/opam-coq-archive maintenance tractable.
    • And there might be some corner cases where, e.g., package foo contains both A.v and B.v, B requires A and relies on native_compute.
    • Finally, the implementation of the coqc -native-compiler ondemand setting could be optimized.

Conclusion and perspectives

  • This CEP was discussed at the 2020-11-13 weekly Coq call, in order to provide full-blown native_compute support for the Coq 8.13 release (cf. PR coq/coq#13352).
  • The Coq team agreed on considering this CEP for Coq 8.13, while the split-native strategy could be further developed for a later Coq release.

Note: at the time this CEP is written, the Coq refman still lacks some documentation of the -native-compiler option; but progress on this is tracked in issue coq/coq#12564; and that doc might incorporate the array above.