Stream: Coq devs & plugin devs

Topic: ✔ Best way to get output of dune exec


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

How do I get the output of dune exec?

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

you run it?

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

Yes, but on the shim its completely silent

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

you mean dune exec -- dev/shim/coqc-prelude not-a-real-file doesn't print an error?

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

That prints an error

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

Ok im doing something wrong I guess

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

I'm trying to generate the .out file for a test

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

whats the best way to do this

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

My output should be a coq message not an error so it looks like it isn't printed

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

OK, nevermind I think my file is just wrong

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

what sort of message? for instance coqc won't print the "foo is defined" messages but does print Check output

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

Ah, that's why I'm confused

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

How do I get those to print?

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

if you want to test coqtop messages you have to run coqtop
eg coqtop < file.v

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

Is it easy to add a folder in sucess or fail or do I have to change the makefile

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: Feb 06 2023 at 20:02 UTC