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
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-native package, if you are interested in that
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: