Stream: Coq users

Topic: Using native_compute


view this post on Zulip Martin Karup Jensen (May 09 2024 at 08:57):

Hello, Coq community.

I'm trying to use the native_compute tactic to evaluate an expression, but Coq keeps falling back to vm_compute.
For example, even just trying to compile

Eval native_compute in (1 + 1).

with coqc gives me the warning:

Warning: native_compute disabled at configure time; falling back to
vm_compute. [native-compute-disabled,native-compiler]
     = 2
     : nat

If I add the flag -native-compiler yes to coqc, I get the warnings

While loading initial state:
Warning: Native compiler is disabled, -native-compiler yes option ignored.
[native-compiler-disabled,native-compiler]
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]
File "./native_test.v", line 2, characters 0-31:
Warning: native_compute disabled at configure time; falling back to
vm_compute. [native-compute-disabled,native-compiler]
     = 2
     : nat

How do I enable the use of native_compute? Does Coq have to be built with a specific flag?
I have installed Coq version 8.17.1 through opam. I know there is the coqnative package in opam, and installing it requires recompiling all of my coq packages, which I was hoping to avoid, since one of them fails to build with coqnative (I know I should probably open an issue...).

Thanks in advance!

view this post on Zulip Guillaume Melquiond (May 09 2024 at 09:06):

Yes, you need to install the coq-native package. The fact that it recompiles all your Coq packages is actually the point, since you need native a "native"-enabled version of your packages.


Last updated: Jun 22 2024 at 15:01 UTC