Stream: MetaCoq

Topic: compilation errors not in the wiki


view this post on Zulip Jason Gross (Feb 24 2023 at 01:36):

What's up with

CAMLC -c gen-src/caml_nat.mli
File "gen-src/caml_nat.mli", line 2, characters 22-35:
2 | val caml_int_of_nat : Datatypes.nat -> int
                          ^^^^^^^^^^^^^
Error: Unbound module Datatypes
Command exited with non-zero status 2
gen-src/caml_nat.cmi (real: 0.06, user: 0.03, sys: 0.03, mem: 14032 ko)
make[2]: *** [Makefile.plugin:726: gen-src/caml_nat.cmi] Error 2
CAMLC -c gen-src/caml_byte.mli
File "gen-src/caml_byte.mli", line 1, characters 5-9:
1 | open Byte
         ^^^^
Error: Unbound module Byte
Hint: Did you mean Bytes?

?

view this post on Zulip Jason Gross (Feb 24 2023 at 01:44):

Ah, I guess this means I need to remove the .vo file from Extraction.v or w/e and recompile

view this post on Zulip Matthieu Sozeau (Feb 24 2023 at 15:52):

I suppose, it’s hard to tell


Last updated: Jun 03 2023 at 17:29 UTC