Ali Caglayan (May 14 2022 at 16:52): 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)
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
Is it OCAMLPATH that controls where the compiler looks for things?
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.
Pierre Roux (May 14 2022 at 17:18):I think it is ./configure -native-compiler yes
Ali Caglayan (May 14 2022 at 17:46):Thank you!
Last updated: Dec 07 2023 at 14:02 UTC