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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2021 at 11:41):

Hi @MackieLoeffel , to get rid of the warning you can either disable it in your flags declaration, or bump to (using coq 0.3); sorry for the problems

view this post on Zulip MackieLoeffel (Sep 22 2021 at 11:46):

Thanks, I will update to coq 0.3 then.

view this post on Zulip Notification Bot (Sep 22 2021 at 11:53):

MackieLoeffel has marked this topic as resolved.

Last updated: Jun 03 2023 at 18:01 UTC