Coq 8.13 and coq-native about platform HOT 6 OPEN

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?

from platform.

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.

from platform.

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).

from platform.

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

from platform.

@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?

from platform.

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?

from platform.