Coq 8.13 and coq-native

[gares]

Since Coq 8.13 CEP 48 is implemented.

In short, when the (empty) package coq-native is installed, coq is configured to pre compile stuff for native_compute.
We should be asking the question in the platform scripts (and provide a -coq-native=[y/n] option).

[MSoegtropIMC]

OK, I will do this. On which platforms is Coq-native expected to work? I think on Windows it should also work if one uses the cygwin/opam based from source variant which includes opam.

[gares]

All of them. It seems it is slow on osx (the loader is slow), so I guess it should contain a generic warning that compilation time for .v files may increase (but you get fast native_compute).

[gares]

To be tested in the installers, which don't ship ocamlc. It should work with at most a warning.

[MSoegtropIMC]

@gares : I am reviewing old issues ...

I have two questions / thoughts on this:

• users already complain that the questions asked by the script are lengthy, so I wonder if we should just provide a command line option - it is more a pro feature. or alternatively we could have an option / question to ask "pro" questions
• I wonder if the parallel install method of Coq Platform works - it does request all packages at once. Would I need to install the coq-native package upfront sequentially?

[gares]

I think you would need to install it upfront, even before installing coq.

Brainstoming: what about telling power users needing the feature to edit the package selection file and add coq-native upfront?

[Zimmi48]

What about having a question asking users if they want the pro or basic mode and showing very few questions to users of the latter?

[MSoegtropIMC]

Triage note: planned for the 8.20 release.