Failed to Build tcoq

[yangky11]

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.

[Luweicai]

Hi, @yangky11. I have met the same problem with you. Do you have any solution now?

[yangky11]

@Luweicai Lol... It has been 5 years. I don't even remember I had this problem. I don't think GamePad is still being maintained. Maybe you should check out CoqGym and LeanDojo?