When I build a Coq project using dune with Coq 8.14+rc1, I get a lot of the following warnings:
Running: (cd _build/default && theories/lithium/.bin/coqc -w -notation-overridden -w -redundant-canonical-projection -w -native-compiler-disabled -native-compiler ondemand -R theories/lithium refinedc.lithium theories/lithium/base.v) While loading initial state: Warning: The native-compiler option is deprecated. To compile native files ahead of time, use the coqnative binary instead. [deprecated-native-compiler-option,deprecated]
I am not using the native compiler in my project (as far as I can tell). How can I get rid of this warning? Why does
-native-compiler ondemand to coqc and can I disable this somehow?
My dune-project file is the following:
(lang dune 2.7) (name refinedc) (using coq 0.2)
Last updated: Oct 16 2021 at 07:02 UTC