Stream: MetaCoq

Topic: errors in coq CI log

view this post on Zulip Gaëtan Gilbert (Sep 24 2020 at 14:27):

In Coq's CI log for metacoq there are a bunch of ignored errors like https://gitlab.com/coq/coq/-/jobs/754770686#L830

Fatal error: exception Sys_error("../template-coq/build: No such file or directory")

what is this about?

view this post on Zulip Matthieu Sozeau (Sep 24 2020 at 14:34):

This is due to the difference between the two build strategies of metacoq (local, where build is here, and global/opam where we don't need the include)

Last updated: Feb 09 2023 at 02:02 UTC