search

ml4tp / gamepad

A Learning Environment for Theorem Proving
Apache License 2.0
71 stars 15 forks source link

build tcoq failed #7

Open dsmic opened 5 years ago

dsmic commented 5 years ago

OK, my error, the OCaml was not probably set to version 4.05.0, it was set to an old one.

maybe others have the same problem, so I keep the description:

I get the following error running ./build_tcoq.sh

Makefile.install:66: die Regel für Ziel „install-binaries“ scheiterte make[1]: Verzeichnis „/home/detlef/RNN/gamepad/tcoq“ wird verlassen Makefile:154: die Regel für Ziel „submake“ scheiterte

in tcoq/build.log: Makefile.build:542: die Regel für Ziel „printing/ptcoq.cmo“ scheiterte make[1]: Verzeichnis „/home/detlef/RNN/gamepad/tcoq“ wird verlassen Makefile:154: die Regel für Ziel „submake“ scheiterte

if I run make in the tcoq subdir I get more detailed info: File "printing/ptcoq.ml", line 46, characters 8-22: Error: Unbound value Sys.getenv_opt Makefile.build:542: die Regel für Ziel „printing/ptcoq.cmo“ scheiterte make[1]: [printing/ptcoq.cmo] Fehler 2 make[1]: Verzeichnis „/home/detlef/RNN/gamepad/tcoq“ wird verlassen Makefile:154: die Regel für Ziel „submake“ scheiterte make: [submake] Fehler 2

I tried to carefully follow the instructions, any hints would be great, thanks