About the -native-compiler flag and the coq-native opam package (to be released before Coq 8.13+beta1)

Announcements
1

Dear Coq users,

This announcement deals with Coq’s native_compute support (which is typically interesting to get increased performance when using reflexive tactics). It focuses in particular on the -native-compiler flag for both ./configure and coqc binaries, as well as the corresponding packaging in opam-repository.

TL;DR: Following the discussion that took place in the CEP 48 (Coq Enhancement Proposal “Packaging coq-native”), a new virtual package coq-native will be released in opam-repository on this Monday 7 December (before the release of Coq 8.13+beta1). So if opam proposes you to upgrade an existing switch, or if you create a brand new opam switch with a given version of Coq ≥ 8.5, you may consider installing first (or simultaneously w.r.t. coq) the coq-native package, if you are interested in that native_compute feature.

Minimal complete example

when Coq 8.13+beta1 will be released, you could run for instance:

opam switch create coq-8.13 4.07.1+flambda
eval $(opam env)
opam repository add coq-released https://coq.inria.fr/opam/released
# for beta versions of coq:
opam repository add coq-core-dev https://coq.inria.fr/opam/core-dev
# for beta versions of coq libs:
opam repository add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam update
opam pin add -n -k version coq 8.13+beta1
opam install -y -v -j 2 coq coq-native

Further details, “semantics” of this package

The presence of this “package flag” in the ambient opam switch directly sets the -native-compiler flag when configuring coq: Coq’s stdlib will be pre-compiled for native if and only if this package coq-native is installed, and in this case (for Coq ≥ 8.13), the reverse dependencies of coq will be pre-compiled for native as well by default.

For details on the motivation, the issues that this approach solves, as well as for the implementation itself (which splits into 3 “items”), see:

2 Likes