Failed to Build tcoq
Opened this issue · 2 comments
yangky11 commented
Hello,
I'm building toq on macOS and I saw this error in my tcoq/time.log when executing build_tcoq.sh:
*** Warning: in file theories/Init/Notations.v, declared ML module coretactics has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module extratactics has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_auto has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_class has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_eqdecide has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_rewrite has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module coretactics has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module extratactics has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_auto has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_class has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_eqdecide has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_rewrite has not been found!
File "lib/pp_control.ml", line 61, characters 22-33:
Error: This expression has type bytes -> int -> int -> unit
but an expression was expected of type string -> int -> int -> unit
Type bytes is not compatible with type string
make[1]: *** [lib/pp_control.cmo] Error 2
make[1]: *** Waiting for unfinished jobs....
make: *** [submake] Error 2
install: bin/coqdep: No such file or directory
make[1]: *** [install-tools] Error 71
make: *** [submake] Error 2
real 1m4.070s
user 0m54.648s
sys 0m58.573s
Any idea? Thanks.