The Coq mailing list

[Erik Martin-Dorel <e.mdorel AT gmail.com>]

[This is a cross-post of the following Discourse thread:
 https://coq.discourse.group/t/about-the-native-compiler-flag-and-the-coq-native-opam-package-to-be-released-before-coq-8-13-beta1/1147]

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

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

```
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:

- The fulltext of the CEP 48:

  https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#readme

- or in particular for library developers and package maintainers, this section of the CEP 48 that explains how to make your opam packages aware of the new coq-native package for Coq < 8.13:

  https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#note-to-library-developers-and-package-maintainers

Kind regards,

Erik

--

Érik Martin-Dorel

http://erik.martin-dorel.org/