Stream: Coq devs & plugin devs

Topic: Error: Unbound module Nativevalues


view this post on Zulip Ali Caglayan (May 14 2022 at 16:52):

I'm getting these in the CI in the test-suite port. Am I missing linking something?

File "./.coq-native/Nbteauto.native", line 1, characters 5-17:
1 | open Nativevalues
         ^^^^^^^^^^^^
Error: Unbound module Nativevalues
Error: Native compiler exited with status 2 (in case of stack overflow,
increasing stack size (typically with "ulimit -s") often helps)

view this post on Zulip Ali Caglayan (May 14 2022 at 16:54):

Command looks like:

(cd _build/default/test-suite/success && .bin/coqc -boot -I ../../../install/default/lib -R ../../theories Coq -R ../prerequisite TestSuite -Q ../../user-contrib/Ltac2 Ltac2 -async-proofs off bteauto.v) > _build/default/test-suite/success/bteauto.v.log

view this post on Zulip Ali Caglayan (May 14 2022 at 16:55):

Is it OCAMLPATH that controls where the compiler looks for things?

view this post on Zulip Ali Caglayan (May 14 2022 at 16:56):

How do we enable native compilation locally? I'm guessing it is now enabled in the CI but I have no idea what to change locally.

view this post on Zulip Pierre Roux (May 14 2022 at 17:18):

I think it is ./configure -native-compiler yes

view this post on Zulip Ali Caglayan (May 14 2022 at 17:46):

Thank you!


Last updated: Feb 05 2023 at 19:29 UTC