How can one test whether the native compiler works correctly when trying to fix a bug in Coq? More precisely, I have done the following:
./configure -native-compiler yes -no-ask make world dune exec -- dev/shim/coqtop
and I get
Error: Unbound module Nativevalues Error: Native compiler exited with status 2
after you configure, do you regenerate the build rules?
it seems you might be using the build rules (eithout native) from before the configure .
make world should do that
the shim isnt designed to do native iirc but building vo from the prelude should still build native deps
Last updated: Nov 29 2023 at 22:01 UTC