Stream: Dune devs & users

Topic: Warning: The native-compiler option is deprecated.

view this post on Zulip MackieLoeffel (Sep 22 2021 at 09:55):

When I build a Coq project using dune with Coq 8.14+rc1, I get a lot of the following warnings:

Running[2]: (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.

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 dune pass -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