MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
382 stars 82 forks source link

Add compile time dependency on python to readme #463

Open DKuhse opened 4 years ago

DKuhse commented 4 years ago

Hello,

during the compilation of metacoq-translations using opam install . there is a dependency on python. Since not all distributions ship with python by default, it might be nice to note this somewhere, since the (non-verbose) error is somewhat cryptic:

[ERROR] The compilation of coq-metacoq-translations failed at "/home/daniel/.opam/opam-init/hooks/sandbox.sh build make -j3

using the verbose flag, the relevant output is

/usr/bin/env: 'python3': No such file or directory
make[2]: *** [Makefile.coq:344: print-pretty-timed] Error 127

There also appears to be a dependency on sed, but missing it doesn't appear to cause any issues.

mattam82 commented 4 years ago

Thanks for the report! Sadly I don't see an easy way to make the package depend on python in opam