How can I enable multicore and/or quick(no proof check) compilation in dune?
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,
-quick is deprecated these days will definitively not work; for the
-async family of flags you could try your luck with
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.vo
Indeed, 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.
-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.