Stream: Coq devs & plugin devs

Topic: Dune, coqtop, and native_compute


view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jun 05 2023 at 09:52):

after you configure, do you regenerate the build rules?

view this post on Zulip Ali Caglayan (Jun 05 2023 at 09:52):

it seems you might be using the build rules (eithout native) from before the configure .

view this post on Zulip Gaëtan Gilbert (Jun 05 2023 at 09:52):

make world should do that

view this post on Zulip 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: Jun 13 2024 at 08:02 UTC