Stream: Coq devs & plugin devs

Topic: ✔ Best way to get output of dune exec


view this post on Zulip Gaëtan Gilbert (Jul 23 2021 at 15:03):

not easy
what for?

view this post on Zulip Ali Caglayan (Jul 23 2021 at 15:07):

I was thinking about grouping some related tests together

view this post on Zulip Ali Caglayan (Jul 23 2021 at 15:07):

but I guess it's not really worth it

view this post on Zulip Guillaume Melquiond (Jul 23 2021 at 15:07):

Just give them the same name prefix.

view this post on Zulip Notification Bot (Jul 23 2021 at 15:15):

Ali Caglayan has marked this topic as resolved.

view this post on Zulip Ali Caglayan (Jul 23 2021 at 16:42):

When running the test-suite I keep getting this error:

File "unit-tests/lib/coqProject.ml", line 23, characters 6-13:
23 |       docroot = None;
           ^^^^^^^
Error: This record expression is expected to have type
         CoqProject_file.project
       The field docroot does not belong to type CoqProject_file.project
make: *** [Makefile:331: unit-tests/lib/coqProject.ml.log] Error 2

is that normal?

view this post on Zulip Gaëtan Gilbert (Jul 23 2021 at 16:48):

someone merge https://github.com/coq/coq/pull/14625 already

view this post on Zulip Gaëtan Gilbert (Jul 23 2021 at 16:49):

the test suite currently has bugs with the unit test setup, I'm guessing it's picking up your installed coq instead of the development coq

view this post on Zulip Ali Caglayan (Jul 23 2021 at 18:12):

I'm confused. I added some tests that will fail to failure but the CI says they "should be rejected"? https://github.com/coq/coq/pull/14699/checks?check_run_id=3145593030

view this post on Zulip Gaëtan Gilbert (Jul 23 2021 at 18:13):

iirc failure/ works just like success/, you should just use success/ with Fail

view this post on Zulip Ali Caglayan (Jul 23 2021 at 18:13):

oh

view this post on Zulip Ali Caglayan (Jul 23 2021 at 18:14):

In that case I can stick them all in one file probably


Last updated: Oct 21 2021 at 21:03 UTC