Guillaume Melquiond (Jun 02 2023 at 13:27): Guillaume Melquiond (Jun 02 2023 at 13:27):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?
Ali Caglayan (Jun 05 2023 at 09:52):it seems you might be using the build rules (eithout native) from before the configure .
Gaëtan Gilbert (Jun 05 2023 at 09:52):make world should do that
Ali Caglayan (Jun 05 2023 at 09:53):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