How can I enable multicore and/or quick(no proof check) compilation in dune?
The coq.theory stanza has the optional flags to pass arguments to coqc (see doc Stanza reference — dune documentation). I don’t know anything about multicore.
These features are not officially supported yet, -vio [ -quick is deprecated these days will definitively not work; for the -async family of flags you could try your luck with (flags ...)
Thank you for the answers. I tried -vio and -vos separetly in flags but getting following error in both:
File "src/Framework/Primitives/_unknown_", line 1, characters 0-0:
Error: Rule failed to generate the following targets:
- src/Framework/Primitives/BaseTypes.voIndeed, that is what I meant “not supported”, for vos there is an experimental patch.
Actually, adding support for -vio for example would be quite trivial, the thing that we have not resolved is the user interface; how would one tell dune about “now you use -vio for this set of targets”. If you have a good proposal I’d love to hear.
I think adding vo-related aliases is the 5th item in my Coq + Dune todo list, that would be a way for example [it is there as to enable the generation of native stuff as an alias].
A super quick workaround that we could do in dune 2.9 is to actually add the rule for the .vio files, but provide no further interface; that would still allow you to call dune build $set_of_vio_files and have it work correctly.
Unfortunately -vos is way more complicated as Coq does erase .vo files when using -vos [not the best decision IMHO] so when setting up the rules for a library you must choose which mode you are in.