Stream: Coq devs & plugin devs

Topic: Why is coqtail failing in ci?

Ali Caglayan (Aug 24 2020 at 04:10):

The coqtail repo seems to be passing, but it fails in the coq CI. I can't seem to find when this started happening. All I know is that it has happened in #12878 and #12879. The error that gets thrown is ERROR: file not found: tests/test_coqtop.py.

Anybody know what is going on?

Gaëtan Gilbert (Aug 24 2020 at 06:36):

because of https://github.com/whonore/Coqtail/pull/134 which renamed the test directory afaict

Wolf Honore (Aug 24 2020 at 18:21):

Sorry about that. https://github.com/coq/coq/pull/12886 should fix it.

Last updated: Oct 08 2024 at 14:01 UTC